From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id EE216BC84 for ; Thu, 31 Mar 2005 02:44:41 +0200 (CEST) Received: from mail25.sea5.speakeasy.net (mail25.sea5.speakeasy.net [69.17.117.27]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j2V0id2Z005605 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Thu, 31 Mar 2005 02:44:41 +0200 Received: (qmail 11681 invoked from network); 31 Mar 2005 00:44:38 -0000 Received: from shell4.sea5.speakeasy.net ([69.17.116.5]) (envelope-sender ) by mail25.sea5.speakeasy.net (qmail-ldap-1.03) with AES256-SHA encrypted SMTP for ; 31 Mar 2005 00:44:38 -0000 Date: Wed, 30 Mar 2005 16:44:38 -0800 (PST) From: brogoff To: Jon Harrop Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Pervasives.compare output type In-Reply-To: Message-ID: References: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Miltered: at nez-perce with ID 424B47F7.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 pervasives:01 uni-bonn:01 ralf:01 genericity:01 haskell's:01 constructors:01 constructors:01 inference:01 simonpj:01 citeseer:01 simonet:01 publis:01 drafts:01 tougher:01 X-Spam-Checker-Version: SpamAssassin 3.0.2 (2004-11-16) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.2 X-Spam-Level: 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 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 >