add separate read and write types for Box types

Author: AlexKnauth

typed-racket-lib/typed-racket/infer/infer-unit.rkt

@@ -654,9 +654,9 @@
           ;; vectors are invariant - generate constraints *both* ways
           [((Vector: e) (Vector: e*))
            (cg/inv e e*)]
-          ;; boxes are invariant - generate constraints *both* ways
-          [((Box: e) (Box: e*))
-           (cg/inv e e*)]
+          ;; boxes are contravariant for writing, covariant for reading
+          [((Box: e-w e-r) (Box: e-w* e-r*))
+           (% cset-meet (cg e-w* e-w) (cg e-r e-r*))]
           [((Weak-Box: e) (Weak-Box: e*))
            (cg/inv e e*)]
           [((MPair: s t) (MPair: s* t*))

typed-racket-lib/typed-racket/private/type-contract.rkt

@@ -366,7 +366,7 @@
         [(Sequence: ts) (apply sequence/sc (map t->sc ts))]
         [(Vector: t) (vectorof/sc (t->sc/both t))]
         [(HeterogeneousVector: ts) (apply vector/sc (map t->sc/both ts))]
-        [(Box: t) (box/sc (t->sc/both t))]
+        [(Box: t1 t2) (box/sc (t->sc/neg t1) (t->sc t2))]
         [(Pair: t1 t2)
          (cons/sc (t->sc t1) (t->sc t2))]
         [(Async-Channel: t) (async-channel/sc (t->sc t))]

typed-racket-lib/typed-racket/rep/type-rep.rkt

@@ -179,8 +179,8 @@
   [#:fold-rhs (*HeterogeneousVector (map type-rec-id elems))])
 
 ;; elem is a Type
-(def-type Box ([elem Type/c])
-  [#:frees (λ (f) (make-invariant (f elem)))]
+(def-type Box ([elem-w Type/c] [elem-r Type/c])
+  [#:frees (λ (f) (combine-frees (list (flip-variances (f elem-w)) (f elem-r))))]
   [#:key 'box])
 
 ;; elem is a Type

typed-racket-lib/typed-racket/static-contracts/combinators/structural.rkt

@@ -156,7 +156,7 @@
   ((promise/sc (#:covariant)) (λ (x) (and/c (promise/c x) (not/c promise/name?))) #:chaperone)
   ((syntax/sc (#:covariant #:flat)) syntax/c #:flat)
   ((hash/sc (#:invariant #:flat) (#:invariant)) hash/c #:chaperone)
-  ((box/sc (#:invariant)) box/c #:chaperone)
+  ((box/sc (#:contravariant) (#:covariant)) box/c #:chaperone)
   ((parameter/sc (#:contravariant) (#:covariant)) parameter/c #:chaperone)
   ((sequence/sc . (#:covariant)) sequence/c #:impersonator)
   ((channel/sc . (#:invariant)) channel/c #:chaperone)

typed-racket-lib/typed-racket/static-contracts/optimize.rkt

@@ -33,7 +33,7 @@
     ;; can call continuations and thus be useful even if they cannot return values.
     ;[(vectorof/sc: (none/sc:)) empty-vector/sc]
     ;[(vector/sc: sc1 ... (none/sc:) sc2 ...) none/sc]
-    ;[(box/sc: (none/sc:)) none/sc]
+    ;[(box/sc: (none/sc:) (none/sc:)) none/sc]
     ;[(promise/sc: (none/sc:)) none/sc]
     ;[(hash/sc: (none/sc:) value/sc) empty-hash/sc]
     ;[(hash/sc: key/sc (none/sc:)) empty-hash/sc]
@@ -45,7 +45,7 @@
     [(vectorof/sc: (any/sc:)) vector?/sc]
     [(vector/sc: (and scs (any/sc:)) ...) (vector-length/sc (length scs))]
     [(set/sc: (any/sc:)) set?/sc]
-    [(box/sc: (any/sc:)) box?/sc]
+    [(box/sc: (any/sc:) (any/sc:)) box?/sc]
     [(syntax/sc: (any/sc:)) syntax?/sc]
     [(promise/sc: (any/sc:)) promise?/sc]
     [(hash/sc: (any/sc:) (any/sc:)) hash?/sc]

typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt

@@ -394,7 +394,7 @@
                                       (generalize (find-stx-type x #f))))])]
     [(box x)
      (match (and expected (resolve (restrict expected -BoxTop 'orig)))
-       [(Box: t) (-box (check-below (find-stx-type x t) t))]
+       [(Box: t-w t-r) (-box t-w (check-below (find-stx-type x t-r) t-r))]
        [_ (-box (generalize (find-stx-type x)))])]
     [(? hash? h)
      (match (and expected (resolve (restrict expected -HashTop 'orig)))

typed-racket-lib/typed-racket/types/abbrev.rkt

@@ -54,7 +54,7 @@
 (define -App make-App)
 (define -mpair make-MPair)
 (define (-Param t1 [t2 t1]) (make-Param t1 t2))
-(define (-box t) (make-Box t))
+(define (-box t1 [t2 t1]) (make-Box t1 t2))
 (define -channel make-Channel)
 (define -async-channel make-Async-Channel)
 (define -thread-cell make-ThreadCell)

typed-racket-lib/typed-racket/types/printer.rkt

@@ -450,7 +450,7 @@
     [(arr: _ _ _ _ _) `(arr ,(arr->sexp type))]
     [(Vector: e) `(Vectorof ,(t->s e))]
     [(HeterogeneousVector: e) `(Vector ,@(map t->s e))]
-    [(Box: e) `(Boxof ,(t->s e))]
+    [(Box: e e) `(Boxof ,(t->s e))]
     [(Weak-Box: e) `(Weak-Boxof ,(t->s e))]
     [(Future: e) `(Futureof ,(t->s e))]
     [(Channel: e) `(Channelof ,(t->s e))]
@@ -500,7 +500,7 @@
                               (Mu: y (Union: (list (F: x)
                                                    (Pair: (F: x) (F: y)))))
                               (Vector: (F: x))
-                              (Box: (F: x))))))
+                              (Box: (F: x) (F: x))))))
      'Syntax]
     [(Mu-name: name body) `(Rec ,name ,(t->s body))]
     [(B: idx) `(B ,idx)]

typed-racket-lib/typed-racket/types/structural.rkt

@@ -61,7 +61,7 @@
      [Param (#:contra #:co)]
 
      [Continuation-Mark-Keyof (#:inv)]
-     [Box (#:inv)]
+     [Box (#:contra #:co)]
      [Channel (#:inv)]
      [Async-Channel (#:inv)]
      [ThreadCell (#:inv)]

typed-racket-lib/typed-racket/types/subtype.rkt

@@ -531,8 +531,8 @@
          [((Channel: t) (Evt: t*)) (subtype* A0 t t*)]
          [((Async-Channel: t) (Evt: t*)) (subtype* A0 t t*)]
          ;; Invariant types
-         [((Box: s) (Box: t)) (type-equiv? A0 s t)]
-         [((Box: _) (BoxTop:)) A0]
+         [((Box: s-w s-r) (Box: t-w t-r)) (subtypes* A0 (list t-w s-r) (list s-w t-r))]
+         [((Box: _ _) (BoxTop:)) A0]
          [((Weak-Box: s) (Weak-Box: t)) (type-equiv? A0 s t)]
          [((Weak-Box: _) (Weak-BoxTop:)) A0]
          [((ThreadCell: s) (ThreadCell: t)) (type-equiv? A0 s t)]