[racket] Typed Racket: limited polymorphism?

On Tue, Jun 14, 2011 at 5:14 PM, Matthias Felleisen
<matthias at ccs.neu.edu> wrote:
>
> I would have expected that something like this might approximate what you want:
>
> #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)
>  (begin0
>    (node x y)
>    (unless (and (sn? x) (sn? y)) (error 'bad ""))))

I'd write this as follows:

#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.
-- 
sam th
samth at ccs.neu.edu