# Type is an extensible GADT

We can define new types in Haskell, so the kind of types is clearly
**extensible**. Looking closer, it turns out that it is also oddly similar to a
**GADT**. ^{1}

(`Type`

is the better
name for `*`

. It can
be imported from
`Data.Kind`

.)

`Type`

is an ADT

Declaring a new type using the `data`

or `newtype`

keyword introduces a new
type constructor^{2}. This suggests a view of `Type`

as a “type”:

```
data Type
= Int
| Bool
| Maybe Type
| IO Type
-- A couple of fancier types
| Fix (Type -> Type)
| ReaderT Type (Type -> Type) Type -- transformers
| HList [Type] -- (heterogeneous lists)
| V Nat Type -- linear (fixed-length vectors)
| Header' [Type] Symbol Type -- servant
... -- very open
```

Constructions can be destructed, this is true of both the term level and the type level. In particular, type families give us type-level pattern matching. One difference with pattern matching as we’re used to at the term level is that there is no way to handle every case individually. The upside is that clauses are defined independently. They can be in any order, or in different modules.

For example, the `UnMTL`

type family below unfolds stacks of common monad
transformers to equivalent but more basic types.
(gist)

```
type family UnMTL (a :: Type) :: Type
type instance UnMTL (ReaderT r m a) = r -> UnMTL (m a)
type instance UnMTL (StateT s m a) = s -> UnMTL (m (a, s))
type instance UnMTL (ExceptT e m a) = UnMTL (m (Either e a))
type instance UnMTL (Identity a) = a
type instance UnMTL (IO a) = IO a
```

If a type family is applied to a type it can’t handle, nothing really happens, until the type checker tries to unify it with another type for example, causing an error at compile-time. (“Stuck” types don’t unify.)

```
ghci> :kind! UnMTL (StateT Int (Except String ()))
Int -> Either String (Int, ())
ghci> :kind! UnMTL Double -- not a transformer stack
UnMTL Double -- not an error
```

`Type`

is an existential type

The main common point of `Type`

with GADTs is that constructors can quantify
variables that don’t appear in their result types, which are then said to be
“existential types”.

Standard examples of polykinded type constructors:

```
data Proxy :: forall k. k -> Type -- Data.Proxy
data (:~:) :: forall k. k -> k -> Type -- Data.Type.Equality
data (:~~:) :: forall j k. j -> k -> Type -- idem
```

(We’ll keep the `forall`

implicit from now on.)

We need the `PolyKinds`

extension to quantify over kinds at all. But since
there’s no place for type variables in `Type`

, any polykinded type constructor
makes `Type`

an existential type.

```
data Type where
Proxy :: k -> Type
:~:) :: k -> k -> Type
(:~~:) :: j -> k -> Type
(Rec :: (u -> Type) -> [u] -> Type -- vinyl
...
```

## A note about indexed types

GADTs are also a form of indexed types: types with parameters that may depend on
the constructor.^{3} For example, singleton types are types indexed by values:

```
data SBool (_ :: Bool) where
-- ^-------------------+- indices
STrue :: SBool 'True -- <--|
SFalse :: SBool 'False -- <--/
```

Each constructor of `SBool`

corresponds to one constructor for the index.
`SBool`

is a “singleton type” because for every index `i :: Bool`

, there is
exactly one value of type `SBool i`

.

But `Type`

has no index, why am I talking about indexed types?
You’ve been tricked into reading so far, `Type`

is not the most interesting
GADT in this post!

To get there, we must take another small detour.
An interesting feature of type families is that constructors don’t need to
be fully applied to be matched. This is a notable difference between the
kind-level `(->)`

and the type-level `(->)`

.^{4}

```
type family IsOnlyJust (x :: a -> Maybe a) :: Bool
type instance IsOnlyJust 'Just = 'True
{- -- Term-level equivalent:
case (x :: a -> Maybe a) of
Just -> True
-- !? -}
type family IsOnlyMaybe (t :: Type -> Type) :: Bool
type instance IsOnlyMaybe Maybe = 'True
type instance IsOnlyMaybe IO = 'False
```

Thus a type constructor, such as `Maybe`

and `IO`

, somehow also behaves like a
constructor of `Type -> Type`

. For the same reasons as given above for `Type`

,
`Type -> Type`

is also GADT-like if we consider it as an atom:

```
data Type->Type where
Maybe :: Type->Type
:: Type -> Type->Type
(,) ReaderT :: Type -> (Type -> Type) -> Type->Type
...
```

More generally, the left hand side of an arrow can be different from `Type`

, so
this is a thing:

```
data (Type->Type)->Type where
Fix, Mu, Nu :: (Type->Type)->Type -- recursion-schemes
:~>) :: (Type -> Type) -> (Type->Type)->Type -- natural-transformation
(...
```

`_ -> Type`

is a GADT

Now consider the kind of unary type constructors, indexed by the kind of their single type parameter.

`type TyCon k = k -> Type`

Well, doesn’t this look like a fine GADT:

```
data TyCon k where
IO :: TyCon Type
Fix :: TyCon (TyCon Type)
Proxy :: TyCon k
:~:) :: k -> TyCon k
(Const :: Type -> TyCon k
Compose :: TyCon j -> (k -> j) -> TyCon k
Product :: TyCon k -> TyCon k -> TyCon k
Rec :: (u -> Type) -> TyCon [u]
...
```

One application of this observation is to implement type functions in Haskell
via *typed* defunctionalization (Defunctionalization for the
win).
It makes abstract sense because GADTs are great to embed typed languages in
typed languages.

In fact, this post was split off from an upcoming one about defunctionalization.