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 }