[Haskell] Generalised algebraic data types

[Simon Peyton-Jones]

Folks

I've finished my first attempt at implementing Generalised Algebraic
Data types in GHC.  Ordinary algebraic data types are generalised to
allow you to write an explicit type signature for each constructor; for
example:

     data Term a where
	Lit :: Int -> Term Int
	Succ :: Term Int -> Term Int
	IsZero :: Term Int -> Term Bool	
	If :: Term Bool -> Term a -> Term a -> Term a

Notice that some of these constructors have return types that are not
just "Term a"... that's the whole point!  Now you can write typed
evaluator for these terms:

    eval :: Term a -> a
    eval (Lit i)		= i
    eval (Succ t) 	= 1 + eval t
    eval (IsZero i) 	= eval i == 0
    eval (If b e1 e2)	= if eval b then eval e1 else eval e2

GADTs are not a new idea.  They go back to inductive type families in
type theory and dependent types, and more recently have been studied in
a programming-language context by Xi, Hinze & Cheney, Simonet & Pottier,
and Sheard.  Indeed, Tim Sheard's language Omega is has taken the same
ideas a good deal further.  He has a good bunch of links at his home
page
	http://www.cs.pdx.edu/~sheard/
The only really new thing is that it's in GHC. Our paper about the ideas
is at
	http://research.microsoft.com/~simonpj/papers/gadt/index.htm, 
and it has lots of references to related work.

GADTs will be in GHC 6.4, which we'll release in the next month or two,
but meanwhile it's in the HEAD of the CVS repository.  Anyone who's
prepared to build from source, or who can grab a development snapshot
from the GHC website, can try it out.  I'd like to encourage you to do
so, so that you can discover the more egregious bugs before we ship 6.4,
rather than after.  (Also error messages are likely to be poor at
first.)  First-cut documentation of the feature is in ghc/docs; a
typeset snapshot is at
	http://research.microsoft.com/~simonpj/tmp/gadt.html, 

There's a small collection of test programs that exercise GADTs in GHC's
test suite:
http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/testsuite/tests/ghc-re
gress/gadt/

You can use these as a guide to syntax, and a source of programming
ideas. You'll find red-black trees (invariants guaranteed by the types),
evaluators, type checkers, and more besides. (NB: some are supposed to
fail: see all.T.  Most are transcribed from Tim's Omega examples.)  

I'd love to have more GADT tests: send them to me and I'll add them.
And let me know how you get on. 

Simon