[racket] typing a function

On 11/22/2012 07:41 AM, Pierpaolo Bernardi wrote:
> OK, I think I'm not smart enough for TR.

One of my rules is "Never let the computer make you feel stupid." It's 
the computers that are dumb, not the people.

> What's wrong in the following?
> ========
> #lang typed/racket
>
> (define-type Array2 (Vectorof (Vectorof Number)))
>
> (: make-array (Positive-Index Positive-Index -> Array2))
>
> (define (make-array xdim ydim)
>    (for/vector: : Array2 ((i : Positive-Index (in-range xdim)))
>      (make-vector ydim 0)))

With a few tweaks, it works in 5.3.1. It *will not work* in 5.3, because 
we hadn't fixed `for/vector:' yet.

(See? The computer is stupid. It didn't fix the problem for us. :D)


#lang typed/racket

(define-type Array2 (Vectorof (Vectorof Number)))

(: make-array (Positive-Index Positive-Index -> Array2))
(define (make-array xdim ydim)
   (for/vector: : Array2 ((i (in-range xdim)))
     (ann (make-vector ydim 0) (Vectorof Number))))


Here, `ann' means "annotate this expression with this type".

Probably the main trick in working with TR is knowing how and when to 
help it figure out expressions' types. I've learned to avoid giving loop 
variables types, for example. Doing so requires guessing what the 
`in-range' macro expands to. (FWIW, in this case, Nonnegative-Fixnum is 
the most restricted type `i' can have.)

In general, TR has a hard time inferring vector types, because vectors 
are mutable, which means subtyping doesn't work on them. That is, if 
"<:" means "is a subtype of", then this is true:

   (Listof Byte) <: (Listof Integer)

because lists are immutable, but this is NOT true:

   (Vectorof Byte) <: (Vectorof Integer)

In your example program, I've had to tell TR that it's making a vector 
of Number. It had assumed that (make-vector ydim 0) was making a vector 
of Integer, which is not a vector of Number.

One extra thing `for/vector:' has in 5.3.1 is body annotations, and 
using it makes the extra annotation unnecessary:

   (for/vector: ((i  (in-range xdim))) : (Vectorof Number)
     (make-vector ydim 0))

It works because this use of `for/vector:' expands to something that 
annotates the body (make-vector ydim 0) for you.

(Sam and Vincent: this is a nice example of why body annotations are 
better. :D)

To sum up: upgrade, because we made the computer less stupid in 5.3.1, 
and learn a few rules of thumb about when and how to annotate. You're 
doing fine.

One more thing. Are you writing an array library for your own use, or as 
an exercise? The next Racket release will have an array data type.

Neil ⊥