*Generalized Algebraic Data Types (GADTs)* generalizes ordinary *Algebraic Data
Types(ADTs)* by permitting value constructors to return specific types. GADTs are used
for ensuring program correctness and in generic programming. This article is
specific to Haskell programming language. In Haskell GADTs are implemented as
a language extension. The article describes these use cases with small programs.

# Introduction

Type system help programmers ensure that the software they write behave correctly. They detect errors and also serve as documentation. A good type system allow abstracting domain specific concepts. Haskell’s much appreciated ADTs though powerful, is still lacking in few aspects. GADTs fill that gap.

This article explains GADTs with simple examples.

## Algebraic Data Types (ADTs)

ADTs are composite types, i.e., types formed by combining other types. Depending
on how the types are combined, we can have either a *sum* type or a *product* type.

```
data Point = Pt Int Int
data Expr a = Number Integer | Boolean Bool
```

In the example above `Point`

and `Expr`

are called *type constructors* and `Pt`

,
`Number`

, and `Boolean`

are called *value constructors*. If a type has more than
one value constructor, they are called alternatives: one can use any of these
alternatives to create a value of that type.

```
ghci> let a = Number 10
ghci> let b = Boolean True
ghci> :t a
a :: Expr
ghci> :t b
b :: Expr
```

Notice that the type of both `a`

and `b`

is `Expr.`

This is because of the type of the
value constructors.

```
ghci> :t Number
Number :: Integer -> Expr
ghci> :t Boolean
Boolean :: Bool -> Expr
```

To showcase how this complicates code, let us extend our type a bit and also add a expression evaluator.

```
data Expr = Number Int
| Succ Expr
| IsZero Expr
| If Expr Expr Expr
data Value = IntVal Int | BoolVal Bool
eval :: Expr -> Value
eval (Number i) = IntVal i
eval (Succ e) = case eval e of
IntVal i -> IntVal (i+1)
eval (IsZero e) = case eval e of
IntVal i -> BoolVal (i==0)
eval (If b e1 e2) = case eval b of
BoolVal True -> eval e1
BoolVal False -> eval e2
```

If you notice carefully, this allows for some invalid expressions to type check successfully.

```
expr1 = Succ (Number 1) -- valid and type checks
expr2 = Succ (IsZero (Number 1)) -- invalid but type checks
```

Also, notice how our `eval`

function is *partially* implemented. We do not know
what to evaluate a expression `Succ (IsZero (Number 1))`

to. We could allow the
function to indicate error by using a `Maybe`

or `Either`

type, but that
complicates the `eval`

function further as we recursively call `eval`

. Try it
out for fun.

## Generalised ADTs

The idea behind GADTs is to allow arbitrary return types for value constructors.
They *generalize* ordinary data types. GADTs are provided in GHC as a language
extension. We can enable this feature using the `LANGUAGE`

pragma. It provides a
new syntax for defining data types. We specify type for each value constructor.
We can now redefine our `Expr`

type like below:

```
{-# LANGUAGE GADTs #-}
data Expr a where
Number :: Int -> Expr Int
Succ :: Expr Int -> Expr Int
IsZero :: Expr Int -> Expr Bool
If :: ExprBool->Expra->Expra->Expra
```

Notice that return type for value constructor can differ. This allows our
program to be more strict. The value constructor `Succ`

, for example, expects a
`Expr Int.`

The compiler can now reject code if you provide `Expr Bool`

or anything
else.

```
ghci> :t Succ (Number 10)
Succ (Number 10) :: Expr Int
ghci> :t Succ (IsZero (Number 0))
<interactive>:1:7: error:
Couldn’t match type Bool with Int
Expected type: Expr Int
Actual type: Expr Bool
In the first argument of Succ, namely (IsZero (Number 0))
In the expression: Succ (IsZero (Number 0))
```

Now, with the refined `Expr`

type, the evaluation of expression become simple. The
expression evaluator need not worry about cases where the type do not match
(ill-typed expression we saw earlier). The new evaluator is easy to write and
read.

```
eval :: Expr a -> a
eval (Number i) = i
eval (Succ e) = 1 + eval e
eval (IsZero e) = 0 == eval e
eval (If b e1 e2) = if eval b then eval e1 else eval e2
```

This version of `eval`

is complete unlike the previously implemented one. If we
are evaluating an expression, the expression is guaranteed to be valid and no
failure cases are possible. Compile time guarantee is always better than a
runtime check.