[racket] typing a function

On 11/19/2012 04:43 AM, Pierpaolo Bernardi wrote:
> #lang typed/racket
>
> (define-type (Array a) (Rec AA (U (Vectorof a) (Vectorof AA))))
>
> (: make-array (All (a) ((Listof Positive-Index) a -> (Array a))))
>
> (define (make-array dims init)
>    (let loop ((dims dims))
>      (match dims
>        ((list first)
>         (make-vector first init))
>        ((list-rest first rest)
>         (let ((v (make-vector first)))
>           (for ((i (in-range first)))
>             (vector-set! v i (loop rest)))
>           v)))))

When `make-vector' is given one argument, it constructs a (Vectorof 
Integer), namely #(0 0 0 ...). In this case you need to construct it 
with the type (Vectorof (Array a)).

This works for me, on 5.3.1:

   (let: ((v : (Vectorof (Array a)) (make-vector first (vector init))))
     ...)

Also, you should know that with a recursive type like that, you'll often 
have a hard time convincing TR that you're dealing with a base case in a 
particular loop iteration. You may end up passing predicates around to 
identify instances of the type `a'.

If you want to know whether you'll have trouble, try writing 
`array-flatten', with this type:

   (All (a) ((Array a) -> (Vectorof a)))

If you can't, try this type:

   (All (a) ((Array a) (Any -> Boolean : a) -> (Vectorof a)))

which is for an `array-flatten' that additionally accepts a predicate as 
an argument.

Neil ⊥