[racket] type of make-vector

From: Vincent St-Amour (stamourv at ccs.neu.edu)
Date: Wed Jun 18 21:23:45 EDT 2014

At Wed, 18 Jun 2014 01:45:08 -0400,
Alexander D. Knauth wrote:
> >> And Is there a reason for the result in the first case being (Vectorof
> >> (U Integer a)) instead of (Vectorof Zero)?
> > 
> > Again, convenience.
> > 
> > Because vectors are mutable, a `(Vectorof Zero)' is not very useful. You
> > can only put zeros in it. In this case, TR generalizes the type to
> > `(Vectorof Integer)', which is more generally useful.
> 
> I keep forgetting that vectors are mutable, even when I’m mutating them.  
> So (Vectorof Zero) would be pretty useless.  
> 
> However, wouldn’t (Vectorof (U Zero a)) be more useful than (Vectorof
> (U Integer a))?
> 
> Otherwise the type of ((inst make-vector Natural) 10) would be
> (Vectorof Integer), not (Vectorof Natural), right?

Good point. I'll give it a try.

Thanks for the report!

Vincent


Posted on the users mailing list.