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

Neil, 

thanks for the user story. We should hear more of those for all kinds of corners in our world. 

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

-- Matthias



On Dec 31, 2012, at 3:27 PM, Neil Toronto wrote:

> 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 ⊥
> _________________________
> Racket Developers list:
> http://lists.racket-lang.org/dev