Home

Generalized ADTs in Haskell

Simon Peyton-Jones, via Haskell-list:

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.

By Bryn Keller at 2004-10-01 17:11 | Functional | Implementation | other blogs | 10823 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Prototyping new monads

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.

By Pseudonym at Sun, 2004-10-03 04:00 | login or register to post comments