add separate read and write types for Box types

[AlexKnauth]

The Boxof type now has two forms:

• (Boxof t), a type for boxes that can contain values of type t. You can write t values into the box with set-box!, and read t values from the box with unbox.
• (Boxof write-t read-t), a type for boxes that only allows writing write-t values with set-box!, while reading with unbox produces read-t.

The write-t position is contra-variant, and the read-t position is covariant. Read-only boxes can be expressed with (Boxof Nothing read-t), and unions of box types make sense since the read-ts can be unioned together while the write-ts are restricted.

[AlexKnauth]

Still need to make a constructor for the more general box type, and fix printing to use that. What should it be called?

(Edit: Resolved)

[stamourv]

You may want to move those out of the invariant types section.

[AlexKnauth]

Ok done.

[stamourv]

Re more general type: You mean the constructor that exposes both type arguments? I don't know how much sense it would make to expose that.

I'm also not 100% clear on the use case. You mentioned better support for unions of box types, and I remember a discussion on IRC last week on that topic, but the particular example in that discussion left me unconvinced. Would you mind elaborating a bit?

FWIW, ISTR @ntoronto wanting something similar for vectors, to have a nicer API for the math library. I think he ended up going with arrays as functions (which have the right variance) to work around that.

Aside from the comments, implementation looks good.

[AlexKnauth]

When I said "unions of box types," I was really thinking in my head "unions of vector types, when I do the same thing for vectors." For that I was thinking of this discussion on the mailing list, which started as talking about (U (Vectorof Index) (Vectorof Integer)), which came about because of using the In-Indexes type from math/array.

[AlexKnauth]

I was also thinking of read-only boxes as (U (Boxof a) (Boxof Nothing)).

[AlexKnauth]

Re more general type:
Mostly because of printing the types.

For example set-box! can take a box that allows a to be written, but allows Any to be read, which allows the set-box! of a union to work.
Right now the type of set-box! prints as:

(All (a)
  (-> (Unknown
       Type:
       #(struct:Box
         1416
         #(struct:combined-frees #hasheq((a . #(struct:Contravariant))) ())
         #(struct:combined-frees #hasheq() ())
         #f
         box
         a
         Any))
      a
      Void))

Where it should really be:

(All (a) (-> (Box/Write-Read a Any) a Void))

Is Box/Write-Read the best name for this?

[stamourv]

Ah, that makes sense.
What about Read-Write-Box? It's consistent with other type names.

[AlexKnauth]

I wanted write to be before read to make the argument order clear, but Write-Read-Boxof sounds good.

(Though I'm also wondering, would changing Read-Only-Boxof to Boxof/Read-Only instead make sense?)

[stamourv]

Usually, read comes before write. Could you change it in the box type representation?

[AlexKnauth]

Write before read is consistent with Parameterof, parameter/c, and box/c, as well as with the co- and contra- variance of function types. Input before output. I could change it, but then it would be inconsistent with those.

[stamourv]

Oh, ugh. In regular English, though, "read" usually goes before "write"...
Consistency with other bits of Racket is more important, let's do w-r.

[AlexKnauth]

Would a set of types like this make sense?

(Boxof/Write-Read w r) ; can write w, read r
(Boxof/Write w) ; = (Boxof/Write-Read w Any)
(Boxof/Read r) ; = (Boxof/Write-Read Nothing r)
(Boxof t) ; = (Boxof/Write-Read t t)

Or this, depending on what we think is better:

(Write-Read-Boxof w r) ; can write w, read r
(Write-Boxof w) ; = (Write-Read-Boxof w Any)
(Read-Boxof r) ; = (Write-Read-Boxof Nothing r)
(Boxof t) ; = (Write-Read-Boxof t t)

Would that set of types make sense? Does the Boxof/Write type make sense? (It's the type that set-box! requires as an argument)

[stamourv]

I prefer the latter.
If we're going to expose the second in the type for set-box!, then we should provide it.

[samth]

I think I prefer the former, but why not just have Boxof work like Parameterof and take either 1 or 2 type arguments?

[AlexKnauth]

Right now, Boxof is a polymorphic type, not a type constructor syntax (like -> for example). If it were a syntax type constructor, there would have to be a special case in parse-type, right? Also is there anything you can do with polymorphic types that you can't do with type constructor syntax identifiers? I thought it would be better to keep it as a normal type.

[AlexKnauth]

Ok, I just renamed Read-Only-Boxof to Boxof/Read and added Boxof/Write as well. Read operations such as unbox take (Boxof/Read a) as arguments, and write operations such as set-box! take (Boxof/Write a) as arguments.

[AlexKnauth]

What do you think? Is it worth another special case in parse-type to make Boxof take an optional argument, or should I leave it as is?

[samth]

Yes, I think it's worth the special case. What do other people think?

[stamourv]

Sure.

[AlexKnauth]

When tc-e gets the type, it doesn't normalize it, and subtyping on unions of boxes doesn't work without normalizing it first. How should I fix this? Do I fix subtyping to merge unions of boxes before going through them?

[samth]

I don't understand why this is needed. What's different than how pairs work?

[AlexKnauth]

You're right. The analogous case for Boxof is this:

For merging boxes (Boxof Aw Ar) and (Boxof Bw Br), if the merged version works

(Boxof (∩ Aw Bw) (U Ar Br)) <: (Boxof Cw Cr)

Then Cw <: both Aw and Bw, and Ar and Br are both <: Cr. Using those, the non-merged verision

(U (Boxof Aw Ar) (Boxof Bw Br)) <: (Boxof Cw Cr)

Should also work because (Boxof Aw Ar) <: (Boxof Cw Cr) and (Boxof Bw Br) <: (Boxof Cw Cr).

So I think I need to replace each tc-e test I currently have with two tests, one tc-e with the non-merged type, and one subtype test checking that the non-merged type is a subtype of the merged type.

[bennn]

Can you change the type of immutable? to have (-Boxof/Read Univ) as a positive proposition?

(I don't think there's a useful negative proposition)

[bennn]

Should "should be" say "must be"?

[AlexKnauth]

No, because the type (Boxof A B) A </: B can still exist, it's just impossible to write an expression that produces a value of that type. (Unless you use cast or require/typed, something that guards it with a contract, in which case it's nearly impossible for that value to keep to that contract for everything you could do to it. "nearly" because weird uses of impersonators might be able to fake it, but it doesn't make sense in normal code.)

[bennn]

Can you use intersect from infer/intersect.rkt here?

I think that would be better than the cond

[AlexKnauth]

I'm not sure what the implications of using intersect might be. @pnwamk what do you think?

[AlexKnauth]

@pnwamk In what situations is it appropriate to use intersect?

[pnwamk]

Hey sorry -- I'm a little slow coming up to speed on this.

intersect is supposed to compute the logical "and" of two types (performing some simplifications where possible), so if something is both of type T1 and type T2, then saying it is of type (intersect T1 T2) should always be fine.

I guess the only "exception" I can think of is in a few places our handling of intersections is not complete (i.e. at the moment we do not fully handle the application of an intersection of function types -- but this isn't a problem with intersect or intersection types, it's just a deficiency in our code that handles function application at the moment).

Anyway, did that answer your question?

[AlexKnauth]

So I'm guessing it is appropriate to use intersect in normalize-type to determine the "write" type of the merged result of a union of two box types?

[AlexKnauth]

(Re: #225 (comment))
Okay, I've changed this to use intersect.

[AlexKnauth]

@bennn That would mean replacing -BoxTop with (-Boxof/Read Univ) here.

Would that actually change anything? BoxTop already allows reading Any from it.

[bennn]

@bennn That would mean replacing -BoxTop with (-Boxof/Read Univ) here.

yes

Would that actually change anything? BoxTop already allows reading Any from it.

I was thinking it would refine (Boxof String) to (Boxof/Read String)

EDIT: nevermind, makes sense to not change immutable? for this

[AlexKnauth]

@bennn No, it wouldn't, because (Boxof String) intersected with (Boxof/Read String) should still be (Boxof String) or the equivalent. Changing it to Boxof/Read wouldn't be a refinement, it would be a "loss of information," assigning it to a supertype.

(Boxof String) <: (Boxof/Read String)

Speaking of intersections, they weren't there when I first started with this pull request. Should I have to change anything about intersections to handle intersections of boxes?

[bennn]

typo: (Boxof/Read t) is not a subtype of (Boxof t)

[AlexKnauth]

I’ll change it to say supertype.

[AlexKnauth]

We need to think of how this pull request should handle programs like this. Should we make box-immutable return a (Boxof X) instead of a (Boxof/Read X) for backwards-compatibility with programs like this?

#lang typed/racket

(define b (box-immutable 5))

(: f : (Boxof Integer) -> Integer)
(define (f b)
  (unbox b))

(f b)

Typed Racket currently lets this pass, but this pull request makes it a type error, because box-immutable returns a read-only box, which can't be used as a (Boxof Integer).

(Edit: Fixed now, this program passes as it should.)

[samth]

I think the point of this PR should be to change what programs people can write, by allowing them to specify read and write types, rather than to change the meaning of existing programs. We definitely shouldn't break that example.

[AlexKnauth]

So box-immutable applied to (generalized) X should return a (Boxof X), not (Boxof/Read X). I need to change that back.

(Edit: Fixed now)

[pnwamk]

I can’t think of a reason why you should avoid using intersect in normalize-type. Should be fine!

…

On Tue, Jan 2, 2018 at 10:57 AM Alex Knauth ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In typed-racket-lib/typed-racket/types/union.rkt <#225 (comment)>: > @@ -30,6 +30,19 @@ (cond [(subtype t* t) (list t)] [(subtype t t*) ts] + ;; the union of two box types is a box type where the write type has to + ;; satisfy both write types, and the read type can satisfy either of the + ;; two read types + [(and (Box? t) (ormap Box? ts)) + (match* (t ts) + [((Box: a-w a-r) (list-no-order (Box: b-w b-r) bs ...)) + (define w + ;; should this use some sort of intersection, or would that So I'm guessing it is appropriate to use intersect in normalize-type to determine the "write" type of the merged result of a union of two box types? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#225 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ADfg6jnL87DZkM9nIC0ytCmXo1wEKv0bks5tGlARgaJpZM4GVTsb> .

[AlexKnauth]

After seeing discussion #1129, I'm thinking this might need a more generalized way of dealing with the opposite-variance-type-pairs for types such as MPairof that have multiple type-arguments. If I did the same thing to MPairof that I'm doing with Boxof here, it would be "ugly" to just put in 4 type-arguments with no extra syntax so signal that they come in opposite-variance pairs. A type-rep data structure for opposite-variance pairs might also be useful, to re-use the common subtyping logic.