[racket] Typed Racket: limited polymorphism?

From: Sam Tobin-Hochstadt (samth at ccs.neu.edu)
Date: Tue Jun 14 17:52:41 EDT 2011

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

Posted on the users mailing list.