On Tue, Jun 14, 2011 at 5:48 PM, Matthias Felleisen <[email protected]> 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 [email protected] _________________________________________________ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/users
