[racket] problem (?) with typed racket
From: Jose A. Ortega Ruiz (jao at gnu.org)
Date: Mon Jul 5 07:19:43 EDT 2010 |
|
Hi,
The following (contrived) typed/racket program doesn't typecheck:
(define-struct: (E) Arrow
([arrow : (E -> (Listof E))]))
(: compose-arrows (All (E) ((Arrow E) (Arrow E) -> (Arrow E))))
(define (compose-arrows a b)
(Arrow (lambda (e) ((Arrow-arrow a) (car ((Arrow-arrow b) e))))))
The typechecker complains about `compose-arrows':
Type Checker: Expected E, but got Any in: e
(pointing to the lambda inside `compose-arrows' above). I can circumvent
the problem giving an explicit type to that lambda:
(define (compose-arrows a b)
(let: ([cmp : (All (E) ((Arrow E) (Arrow E) -> (E -> (Listof E))))
(lambda (a b)
(lambda (e) ((Arrow-arrow a) (car ((Arrow-arrow b) e)))))])
(Arrow (cmp a b))))
but this feels a bit verbose, compared to the original definition above.
(I've tried other combinations using `define:', but the problem is
always unifying all occurences of the type parameter 'E'.)
Is the failure to type check a genuine limitation of the type inference
engine, or is it me expecting too much from type inference in general?
And, is there a more compact way of indicating the type of that lambda?
TIA,
jao