[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 ⊥