## 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:

• 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 }
```