[racket] problem (?) with typed racket

On Jul 5, 2010, at 7:19 AM, Jose A. Ortega Ruiz wrote:

> 
> 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))))))

As Noel points out, all that's missing is a type declaration for 
the parameter e in the lambda: 

 (lambda ({e : E}) ...)

will do the trick. 

Why? TR does not infer types. It checks them. When a type declaration
is missing, TR assumes that e is of type TheRacketType, aka Any. For 
a parameter of type Any, it makes no sense to be used in a position 
where it is supposed to be a number, a boolean, or an E. Your program
must somehow 'narrow' the type of e down to what the operation expects, 
in your case E. 

If I knew where the TR guide lives, I'd add the appropriate two-line 
paragraph to clarify this point. 

;; --- 

> 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?

It is not quite true that TR doesn't infer types. It does so but in 
an extremely limited manner. Technically, this is called LOCAL Inference. 

What does this mean? 

When you write (lambda (x) ...) TR can't know what this function will be 
applied to. It must really assume x ranges over Any. 

When you write (let ((x 7)) ...) however, TR assumes you want x to range 
over numbers in the body of let because the initial value has type Number. 
To see how this fails, try 

 (let ([x 7]) (set! x "hello") x)

Again, I wish I could clarify this bit in the docs. 

-- Matthias