[racket] Typed Racket reactions on developing polymorphic typed array library, and questions

At Sun, 22 Aug 2010 21:31:09 -0700,
Neil Toronto wrote:
> Vincent will be happy to know that all the flonum and fixnum ops are 
> changed by TR's optimizer to be unsafe. (Except a certain add1 that TR 
> can't prove doesn't overflow; I can prove it, so I changed it
> myself.)

I am indeed happy. I'm pleasantly surprised about the fixnum part,
since we can only optimize these in limited circumstances.

Was simply adding types enough to trigger all these optimizations, or
did you need to do a bit of extra work (except for that add1 case)?

>  From my admittedly limited tests, I'd say that this particular forall 
> gets within spitting distance of equivalent C code. ("Spitting distance" 
> is a technical term meaning "within 3x to 5x time elapsed".) There's a 
> "foralln!:" that destructively updates arrays, which might get a little 
> closer; perhaps it gets within pinching distance of the C equivalent's 
> buttocks.

That's impressive! If you get around to do precise measurements, I'm
really interested in the results.

>   - Indentation is in a rather evil state in TR. Could DrRacket have 
> more than one regexp for each "*-like keyword"? That would make it 
> easier to auto-indent TR's built-in loop syntax, or any other syntax 
> (like forall) that is in a state of flux. The indentation rules for 
> for/*: loops could be tricky because of the required "return" type - but 
> see the next item.

That would indeed be nice. I'll see what I can do.

>   - Why require "return" or body types for for/*: loops in TR? I haven't 
> needed them in forall/*: loops. Also, writing the "Listof" in "for/list: 
> : (Listof T)" is annoying. I know it's a list from reading "for/list:", 
> and for/list: knows it, too. I also know the return type of a 
> "for/fold:" from the accumulators' types; why require them twice? I'm 
> also annoyed by having to give a body type for every named "let:".

As Sam answered, we need at least some type information because the
expanded versions of the for: macros need it to typecheck.

However, you're right that the return type of a for/list: will always
be a list, making the Listof redundant. This is even more true of
for/fold:, and it annoys me too. In the case of for/fold:, it
shouldn't be a problem since the types of the accumulators tell us all
we need. I'll look into that.

But, in the case of for/list:, for/vector: and others, we would still
need an annotation to know the type of the elements of the resulting
list, vector, etc. We could remove the Listof, Vectorof and co from
the annotation, but that could lead to some ambiguity while reading
code.

For example, assuming we get annotate only the type of the elements of
the result sequence:

(for/list: : (Listof Integer) ...)

At first glance, what does this return? A list of integers, or a list
of lists of integers? It may be confusing.

>   - I've found it useful to have a macro shaped like (with-refine* ([x 
> pred?] ...) body ...). I have a lot of functions that take Integer and 
> (Listof Integer) arguments, but actually operate only on 
> Nonnegative-Fixnum indexes. (Nonnegativity and fixnum-ness are hard for 
> TR to prove.) The function bodies are wrapped with this macro.

Having an assert* macro that would do something like that would be
useful to have in the core. Could you send me your with-refine* macro
so that I can include it in TR?

Vincent