[racket-dev] TR: Five feature/limitation interactions conspire to drive mad
At Mon, 31 Dec 2012 13:27:50 -0700,
Neil Toronto wrote:
> 1. Allow submodules to extend the reader.
Would using `#lang typed/racket/no-check' instead of `#lang racket' for
the top-level module work? It extends the reader and provides TR's
annotated forms, but otherwise counts as an untyped language.
That's not a general solution, but it may solve your problem.
> 2. Don't generalize argument types in let loops.
>
> This is a bad idea. Often, inferring the types of loops only works
> because of type generalization.
Agreed. Since this one is only a problem because of the other
limitations you list, ideally we should fix the others and leave this
one alone. Do you agree?
> 3. Allow let: loops to have unannotated arguments and return values.
>
> This would totally work. I could use [i : Nonnegative-Fixnum 0] instead
> of [#{i : Nonnegative-Fixnum} 0], and still not have to annotate `acc'
> or the loop's return value.
Trying this one right now.
> I think all of TR's annotating forms should allow any annotation to be
> left out.
I'll look into that next.
> 4. Extend the set of types TR can produce contracts for.
>
> This probably only works for first-order function types. It would be
> helpful, but may not even work for functions with `Array' or `Matrix'
> arguments (they're higher-order).
I can look into making contract generation smarter. Could you send me
a list of types that caused you issues with contract generation?
> There are two more general solutions to the first problem, that
> single-arity `case->' types sometimes make annotating impossible:
>
> 5. Find some way to name the polymorphic arguments in `case->' types.
>
> Yes. This. At least 25% of my time refactoring `math/matrix' has gone to
> writing twisty, annotation-free function bodies.
I agree that this would be useful. Sam, do you think this is doable?
In general, we need a better story for scaling up programming with
intersection types.
Vincent