# [racket] typing a function

 From: Neil Toronto (neil.toronto at gmail.com) Date: Mon Nov 19 11:58:15 EST 2012 Previous message: [racket] typing a function Next message: [racket] typing a function Messages sorted by: [date] [thread] [subject] [author]

```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 ⊥

```

 Posted on the users mailing list. Previous message: [racket] typing a function Next message: [racket] typing a function Messages sorted by: [date] [thread] [subject] [author]