# GADTs

GADTs let you associate different type parameters for different data constructors of a type.

For example, imagine we represent simple language terms that can only be bool/int literals and And/Add operations between those:

```
data Expr = ExprInt Int
| ExprBool Bool
| ExprAnd Expr Expr
| ExprAdd Expr Expr
```

This would let us do invalid things like:

`ExprAnd (ExprInt 5) (ExprBool True)`

Firstly and less importantly, GADTs let us write the same definition using a different notation:

```
data Expr where
ExprInt :: Int -> Expr
ExprBool :: Bool -> Expr
ExprAnd :: Expr -> Expr -> Expr
ExprAdd :: Expr -> Expr -> Expr
```

The real point of this notation is that it is an opportunity to associate different constructors of `Expr`

with different type constraints and type parameters:
So you restrict the return value of the

```
data Expr :: * -> * where
ExprInt :: Int -> Expr Int
ExprBool :: Bool -> Expr Bool
ExprAnd :: Expr Bool -> Expr Bool -> Expr Bool
ExprAdd :: Expr Int -> Expr Int -> Expr Int
```

This rules out non-sensical terms like:

ExprAnd (ExprInt 5) (ExprBool True)

Additionally, GADTs let you add type-class constraints and forall’d variables to each of the constructors. For example, let’s say we want to represent a length-indexed list:

```
data LenList :: Nat -> * -> * where
Nil :: LenList 0 a
Cons :: a -> LenList n a -> LenList (1 + n) a
```

Note that not only do the 2 differing constructors have differing type params (0/1+n), they also have constraints linking the "n" from the "LenList" type index (aka type parameter) to the "n" of the given list.

Another important facet of GADTs is that all this extra information is not just used to type-check value constructions as shown above. It also gives you back type information when you do case analysis. i.e:

```
case myLenList of
Nil -> ... -- ^ the type of myLenList in this case is inferred to (LenList 0 a)
Cons x xs -> ... -- ^ the type of myLenList in this case is inferred to
(LenList (1 + n) a) and the type of xs is inferred to (LenList n a)
```

f To reiterate, the type of the term we're case analyzing is inferred differently according to runtime values (which constructor is chosen).

Lastly, by allowing interesting types and constraints on each constructor, GADTs implicitly allow existential quantification, and storing of type-class instances inside values.

For example, this existentially quantified (and mostly useless) type:

data SomeShowable = forall a. Show a => MkSomeShowable a

Can be represented with GADTs as:

data SomeShowable where MkSomeShowable :: Show a => a -> SomeShowable

Note the `forall a.`

can be left implicit in the GADT version.

Interestingly, with GADTs, you can have existential quantification only in some of your constructors. You can have differing type-class instances stored inside different constructors. When you pattern-match your GADT constructor, the instance implicitly comes into scope.