[racket] Typed Racket: limited polymorphism?

On Tue, Jun 14, 2011 at 5:48 PM, Matthias Felleisen
<matthias at ccs.neu.edu> wrote:
>
> On Jun 14, 2011, at 5:41 PM, Sam Tobin-Hochstadt wrote:
>
>>>
>>
>> #lang typed/racket
>> (define-type SN (U String Number))
>> (define-predicate sn? SN)
>> (struct: (α) node ({left : α} {right : α}))
>>
>> (: create-node (All (β) (β β -> (node SN))))
>> (define (create-node x y)
>>  (if (and (sn? x) (sn? y))
>>      (node x y)
>>      (error 'bad "")))
>>
>> Unfortunately, Typed Racket doesn't know that the function Matthias
>> wrote never returns if `x' and `y' aren't in `SN', so his version
>> won't typecheck, regardless of the bug he's found.
>
> That's the version I had first. Then I thought I'd trick it into believing me with begin0 and unless.
>
> Why doesn't error return empty and then it all works out? BTW, the SN should be a beta.

First, why the `begin0'?  I find this clearer:

(define (create-node x y)
  (unless (and (sn? x) (sn? y)) (error 'bad))
  (node x y))

Second, the problem is that TR doesn't understand that if one branch
of an `if' returns an empty type, then the conditions of the other
branch must be true in subsequent statements in sequence.
Fundamentally, TR has no knowledge about sequencing -- every element
of a `begin' might be run in any order as far as the type checker
cares.  Fixing this is on the long-term todo list.
-- 
sam th
samth at ccs.neu.edu