Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread output type
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2005-03-30 (20:43)
From: Jacques Carette <carette@m...>
Subject: Re: [Caml-list] output type
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
for a pleasant and informative read.  The slides give references as well as example applications.

For more information: (and several more at   [tougher read...]

For interesting but serious discussions:

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".