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

From: Vincent St-Amour (stamourv at ccs.neu.edu)
Date: Mon Dec 31 16:56:51 EST 2012

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

Posted on the dev mailing list.