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

The subject sounds complainy, and so will the rest of this email. So I 
will state up front that I love Typed Racket, and I'm only frustrated 
because I want to love it more.

Also, I apologize for the length of this email, but I have to tell a 
story. Otherwise, I'll get a bunch of "Why don't you try this?" replies, 
which I'll have to answer, leading to an inseparable tangle of ideas. 
How the features and limitations interact is not always obvious.

The features and limitations are:

  1. The reader is set by the #lang line, but not submodule forms.

  2. Implicit argument types in let loops are generalized from the types
     of their initial values.

  3. let: loops require every argument type and the return type to be
     annotated.

  4. TR can't produce contracts for single-arity `case->' types.

  5. Using single-arity `case->' types makes annotating function bodies
     in certain ways impossible.

So here's my user story.

   ********** ONCE UPON A TIME **********

I'm working on `math/matrix'. TR doesn't do generics, which is fine for 
now, but it means a lot of the matrix library's functions have to have 
single-arity types like this:

   (: matrix-hermitian (case-> ((Matrix Real) -> (Matrix Real))
                               ((Matrix Number) -> (Matrix Number))))

It could be (Matrix Number) -> (Matrix Number). But the real matrices 
are closed under almost every matrix operation, so `math/matrix' 
shouldn't make users worry needlessly about complex numbers.

Annotating expressions inside the bodies of functions with single-arity 
`case->' types like that is often impossible, because there's no name 
for polymorphic type arguments (in this case, either `Real' or 
`Number'). To separate the issues from `math/matrix', consider this 
function instead:

   (: repeat+1 (case-> (Index Real -> (Listof Real))
                       (Index Number -> (Listof Number))))
   (define (repeat+1 n num)
     (let loop ([i 0] [acc empty])
       (cond [(< i n)  (loop (+ i 1) (cons (+ num 1) acc))]
             [else  acc])))

It should act like this:

   > (repeat+1 3 10)
   - : (Listof Real)
   '(11 11 11)
   > (repeat+1 0 11+4i)
   - : (Listof Number)
   '()

But it doesn't type:

   Type Checker: Expected (Listof Real), but got (Listof Any) in: acc
   Type Checker: Expected (Listof Number), but got (Listof Any) in: acc

The highlighted expression is the `acc' inside of [else acc]. The 
causes: TR gives the expression `empty' the type (Listof Any) in both 
passes through the function body (one for each case).

The level of inference TR does is generally fine, requiring few 
annotations. The problem here is that *I can't annotate `empty'*. I 
don't have a name for the type argument to `Listof'.

Here's one annotation-less solution:

   (define (repeat+1 n num)
     (cond [(= n 0)  empty]
           [else
            (let loop ([i 1] [acc  (list (+ num 1))])
              (cond [(< i n)  (loop (+ i 1) (cons (+ num 1) acc))]
                    [else  acc]))]))

TR helpfully generalizes the type of (list (+ num 1)) from (List Real) 
to (Listof Real) in the first typechecking pass and from (List Number) 
to (Listof Number) in the second typechecking pass, so `acc' has the 
correct type in both passes.

I committed the off-by-one error [i 0] and the copy error [acc (list 
num)] while deriving that solution. Not liking either kind of error, I 
figure this is safer, and also cleverer:

   (define (repeat+1 n num)
     (let loop ([i 0] [acc  (rest (list num))])
       (cond [(< i n)  (loop (+ i 1) (cons (+ num 1) acc))]
             [else  acc])))

I'm trying to get a properly typed `empty' by taking the rest of a 
one-element list.

I get two type errors like this, highlighting (cons (+ num 1) acc):

   Type Checker: Polymorphic function cons could not be applied to
   arguments:
   Types: a (Listof a) -> (Listof a)
          a b -> (Pairof a b)
   Arguments: Real (Listof Nothing)
   Expected result: (Listof Nothing)

Ah, I see what happened. TR generalized from the type of (rest (list 
num)), which is (Listof Nothing) because (list num) has the type (List 
Real) or (List Number). I need to force it to generalize differently. 
One way to do that is to turn the base case into a call to a polymorphic 
function like `empty-listof':

   (define (repeat+1 n num)
     (let loop ([i 0] [acc  (empty-listof num)])
       (cond [(< i n)  (loop (+ i 1) (cons (+ num 1) acc))]
             [else  acc])))

   (: empty-listof (All (A) (A -> (Listof A))))
   (define (empty-listof x) (rest (list x)))

Basically, `empty-listof' gives me a way to name the type parameter to 
`Listof' in that one expression.

Well, it's either this or the wordier version, and this abstracts a 
little better. So I'll package it up. First, though, I want to make the 
loop faster. It turns out that this:

   [#{i : Nonnegative-Fixnum} 0]

is enough to turn `<' and `+' into `unsafe-fx<' and `unsafe-fx+', and I 
still don't have to annotate `acc' or the loop's return value. Awesome. 
Provide and commit.

Jens Axel reminds me days later that TR can't put a contract on 
`repeat+1'. That shouldn't be too hard to fix, though. I can even use 
submodules to keep everything in one file, containing a typed submodule 
for typed clients and a typed submodule for untyped clients. The latter 
just re-exports `repeat+1' with a type that TR can put a contract on. 
Starting with the module for typed clients:

   (module typed-defs typed/racket
     (provide repeat)

     (: repeat+1 (case-> (Index Real -> (Listof Real))
                         (Index Number -> (Listof Number))))
     (define (repeat+1 n num)
       (let loop ([#{i : Nonnegative-Fixnum} 0] [acc (empty-listof num)])
         (cond [(< i n)  (loop (+ i 1) (cons (+ num 1) acc))]
               [else  acc])))

     (: empty-listof (All (A) (A -> (Listof A))))
     (define (empty-listof x) (rest (list x))))

Oh, no! Submodules don't extend the reader:

   let: bad syntax (not an identifier) in: #(i : Nonnegative-Fixnum)

I'd rather not split this into multiple files. But I can't figure out a 
way to annotate `i' without either annotating `acc' (which I can't do), 
or causing TR to generalize the type of `i' to `Integer' (which defeats 
the optimization).

   ********** THE END **********

There are four more general solutions to the last error. Here they are, 
and their downsides:

  1. Allow submodules to extend the reader.

This seems hard, because module forms are expanded after they've been 
read. One possibility is a #module reader macro. Seems like overkill.

  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.

  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.

I think all of TR's annotating forms should allow any annotation to be 
left out.

  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).

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.

  6. Do generics in TR so single-arity `case->' types are less necessary.

Research topic. Also, it wouldn't solve the problem generally, just 
reduce the number of instances. Single-arity `case->' types will 
probably always be necessary.

Neil ⊥