[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