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