7.5. Generalised Algebraic Data Types (GADTs)

Generalised Algebraic Data Types 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 t)   = eval t == 0
  eval (If b e1 e2) = if eval b then eval e1 else eval e2
  eval (Pair e1 e2) = (eval e1, eval e2)

These and many other examples are given in papers by Hongwei Xi, and Tim Sheard. There is a longer introduction on the wiki, and Ralf Hinze's Fun with phantom types also has a number of examples. Note that papers may use different notation to that implemented in GHC.

The rest of this section outlines the extensions to GHC that support GADTs. It is far from comprehensive, but the design closely follows that described in the paper Simple unification-based type inference for GADTs, which appeared in ICFP 2006.

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 }