add separate read and write types for Box types

typed-racket-doc/typed-racket/scribblings/reference/types.scrbl

@@ -360,10 +360,48 @@ corresponding to @racket[trest], where @racket[bound]
 @ex[(lambda: ([x : Any]) (if (mpair? x) x (error "not an mpair!")))]
 }
 
-@defform[(Boxof t)]{A @rtech{box} of @racket[t]}
+@defform*[[(Boxof t)
+           (Boxof write-t read-t)]]{
+  The first form is a @rtech{box} of @racket[t].
+
+  The second form is a @rtech{box} that supports write operations like
+  @racket[set-box!] taking @racket[write-t], and read operations like
+  @racket[unbox] returning @racket[read-t]. For this type to make sense,
+  @racket[write-t] should be a subtype of @racket[read-t]. This form can
+  be used to restrict writing to the box, or to safely express uncertainty
+  about the values other code could put in the box.
+}
 
 @ex[(box "hello world")]
 
+@defform[(Boxof/Read t)]{
+  A @rtech{box} of @racket[t] that only supports read-only operations
+  such as @racket[unbox]. A @racket[(Boxof/Read a)] is a subtype of
+  @racket[(Boxof/Read b)] if @racket[a] is a subtype of @racket[b].
+
+  A @racket[(Boxof/Read t)] is a supertype of @racket[(Boxof t)], so
+  any @racket[(Boxof t)] can be used as a @racket[(Boxof/Read t)], but
+  but not the other way around. It is equivalent to
+  @racket[(Boxof Nothing t)].}
+
+@ex[(box-immutable "hello world")
+    (code:comment "though this does not necessarily imply immutability:")
+    (define b : (Boxof Integer) (box 3))
+    (define b-read-only : (Boxof/Read Integer) b)
+    (eval:error (set-box! b-read-only 5))
+    (unbox b-read-only)
+    (set-box! b 5)
+    (unbox b-read-only)]
+
+@defform[(Boxof/Write t)]{
+  A @rtech{box} that could contain anything, but can only take
+  @racket[t] for write operations such as @racket[set-box!].
+
+  A @racket[(Boxof/Write t)] is a supertype of @racket[(Boxof t)], so
+  a @racket[(Boxof t)] can be used as a @racket[(Boxof/Write t)], but
+  but not the other way around. It is equivalent to
+  @racket[(Boxof t Any)].}
+
 @defidform[BoxTop]{is the type of a @rtech{box} with an unknown element
   type and is the supertype of all box types. Only read-only box operations
   (e.g. @racket[unbox]) are allowed on values of this type. This type

typed-racket-lib/typed-racket/base-env/base-env.rkt

@@ -21,7 +21,7 @@
  "base-structs.rkt"
  racket/file
  (only-in racket/private/pre-base new-apply-proc)
- (only-in (types abbrev) [-Boolean B] [-Symbol Sym] -Flat)
+ (only-in (types abbrev) [-Boolean B] [-Symbol Sym] -Flat -Boxof/Read -Boxof/Write)
  (only-in (types numeric-tower) [-Number N])
  (only-in (rep type-rep values-rep object-rep)
           -car
@@ -902,18 +902,18 @@
 [box (-poly (a) (a . -> . (-box a)))]
 [box-immutable (-poly (a) (a . -> . (-box a)))]
 [unbox (-poly (a) (cl->*
-                   ((-box a) . -> . a)
+                   ((-Boxof/Read a) . -> . a)
                    (-BoxTop . -> . Univ)))]
-[set-box! (-poly (a) ((-box a) a . -> . -Void))]
+[set-box! (-poly (a) ((-Boxof/Write a) a . -> . -Void))]
 [box-cas! (-poly (a) ((-box a) a a . -> . -Boolean))]
 [unsafe-unbox (-poly (a) (cl->*
-                          ((-box a) . -> . a)
+                          ((-Boxof/Read a) . -> . a)
                           (-BoxTop . -> . Univ)))]
-[unsafe-set-box! (-poly (a) ((-box a) a . -> . -Void))]
+[unsafe-set-box! (-poly (a) ((-Boxof/Write a) a . -> . -Void))]
 [unsafe-unbox* (-poly (a) (cl->*
-                           ((-box a) . -> . a)
+                           ((-Boxof/Read a) . -> . a)
                            (-BoxTop . -> . Univ)))]
-[unsafe-set-box*! (-poly (a) ((-box a) a . -> . -Void))]
+[unsafe-set-box*! (-poly (a) ((-Boxof/Write a) a . -> . -Void))]
 [unsafe-box*-cas! (-poly (a) ((-box a) a a . -> . -Boolean))]
 [box? (make-pred-ty -BoxTop)]
 

typed-racket-lib/typed-racket/base-env/base-types-extra.rkt

@@ -19,7 +19,7 @@
 
 ;; special type names that are not bound to particular types
 (define-other-types
-  -> ->* case-> U Union ∩ Intersection Rec All Opaque Vector
+  -> ->* case-> U Union ∩ Intersection Rec All Opaque Vector Boxof
   Parameterof List List* Class Object Row Unit Values AnyValues Instance Refinement
   pred Struct Struct-Type Prefab PrefabTop Distinction Sequenceof Refine)
 

typed-racket-lib/typed-racket/base-env/base-types.rkt

@@ -183,7 +183,9 @@
 [HashTable (-poly (a b) (Un (-Mutable-HT a b) (-Immutable-HT a b) (-Weak-HT a b)))]
 [Promise (-poly (a) (-Promise a))]
 [Pair (-poly (a b) (-pair a b))]
-[Boxof (-poly (a) (make-Box a))]
+;; Boxof is implemented as a special form in base-types-extra and parse-type
+[Boxof/Read (-poly (r) (-Boxof/Read r))]
+[Boxof/Write (-poly (w) (-Boxof/Write w))]
 [Weak-Boxof (-poly (a) (-weak-box a))]
 [Channelof (-poly (a) (make-Channel a))]
 [Async-Channelof (-poly (a) (make-Async-Channel a))]

typed-racket-lib/typed-racket/env/init-envs.rkt

@@ -118,8 +118,8 @@
      `(make-Vector ,(type->sexp ty))]
     [(HeterogeneousVector: elems)
      `(-vec* ,@(map type->sexp elems))]
-    [(Box: ty)
-     `(make-Box ,(type->sexp ty))]
+    [(Box: ty-w ty-r)
+     `(make-Box ,(type->sexp ty-w) ,(type->sexp ty-r))]
     [(Channel: ty)
      `(make-Channel ,(type->sexp ty))]
     [(Async-Channel: ty)

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

@@ -736,9 +736,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/parse-type.rkt

@@ -132,6 +132,7 @@
 (define-literal-syntax-class #:for-label Union)
 (define-literal-syntax-class #:for-label All)
 (define-literal-syntax-class #:for-label Opaque)
+(define-literal-syntax-class #:for-label Boxof)
 (define-literal-syntax-class #:for-label Parameter)
 (define-literal-syntax-class #:for-label Vector)
 (define-literal-syntax-class #:for-label Struct)
@@ -764,6 +765,15 @@
        (make-Opaque #'p?)]
       [(:Distinction^ name:id unique-id:id rep-ty:expr)
        (-Distinction (syntax-e #'name) (syntax-e #'unique-id) (parse-type #'rep-ty))]
+      [(:Boxof^ t)
+       (-box (parse-type #'t))]
+      [(:Boxof^ w r)
+       (-box (parse-type #'w) (parse-type #'r))]
+      [((~and b :Boxof^) args ...)
+       (parse-error
+        #:stx stx
+        (~a (syntax-e #'b) " expects one or two type arguments, given "
+            (sub1 (length (syntax->list #'(args ...))))))]
       [(:Parameter^ t)
        (let ([ty (parse-type #'t)])
          (-Param ty ty))]

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

@@ -534,7 +534,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

@@ -242,7 +242,7 @@
   [#:mask mask:box]
   [#:singleton -BoxTop])
 
-(def-structural Box ([elem #:invariant])
+(def-structural Box ([elem-w #:contravariant] [elem-r #:covariant])
   [#:mask mask:box])
 
 ;;----------

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

@@ -164,7 +164,7 @@
   ((mutable-hash/sc (#:invariant) (#:invariant)) mutable-hash/c #:chaperone)
   ((immutable-hash/sc (#:covariant) (#:covariant)) immutable-hash/c #:flat)
   ((weak-hash/sc (#:invariant) (#:invariant)) weak-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

@@ -32,7 +32,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]
@@ -44,7 +44,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]
@@ -213,7 +213,7 @@
    [(or (->/sc: _ _ _ _ _ _)
         (arr/sc: _ _ _)
         (async-channel/sc: _)
-        (box/sc: _)
+        (box/sc: _ _)
         (channel/sc: _)
         (cons/sc: _ _)
         (continuation-mark-key/sc: _)

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

@@ -438,7 +438,7 @@
                                       (generalize (find-stx-type x #f))))])]
     [(box x)
      (match (and expected-type (resolve (intersect expected-type -BoxTop)))
-       [(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? hash-val) (tc-hash find-stx-type hash-val expected-type)]
     [(? prefab-struct-key prefab-val) (tc-prefab find-stx-type prefab-val expected-type)]

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

@@ -30,7 +30,9 @@
 (define -App make-App)
 (define -mpair make-MPair)
 (define (-Param t1 [t2 t1]) (make-Param t1 t2))
-(define -box make-Box)
+(define (-box t1 [t2 t1]) (make-Box t1 t2))
+(define (-Boxof/Read t) (-box -Bottom t))
+(define (-Boxof/Write t) (-box t Univ))
 (define -channel make-Channel)
 (define -async-channel make-Async-Channel)
 (define -thread-cell make-ThreadCell)
@@ -96,7 +98,7 @@
   (-mu e
        (Un -Null -Boolean -Symbol -String -Keyword -Char -Number
            (make-Vector (-Syntax e))
-           (make-Box (-Syntax e))
+           (-box (-Syntax e))
            (make-Listof (-Syntax e))
            (-pair (-Syntax e) (-Syntax e)))))
 (define/decl Any-Syntax (-Syntax In-Syntax))
@@ -107,7 +109,7 @@
            -Number -Boolean -Symbol -String -Keyword -Char
            (-pair sexp sexp)
            (make-Vector sexp)
-           (make-Box sexp)
+           (-box sexp)
            t)))
 (define/decl -Flat
   (-mu flat

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

@@ -652,7 +652,10 @@
     [(? Arrow?) `(Arrow ,(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))]
+    [(Box: (Bottom:) e) `(Boxof/Read ,(t->s e))]
+    [(Box: e (Univ:)) `(Boxof/Write ,(t->s e))]
+    [(Box: e1 e2) `(Boxof ,(t->s e1) ,(t->s e2))]
     [(Weak-Box: e) `(Weak-Boxof ,(t->s e))]
     [(Future: e) `(Futureof ,(t->s e))]
     [(Channel: e) `(Channelof ,(t->s e))]

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

@@ -647,10 +647,13 @@
                   ([b (in-list (BaseUnion-bases t1))]
                    #:break (not A))
           (subtype* A b t2 obj))])]
-  [(case: Box (Box: elem1))
+  [(case: Box (Box: elem1-w elem1-r))
    (match t2
      [(? BoxTop?) A]
-     [(Box: elem2) (type≡? A elem1 elem2)]
+     [(Box: elem2-w elem2-r)
+      (subtype-seq A
+                   (subtype* elem2-w elem1-w)
+                   (subtype* elem1-r elem2-r))]
      [_ (continue<: A t1 t2 obj)])]
   [(case: Channel (Channel: elem1))
    (match t2

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

@@ -4,6 +4,7 @@
          (rep type-rep rep-utils)
          (prefix-in c: (contract-req))
          (types subtype base-abbrev resolve current-seen)
+         (only-in (infer infer) intersect)
          racket/match
          racket/list)
 
@@ -30,6 +31,13 @@
     (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 ...))
+          (cons (make-Box (intersect a-w b-w) (union a-r b-r)) bs)])]
       [else (cons t (filter-not (λ (ts-elem) (subtype ts-elem t)) ts))])))
 
 ;; Recursively reduce unions so that they do not contain

typed-racket-test/succeed/pr225-box-immutable.rkt

@@ -0,0 +1,12 @@
+#lang typed/racket
+
+;; box-immutable should not break programs that use Boxof
+
+(define b (box-immutable 5))
+
+(: f : (Boxof Integer) -> Integer)
+(define (f b)
+  (unbox b))
+
+(f b)
+

typed-racket-test/unit-tests/infer-tests.rkt

@@ -98,8 +98,8 @@
    (pd-t (-vec (-lst (-v a))) (a) (-vec -Bottom) (-vec Univ))
    (pd-t (-vec (-v a)) (b) (-vec (-v a)) (-vec (-v a)))
 
-   (pd-t (-box (-v a)) (a) (-box -Bottom) (-box Univ))
-   (pd-t (-box (-lst (-v a))) (a) (-box -Bottom) (-box Univ))
+   (pd-t (-box (-v a)) (a) (-box Univ -Bottom) (-box -Bottom Univ))
+   (pd-t (-box (-lst (-v a))) (a) (-box (-lst Univ) (-lst -Bottom)) (-box (-lst -Bottom) (-lst Univ)))
    (pd-t (-box (-v a)) (b) (-box (-v a)) (-box (-v a)))
 
    (pd-t (-channel (-v a)) (a) (-channel -Bottom) (-channel Univ))

typed-racket-test/unit-tests/init-env-tests.rkt

@@ -38,7 +38,10 @@
         '(make-Path (list -car) (cons 0 0)))
       (check-equal?
         (convert-type (-mu x (-lst* Univ (-box x))))
-        '(make-Mu 'x (make-Pair Univ (make-Pair (make-Box (make-F 'x)) -Null))))
+        '(make-Mu 'x
+                  (make-Pair Univ
+                             (make-Pair (make-Box (make-F 'x) (make-F 'x))
+                                        -Null))))
       (check-equal?
         (convert-type -StructTypeTop)
         '-StructTypeTop)