[racket] type of make-vector

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.

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.

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.

Vincent