# Kinds and Type Level Programming

Recently, I have been playing around with some more advanced features of the Haskell programming language. Specifically with type level computations and kinds. Over the coming weeks, I will write a few posts from my notes on this subject.

### Distinguishing Type-Level and Value-Level

For newcomers to Haskell, the idea of computing at the type level may seem
strange. These abilities are still somewhat limited but this feature set is
constantly being extended and improved. An important separation that you
should keep in mind is between the *type level* and the *value
level*.

Let's say for example you have some `String` input which can be
validated. One way to model this would be via
a *phantom type*
similar to this:

```
data NonValidated
data Validated
newtype Input a = String
readNextInput :: IO (Input NonValidated)
readNextInput = undefined -- the implementation is not relevant here
validateInput :: Input a -> Input Validated
validateInput (Input xs) = Input $ filter (/= ' ') xs
```

In the example above, the `Input a`

type is just a newtype wrapper
around `String`

, which *completely* disappears at runtime. So
even though the type is different from the
`String`

type, due to Haskell's type erasure this has no
bearing on any runtime representation of information.

However, no runtime impact doesn't mean that there is no impact on the logic
we can express. The phantom type ensures, that we can't accidentally pass
around invalid data at compile time before the program ever runs. What happens
on the *type level* at compilation constrains *value level*
operations taking place at runtime.

### Kinds - A Level Above Types

A problem with the code above is, that it would be possible for a programmer to
introduce values of type `Input Int`

or `Input Bool`

or
use any other type in the parameter of our `Input`

newtype. Wouldn't
it be nicer if we could be sure that we only ever got `Input Validated`

or
`Input NonValidated`

? We can do this by introducing a new *kind*.

Just as there is a type-level "above" the value-level, there is a kind-level
above the type level. Using standard Haskell 98, however, we hardly notice it
being there. Values such as `True`

and `False`

are
inhabitants of the type `Bool`

. In much the same way, types such
as `Bool`

or `String`

are inhabitants of the
kind `*`

, which is the kind of types.

The kind `*`

is inhabited by all ordinary types that don't have type
parameters. `*`

is not the only kind we have at our disposal in
standard Haskell. A familiar type of a kind other than `*`

is `Maybe`

. Note, that we are not talking about ```
Maybe
ByteString
```

or `Maybe Handle`

but just `Maybe`

.

The kind of `Maybe`

is `(* -> *)`

. The easiest way to
think of it is, that `Maybe`

is a function that takes an ordinary
type as an argument and returns an ordinary type. Another familiar
type, `Either`

, shows us yet another kind, namely ```
(* -> * ->
*)
```

. We can actually observe this in ghci:

```
λ :kind Int
Int :: *
λ :kind Bool
Bool :: *
λ :kind Maybe
Maybe :: * -> *
λ :kind Either
Either :: * -> * -> *
```

GHC comes with an extension called `DataKinds`

that allows us to
lift data constructors to the type level. This may at first sound somewhat
abstract so I'll start out with an example:

```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
data ValidationState = Validated | NonValidated
newtype Input (a :: ValidationState) = Input String
```

Just as in our first validation example above, we defined a newtype
Wrapper `Input a`

around String. The difference, however, is that
before `Validated`

and `NonValidated`

were two different
types. And, worse, nothing prevented the type parameter of `Input`

from being any type such as `Word`

or `(IO Int)`

.

This changes with our lifted data
type `ValidationState`

. The `DataKinds`

extension lifts
data types and constructors up a level. So the
type `ValidationState`

becomes available to us as a kind and the
two constructors `Validated`

and `NonValidated`

become
types. We again turn to ghci:

```
λ :kind Validated
Validated :: ValidationState
λ :kind NonValidated
NonValidated :: ValidationState
λ :kind Input
Input :: ValidationState -> *
λ :kind Input Validated
Input Validated :: *
```

The `DataKinds`

extension actually is far more powerful than our
rather trivial example may suggest. Using this extension *every type and
constructor* becomes lifted so that we e.g. have
a *kind* `Bool`

and `True`

and `False`

are types of this kind:

```
λ :kind True
True :: Bool
λ :kind False
False :: Bool
```

Bearing in mind that the standard Haskell List type is basically defined as a
type with two constructors, `:`

and `[]`

,
the `DataKinds`

extension lets us define type level lists:

```
λ :set -XTypeOperators
λ :kind '[]
'[] :: [k]
λ :kind (:)
(:) :: a -> [a] -> [a]
λ :kind String ': Int ': '[]
String ': Int ': '[] :: [*]
```

The single quote in `':`

and `'[]`

is a way to
syntactically indicate that we are talking about the type level list constructors
(and not the value level ones).
### Type-Level Numbers and Type-Level Functions

So far we haven't done any actual computing yet: we have no type-level numbers
and no way to compute anything on the type level! So let's change that by first
defining natural numbers on the type level. We do this by
using `DataKinds`

to define Natural numbers:

```
data Nat = Z | S Nat
```

where `Z`

is zero and `(S x)`

is x+1. We now have a kind
Nat and all natural numbers also exist on the type level as inhabitants of
the *kind* `Nat`

The last piece of the puzzle we are missing are type level functions. GHC gives
us these as an extension with the somewhat strange
name `TypeFamilies`

. A type family is basically a type level
function. We will now build a type family for adding our numbers we defined
above. Just like an ordinary function we start with a signature:

`type family Add (a :: Nat) (b :: Nat) :: Nat where`

This signature tells us that our type family `Add`

turns
two `Nat`

s into a new `Nat`

. Now we define the whole
logic as follows:

```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies#-}
{-# LANGUAGE UndecidableInstances#-}
data Nat = Z | S Nat
type family Add (a :: Nat) (b :: Nat) :: Nat where
Add Z a = a
Add (S a) b = Add a (S b)
```

That we have to use the `UndecidableInstances`

extension of GHC here
is a bit of a wart, but it can't be avoided. The danger here is that we could
build a type family that never terminates. Since type families are always
evaluated at compile-time this could lead to the compiler not terminating. In
general, GHC can't decide if a type family will terminate (ultimately due to the
halting problem) and therefore we have to tell GHC "it's OK, believe us"
using `UndecidableInstances`

.

As usual, we want to play with this in ghci. To actually evaluate our type family we
can use the `:kind!`

command as follows:

```
λ :kind! Z
Z :: Nat
= 'Z
λ :kind! (S Z)
(S Z) :: Nat
= 'S 'Z
λ :kind! (S (S Z))
(S (S Z)) :: Nat
= 'S ('S 'Z)
λ :kind! Add Z Z
Add Z Z :: Nat
= 'Z
λ :kind! Add Z (S Z)
Add Z (S Z) :: Nat
= 'S 'Z
λ :kind! Add (S Z) (S Z)
Add (S Z) (S Z) :: Nat
= 'S ('S 'Z)
```

### Conclusion

We have covered a lot of ground in this post. The discussed material, along with a bit of basic Haskell, will allow us to do some quite amazing things. I will continue this exploration of type-level computation in an upcoming post very soon. Until then I encourage anyone who reads this to play around with the code above. See you soon!