[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



Posted on the users mailing list.