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:
Data type declarations have a 'where' form, as exemplified above. The type signature of
each constructor is independent, and is implicitly universally quantified as usual. Unlike a normal
Haskell data type declaration, the type variable(s) in the "data Term a where" header
have no scope. Indeed, one can write a kind signature instead:
data Term :: * -> * where ...
or even a mixture of the two:
data Foo a :: (* -> *) -> * where ...
The type variables (if given) may be explicitly kinded, so we could also write the header for Foo
like this:
data Foo a (b :: * -> *) where ...
There are no restrictions on the type of the data constructor, except that the result
type must begin with the type constructor being defined. For example, in the Term data
type above, the type of each constructor must end with ... -> Term ....
You cannot use a deriving clause on a GADT-style data type declaration,
nor can you use record syntax. (It's not clear what these constructs would mean. For example,
the record selectors might ill-typed.) However, you can use strictness annotations, in the obvious places
in the constructor type:
data Term a where
Lit :: !Int -> Term Int
If :: Term Bool -> !(Term a) -> !(Term a) -> Term a
Pair :: Term a -> Term b -> Term (a,b)
Pattern matching causes type refinement. For example, in the right hand side of the equation
eval :: Term a -> a eval (Lit i) = ...
the type a is refined to Int. (That's the whole point!)
A precise specification of the type rules is beyond what this user manual aspires to, but there is a paper
about the ideas: "Wobbly types: practical type inference for generalised algebraic data types", on Simon PJ's home page.
The general principle is this: type refinement is only carried out based on user-supplied type annotations.
So if no type signature is supplied for eval, no type refinement happens, and lots of obscure error messages will
occur. However, the refinement is quite general. For example, if we had:
eval :: Term a -> a -> a eval (Lit i) j = i+j
the pattern match causes the type a to be refined to Int (because of the type
of the constructor Lit, and that refinement also applies to the type of j, and
the result type of the case expression. Hence the addition i+j is legal.
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 }