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]

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.

[samth]

@AlexKnauth what's the current status here?

[AlexKnauth]

I need to rebase again, and then I need to implement the new parse-type case for Box for the optional argument. I think I'll re-visit this that after the current cast and any-wrap/c stuff is done.

[samth]

@AlexKnauth do you want to pick this up again, or should we close this?

[AlexKnauth]

I'll pick it up again starting this Thursday.

[AlexKnauth]

Who should I ask about optimizing box/sc contracts with contravariant and covariant write and read fields?

(Edit: Resolved)

[samth]

What do you mean? Let's add the semantics first, and then do optimization.

[AlexKnauth]

That makes sense. However, the reason I asked is that without me adding anything specifically for box/sc optimizations, the optimizer still seems to be trying to optimize parts of them away, resulting in failing optimizer tests. These tests have comments like don't optimize if any contracts are non-flat --- but do optimize under guarded constructors, and they test that it goes through the optimizer unchanged. The problem is that it is trying to optimize them, and I'm not sure what the right thing to do is.

[bennn]

Those are my comments & tests. If box/sc is no longer invariant, they need to be updated.

The idea with the tests is:

• if there's an (or/sc sc_0 sc_1)
• and sc_0 is not flat
• then the optimized contract should be something like (or/sc sc_0+ sc_1+) and NOT any/sc

To change the tests, I think you just need to change what's inside the expected or/scs. You could also change them to use vector/sc instead of box/sc.

EDIT: yeah so for a failure like this, the test needs to be updated. The "actual" is right and the "expected" should be changed to use any/sc:

(or/sc set?/sc (list/sc (flat/sc (syntax symbol?))) (box/sc (flat/sc (syntax symbol?)) (flat/sc (syntax symbol?)))) > Optimizer Tests > Static Contracts > Unit Tests > Typed Racket Tests > Trusted Positive
FAILURE
original:   #<or/sc #<flat/sc set?> #<list/sc #<flat/sc symbol?>> #<box/sc #<flat/sc symbol?> #<flat/sc symbol?>>>
trusted:    positive
expected:   (or/sc (flat/sc set?) (list-length/sc 1) (box/sc (flat/sc symbol?) (flat/sc symbol?)))
actual:     (or/sc (flat/sc set?) (list-length/sc 1) (box/sc (flat/sc symbol?) any/sc))

[AlexKnauth]

Is the "actual" correct for all 10 of those failures, for both "positive" and "negative" as trusted sides?

[bennn]

yes

[AlexKnauth]

The only remaining test failures are these, where the "expected" and "actual" look the same visually printed out, but the test thinks they're different.

The test uses (and (subtype A B) (subtype B A)) to check that the types match, and that's failing.

--------------------
tc-expr tests > Typechecker tests > Unit Tests > Typed Racket Tests > 1436 (if (zero? (random 2)) (box hello) (box (quote hello)))
FAILURE
location:   ("<pkgs>/typed-racket-test/unit-tests/typecheck-tests.rkt" 1436 8 60243 109)
actual:     #(struct:tc-results (#(struct:tc-result (Boxof/Read (U String Symbol)) (Top | Bot) -)) #f)
expected:   #(struct:tc-results (#(struct:tc-result (Boxof/Read (U String Symbol)) (Top | Bot) -)) #f)
tc-expr did not return the expected value. The types don't match.
--------------------
--------------------
tc-expr tests > Typechecker tests > Unit Tests > Typed Racket Tests > 1440 (if (zero? (random 2)) ((inst box Natural) 3) ((inst box Integer) -5))
FAILURE
location:   ("<pkgs>/typed-racket-test/unit-tests/typecheck-tests.rkt" 1440 8 60472 108)
actual:     #(struct:tc-results (#(struct:tc-result (Boxof Nonnegative-Integer Integer) (Top | Bot) -)) #f)
expected:   #(struct:tc-results (#(struct:tc-result (Boxof Nonnegative-Integer Integer) (Top | Bot) -)) #f)
tc-expr did not return the expected value. The types don't match.
--------------------

[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?