[racket] type of make-vector

On Jun 17, 2014, at 8:21 PM, Vincent St-Amour <stamourv at ccs.neu.edu> wrote:

> At Tue, 17 Jun 2014 19:40:44 -0400,
> Alexander D. Knauth wrote:
>> 
>> The type of make-vector appears to be this:
>>> make-vector
>> - : (All (a)
>>      (case->
>>       (-> Integer (Vectorof (U Integer a)))
>>       (-> Integer a (Vectorof a))))
>> #<procedure:make-vector>
>> 
>> Is there a reason for the first argument being Integer instead of Natural?  
> 
> Convenience for users. It's much easier to get something to typecheck as
> Integer than as Natural.

That makes sense.  It would be a bit of a pain to put (cast ... Index) everywhere.  

> 
> As with most things in language / type system design, it's a
> tradeoff. The type system may catch more bugs if it required vector
> indices to be `Natural's (and even more if it required `Index'es) at the
> cost of ruling out (or requiring extra runtime checks for) more valid
> programs.
> 
> Section 6.2 of our paper on the design of TR's numeric tower discusses
> this tradeoff.
>    http://www.ccs.neu.edu/home/stamourv/papers/numeric-tower.pdf
> 
> As the paper explains, you can write a wrapper that only accepts
> `Natural's if you want to enforce this restriction.
> 
> 
>> 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?  

> 
> Section 6.1 of the paper discusses this other tradeoff.
> 
> You may also find the rest of the paper interesting, as it discusses
> other aspects of TR's design.

It was very interesting and helped me understand a lot of things, so thank you.  

> 
> Vincent