From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <carette@univmail.cis.mcmaster.ca>
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 E905CBC84
	for <caml-list@yquem.inria.fr>; Wed, 30 Mar 2005 22:43:20 +0200 (CEST)
Received: from cgpsrv2.cis.mcmaster.ca (cgpsrv2.CIS.McMaster.CA [130.113.64.62])
	by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j2UKhKeQ014438
	for <caml-list@yquem.inria.fr>; Wed, 30 Mar 2005 22:43:20 +0200
Received: from [24.43.193.126] (account carette@univmail.cis.mcmaster.ca)
  by cgpsrv2.cis.mcmaster.ca (CommuniGate Pro WebUser 4.1.8)
  with HTTP id 87517767; Wed, 30 Mar 2005 15:43:19 -0500
From: "Jacques Carette" <carette@mcmaster.ca>
Subject: Re: [Caml-list] Pervasives.compare output type
To: Jon Harrop <jon@ffconsultancy.com>, caml-list@yquem.inria.fr
X-Mailer: CommuniGate Pro WebUser Interface v.4.1.8
Date: Wed, 30 Mar 2005 15:43:19 -0500
Message-ID: <web-87517767@cgpsrv2.cis.mcmaster.ca>
In-Reply-To: <200503302106.11361.jon@ffconsultancy.com>
MIME-Version: 1.0
Content-Type: text/plain; charset="ISO-8859-1"; format="flowed"
Content-Transfer-Encoding: 8bit
X-Miltered: at nez-perce with ID 424B0F68.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)!
X-Spam: no; 0.00; caml-list:01 pervasives:01 constructors:01 constructors:01 inference:01 simonpj:01 citeseer:01 simonet:01 publis:01 drafts:01 tougher:01 convincing:01 rec:01 2004.:98 psu:98 
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 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