Jon (and others),
   In addition to the sources Jacques provided, let me point you to

   http://www.informatik.uni-bonn.de/~ralf/publications/With.pdf

for a very readable description that doesn't rely on heavy type theory to get
the idea across.

I wonder, if you really want to use this approach for genericity on, say
numeric types, if you need something like Haskell's newtype (and a guarantee
that the constructor get optimized away) to make it useful?

-- Brian

On Wed, 30 Mar 2005, Jacques Carette wrote:

> Jon Harrop <jon@ffconsultancy.com> wrote:
> > Would someone be so kind as to enlighten me (and probably a few other people!)
> > as to what these intruiging GADT things are and what they're good for? :-)
>
> They are a (conservative) extension to Algebraic Data Types (and G=Guarded or Generalized, depending on the author).
>  The basic idea is that instead of giving names to the various constructors in a Sum type, you give explicit functions
> which become the constructors.  Furthermore, you then make type inference context-dependent: the type of each
> constructor is inferred independently, and can have different 'guards'.
>
> Or at least that's my quick-and-dirty impression, which definitely contains technical inaccuracies, but is roughly
> right.  To get a good introduction, why not turn to
> http://pauillac.inria.fr/~fpottier/slides/slides-msr-11-2004.pdf
> for a pleasant and informative read.  The slides give references as well as example applications.
>
> For more information:
> http://research.microsoft.com/Users/simonpj/papers/gadt/gadt.ps.gz
> http://citeseer.ist.psu.edu/669510.html (and several more at http://cristal.inria.fr/~simonet/publis/)
> http://www.cs.bu.edu/~hwxi/academic/drafts/ATS.pdf   [tougher read...]
>
> For interesting but serious discussions:
> http://lambda-the-ultimate.org/node/view/552
> http://lambda-the-ultimate.org/node/view/116
> http://lambda-the-ultimate.org/node/view/290
>
> 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".
>
> 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
>