# [racket-dev] A Const type constructor

After thinking about it, I don't want an Immutable-Vector type, for
which v : Immutable-Vector proves (immutable? v) is #t. That would be
seriously annoying to users of a vector library.
What if TR had a notion of const-ness, like in C? Suppose (Vectorof A)
is a subtype of (Const-Vectorof B) when A is a subtype of B, and
(Const-Vectorof A) is never a subtype of (Vectorof B).
Then I could tell TR that my functions *can't use the possibly mutable
vectors they get as a communication channel*. For example:
vector+ : (Const-Vectorof Number) (Const-Vectorof Number)
-> (Vectorof Number)
Then (vector+ xs ys) would type if `xs' and `ys' were any kind of vector
of numbers, immutable or not.
It could be made more general, with Const as a type constructor:
vector+ : (Const (Vectorof Number)) (Const (Vectorof Number))
-> (Vectorof Number)
Also,
vector-ref : All (a) ((Const (Vectorof a)) Integer -> a)
vector-set! : All (a) ((Vectorof a) Integer a -> Void)
vector : All (a) (a * -> (Vectorof a)
vector-immutable : All (a) (a * -> (Const (Vectorof a))
bytes-ref : (Const Bytes) Integer -> Byte
bytes-set! : Bytes Integer Integer -> Void
(Const A) = A for Const A (e.g. Number, (Const (Vectorof B)))
(struct: (a) const-wrap ([data : (Const (Vectorof a))]))
(Const (const-wrap A)) = (const-wrap A)
(struct: (a) wrap ([data : (Vectorof a)]))
If v : (Const (wrap A)) then (wrap-data v) : (Const (Vectorof a))
(Const (Vectorof (Vectorof a)))
= (Const (Vectorof (Const (Vectorof a))))
Would this work? Am I thinking about it correctly in the first place?
Neil ⊥