Example
Conventional algebraic datatypes are parametric in their type variables. For example, if we define an ADT like
data Expr a = IntLit Int
| BoolLit Bool
| If (Expr Bool) (Expr a) (Expr a)
with the hope that this will statically rule out non-well-typed conditionals, this will not behave as expected since the type of IntLit :: Int -> Expr a is universially quantified: for any choice of a, it produces a value of type Expr a. In particular, for a ~ Bool, we have IntLit :: Int -> Expr Bool, allowing us to construct something like If (IntLit 1) e1 e2 which is what the type of the If constructor was trying to rule out.
Generalised Algebraic Data Types allows us to control the resulting type of a data constructor so that they are not merely parametric. We can rewrite our Expr type as a GADT like this:
data Expr a where
IntLit :: Int -> Expr Int
BoolLit :: Bool -> Expr Bool
If :: Expr Bool -> Expr a -> Expr a -> Expr a
Here, the type of the constructor IntLit is Int -> Expr Int, and so IntLit 1 :: Expr Bool will not typecheck.
Pattern matching on a GADT value causes refinement of the type of the term returned. For example, it is possible to write an evaluator for Expr a like this:
crazyEval :: Expr a -> a
crazyEval (IntLit x) =
-- Here we can use `(+)` because x :: Int
x + 1
crazyEval (BoolLit b) =
-- Here we can use `not` because b :: Bool
not b
crazyEval (If b thn els) =
-- Because b :: Expr Bool, we can use `crazyEval b :: Bool`.
-- Also, because thn :: Expr a and els :: Expr a, we can pass either to
-- the recursive call to `crazyEval` and get an a back
crazyEval $ if crazyEval b then thn else els
Note that we are able to use (+) in the above definitions because when e.g. IntLit x is pattern matched, we also learn that a ~ Int (and likewise for not and if_then_else_ when a ~ Bool).
