7.5. Generalised Algebraic Data Types

Generalised Algebraic Data Types (GADTs) generalise ordinary algebraic data types by allowing you to give the type signatures of constructors explicitly. 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
      Pair   :: Term a -> Term b -> Term (a,b)

Notice that the return type of the constructors is not always Term a, as is the case with ordinary vanilla data types. Now we can write a well-typed eval function 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
  eval (Pair e1 e2) = (eval e2, eval e2)

These and many other examples are given in papers by Hongwei Xi, and Tim Sheard.

The extensions to GHC are these:

Notice that GADTs generalise existential types. For example, these two declarations are equivalent:

  data T a = forall b. MkT b (b->a)
  data T' a where { MKT :: b -> (b->a) -> T a }