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