Re: [racket] type of make-vector

2014-06-18 Thread Vincent St-Amour
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 >

Re: [racket] type of make-vector

2014-06-17 Thread Alexander D. Knauth
On Jun 17, 2014, at 8:21 PM, Vincent St-Amour 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 (Vector

Re: [racket] type of make-vector

2014-06-17 Thread Vincent St-Amour
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 > # > > Is there a reason for the first argument bein

[racket] type of make-vector

2014-06-17 Thread Alexander D. Knauth
The type of make-vector appears to be this: > make-vector - : (All (a) (case-> (-> Integer (Vectorof (U Integer a))) (-> Integer a (Vectorof a # Is there a reason for the first argument being Integer instead of Natural? And Is there a reason for the result in the first c