[racket-dev] Five feature/limitation interactions conspire to drive mad

On 01/01/2013 03:35 PM, Matthias Felleisen wrote:
>
> Neil,
>
> thanks for the user story. We should hear more of those for all kinds of corners in our world.

You're welcome!

> Question: did you start the math library in an untyped form (and switch) or did you go with types from the get-go?

It's all been in Typed Racket from the beginning. This was initially 
because I mostly had floating-point functions planned, and I wanted TR's 
help proving that I never used non-flonums by mistake. Also, I wanted 
the special functions to have performance competitive with C 
implementations.

When I decided to do arrays, Typed Racket was again the natural choice. 
First, because it's not possible to use `require/typed' to import 
polymorphic struct types. Second, because it allowed me to avoid a lot 
of runtime checks.

I discovered reasons #3 and #4 while I was writing `math/array':

3. Passing around higher-order functions can get confusing. I can't 
speak for anyone else, but when I get something like `array-axis-reduce' 
- which is like a fold but with complicated types - to pass the type 
checker, my code is usually correct.

4. TR's types for Racket's numeric tower, especially the additional 
`Index' type, makes it easy to safely use unsafe indexing. Throughout 
`math/array', values of type `Index' are always either a size (e.g. a 
vector length) or an index that has been proved to be less than a size. 
IOW, if I can get TR to prove j : Index, I'm satisfied that 
(unsafe-vector-ref xs j) is actually safe. Also, if `j' is a loop 
counter, TR can usually compare and increment using unsafe fixnum ops.

There are a bunch of other little things that are like #4 (which is only 
a big thing because indexes are so prevalent in `math/array'). Maybe 
I'll collect those into a separate user story.

Neil ⊥