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 ⊥

_________________________
 Racket Developers list:
 http://lists.racket-lang.org/dev

Reply via email to