add Read-Only-Boxof

Author: AlexKnauth

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

@@ -354,6 +354,12 @@ corresponding to @racket[trest], where @racket[bound]
 
 @ex[(box "hello world")]
 
+@defform[(Read-Only-Boxof t)]{A read-only @rtech{box} of @racket[t].}
+
+@ex[(box-immutable "hello world")
+    (code:comment "though this does not necessarily imply immutability:")
+    (if (zero? (random 2)) (box "hello") (box 'hello))]
+
 @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 -Read-Only-Boxof)
  (only-in (types numeric-tower) [-Number N])
  (only-in (rep type-rep)
           make-ClassTop
@@ -866,7 +866,7 @@
 
 ;; Section 4.12 (Boxes)
 [box (-poly (a) (a . -> . (-box a)))]
-[box-immutable (-poly (a) (a . -> . (-box a)))]
+[box-immutable (-poly (a) (a . -> . (-Read-Only-Boxof a)))]
 [unbox (-poly (a) (cl->*
                    ((-box a) . -> . a)
                    ((make-BoxTop) . -> . Univ)))]

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

@@ -172,6 +172,7 @@
 [Promise (-poly (a) (-Promise a))]
 [Pair (-poly (a b) (-pair a b))]
 [Boxof (-poly (a) (-box a))]
+[Read-Only-Boxof (-poly (a) (-Read-Only-Boxof a))]
 [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,7 @@
 (define -mpair make-MPair)
 (define (-Param t1 [t2 t1]) (make-Param t1 t2))
 (define (-box t1 [t2 t1]) (make-Box t1 t2))
+(define (-Read-Only-Boxof t) (-box -Bottom t))
 (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,7 @@
     [(Vector: e) `(Vectorof ,(t->s e))]
     [(HeterogeneousVector: e) `(Vector ,@(map t->s e))]
     [(Box: e e) `(Boxof ,(t->s e))]
+    [(Box: (Union: '()) e) `(Read-Only-Boxof ,(t->s e))]
     [(Weak-Box: e) `(Weak-Boxof ,(t->s e))]
     [(Future: e) `(Futureof ,(t->s e))]
     [(Channel: e) `(Channelof ,(t->s e))]