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


This is implementation of the "wobbly types" we've discussed before in GHC, slated for release in version 6.4. Simon also give a pointer to Tim Sheard's site, as he's done a lot of related work. There I found an interesting looking paper on Omega, a language which takes the GADT idea even further.

## Comment viewing options

One of the things that this will make easier is prototyping implementations of new monads.

Take, for example, a simple state monad:

type State s a = {- as yet unknown -}

(>>=) :: State s a -> (a -> State s b) -> State s b
return :: a -> State s a
fetch :: State s s
store :: s -> State s ()

runState :: State s a -> s -> (s,a)  -- observer


Ralf Hinze's paper, Deriving Backtracking Monad Transformers, expounds on John Hughes' method for deriving efficient implementations of monads like this by inventing axioms as needed and doing case-analysis on left-hand arguments.

One of the problems of this approach is that the intermediate steps weren't always implementable. Thanks to GADTs, they now are:

data State s a
= Bind :: State s a -> (a -> State s b) -> State s b
| Return :: a -> State s a
| Fetch :: State s s
| Store :: s -> State s ()

runState :: State s a -> s -> (s,a)
runState (Return a) s = (s,a)
runState Fetch s = (s,s)
runState (Store s) _ = (s,())
runState (Bind (Return a) k) s = runState (k a) s
runState (Bind Fetch k) s = runState (k s) s
runState (Bind (Store s) k) _ = runState (k ()) s
runState (Bind (Bind m k1) k2) s = runState m (\x -> Bind (k1 x) k2) s


It's not terribly efficient, but you can actually run it, which makes it easier to determine whether or not you've implemented the right interface.