[racket] type of make-vector
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