On Wed, 30 Mar 2005, Jacques Carette wrote:

> The most convincing example I have seen is that an eval function for a 
> statically-typed language
> let rec eval e =   match e with     | Lit n -> n
>    | Plus(a,b) -> (eval a) + (eval b)
>    | True -> true
>    | False -> false
>    | And(a,b) -> (eval a) && (eval b)
>    | If(t,c,a) -> if eval t then eval c else eval a
>    | IfZero e' -> (eval e') = 0
> is currently rejected in ML languages, but with GADTs the above can be 
> accepted, as it can't "go wrong".

I've played a little with GADTs in GHC 6.4.  What strikes me as most 
valuable about this example (besides its conciseness) it that it leverages 
the type-inferencer/checker in the metalanguage (Haskell) into a 
type-inferencer/checker for the object language.  I'm trying to make it do 
subtyping by passing lists of types (simulated by pairs).

  --
Christopher Dutchyn
UBC Computer Science


>
> Jacques
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>