[racket] problem (?) with typed racket

From: Jose A. Ortega Ruiz (jao at gnu.org)
Date: Mon Jul 5 10:09:02 EDT 2010

On Mon, Jul 05 2010, Noel Welsh wrote:

> This type checks for me:
>  (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 : E)) ((Arrow-arrow a) (car ((Arrow-arrow b) e))))))

Ah, much better! I was under the false impression that the type variable
E wasn't visible inside the `define' body; the reason is that, as a
matter of fact, it doesn't seem to be visible when one's defining a
variable which is not a procedure. For instance, adding to the above the
following struct definition:

  (define-struct: (A) C
    ([compose : (A A -> A)]))

the following procedure type-checks just fine:

  (: make-CArrow (All (E) (-> (C (Arrow E)))))
  (define (make-CArrow)
    (C #{compose-arrows :: ((Arrow E) (Arrow E) -> (Arrow E))}))

but, if we want to define a non-procedural value in an analogous fashion:

  (: carrow (All (E) (C (Arrow E))))
  (define carrow
    (C #{compose-arrows :: ((Arrow E) (Arrow E) -> (Arrow E))}))

the type checker complains that E is an unbound type name, for all
occurrences of E inside the define form.

Perhaps i am missing something again?

Children enter school as question marks and leave as periods.
 -Neil Postman, professor and author (1931- )

Posted on the users mailing list.