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