add Boxof/Read, Boxof/Write, and Boxof/Write-Read

Author: AlexKnauth

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

@@ -354,6 +354,41 @@ corresponding to @racket[trest], where @racket[bound]
 
 @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 t)] is a subtype of
+  @racket[(Boxof t)], and a @racket[(Boxof/Read a)] is a subtype of
+  @racket[(Boxof/Read b)] if @racket[a] is a subtype of @racket[b]. It
+  is equivalent to @racket[(Boxof/Write-Read 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)
+    (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)], and
+  it is equivalent to @racket[(Boxof/Write-Read t Any)].}
+
+@defform[(Boxof/Write-Read write-t read-t)]{
+  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].
+
+  The type @racket[(Boxof t)] is equivalent to
+  @racket[(Boxof/Write-Read t t)], the type
+  @racket[(Boxof/Read t)] is equivalent to
+  @racket[(Boxof/Write-Read Nothing t)], and the type
+  @racket[(Boxof/Write t)] is equivalent to
+  @racket[(Boxof/Write-Read 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)
           make-ClassTop
@@ -866,19 +866,19 @@
 
 ;; Section 4.12 (Boxes)
 [box (-poly (a) (a . -> . (-box a)))]
-[box-immutable (-poly (a) (a . -> . (-box a)))]
+[box-immutable (-poly (a) (a . -> . (-Boxof/Read a)))]
 [unbox (-poly (a) (cl->*
-                   ((-box a) . -> . a)
+                   ((-Boxof/Read a) . -> . a)
                    ((make-BoxTop) . -> . Univ)))]
-[set-box! (-poly (a) ((-box a) a . -> . -Void))]
+[set-box! (-poly (a) ((-Boxof/Write a) a . -> . -Void))]
 [unsafe-unbox (-poly (a) (cl->*
-                          ((-box a) . -> . a)
+                          ((-Boxof/Read a) . -> . a)
                           ((make-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)
                            ((make-BoxTop) . -> . Univ)))]
-[unsafe-set-box*! (-poly (a) ((-box a) a . -> . -Void))]
+[unsafe-set-box*! (-poly (a) ((-Boxof/Write a) a . -> . -Void))]
 [box? (make-pred-ty (make-BoxTop))]
 
 ;; Section 4.13 (Hash Tables)

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

@@ -172,6 +172,9 @@
 [Promise (-poly (a) (-Promise a))]
 [Pair (-poly (a b) (-pair a b))]
 [Boxof (-poly (a) (-box a))]
+[Boxof/Read (-poly (r) (-Boxof/Read r))]
+[Boxof/Write (-poly (w) (-Boxof/Write w))]
+[Boxof/Write-Read (-poly (w r) (-box w r))]
 [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/types/abbrev.rkt

@@ -55,6 +55,8 @@
 (define -mpair make-MPair)
 (define (-Param t1 [t2 t1]) (make-Param t1 t2))
 (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)

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

@@ -451,6 +451,9 @@
     [(Vector: e) `(Vectorof ,(t->s e))]
     [(HeterogeneousVector: e) `(Vector ,@(map t->s e))]
     [(Box: e e) `(Boxof ,(t->s e))]
+    [(Box: (Union: '()) e) `(Boxof/Read ,(t->s e))]
+    [(Box: e (Univ:)) `(Boxof/Write ,(t->s e))]
+    [(Box: e1 e2) `(Boxof/Write-Read ,(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))]