# Kinds and Type Level Programming 2

This is the continuation of my first post on advanced type-level programming features of the Haskell programming language. In this post I am going to implement some features of the haskell Prelude on the type level.

Since the features we are going to use in the following are not standard Haskell as defined by the Haskell2010 Report, we will start with activating a number of language extensions to get all the code in this post to work:

```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RankNTypes #-}
import GHC.TypeLits (TypeError (..), ErrorMessage(..))
```

### Booleans and control structures

The best type-level equivalent to a function on the value-level is a (closed) type family. We will start out by defining a few basic type families to model basic boolean logic and conditions.

```
type family Negate (x :: Bool) :: Bool where
Negate True = False
Negate False = True
type family Equals (a :: k) (b :: k) :: Bool where
Equals a a = True
Equals _ _ = False
type family And (a :: Bool) (b :: Bool) :: Bool where
And True True = True
And _ _ = False
type family Or (a :: Bool) (b :: Bool) :: Bool where
Or False False = False
Or _ _ = True
```

An essential control structure is `if/then/else` branching. Haskell
does not provide this for us on the type level, but we can still roll our
own. What we do is to write type family with one boolean parameter (the
condition) and two parameters representing the result of
the `then/else` branches.

```
type family IfThenElse (c :: Bool) (a :: k) (b :: k) where
IfThenElse True a _ = a
IfThenElse False _ b = b
```

### Basic list processing

By using the `DataKinds` extension, Lists Haskell automatically lifts
lists to the type level for us. Instead of defining our own list-type we will
simply reuse Haskell's List type.

#### Head & tail with custom type errors

Recall the value level definition of head:

```
head :: [a] -> a
head (x:_) = x
head [] = error "Head of empty list"
```

Pattern matching on a list's head in a type family is very straight forward, in
fact we did so in the previous post. What's new to us is
the `error`

call in the case of an empty list. It turns out just as
we can call error on the value level, Haskell also lets us do an error call on
the type level which will lead to a compile-time error message. For this we
need the `GHC.TypeLits`

import from above. Our head function will
then look like this:

```
type family Head (xs :: [a]) :: a where
Head '[] = TypeError (Text "Head of empty (type level) list!")
Head (x ': _) = x
```

Remember that the single quote `(')` before an identifier is for
emphasizing that we are talking about the "lifted" type level
version. `Text` is a constructor of the `TypeError` type. With
this technique, we can easily define a type level version
of `tail`

.

```
type family Tail (xs :: [a]) :: [a] where
Tail '[] = TypeError (Text "Tail of empty (type level) list!")
Tail (_ ': xs) = xs
```

#### Catenating lists

List concatenation will come in very handy for some of the next steps:

```
type family Catenate (x :: [k]) (y :: [k]) :: [k] where
Catenate '[] ys = ys
Catenate (x ': xs) ys = x ': (Catenate xs ys)
```

### Higher order functions

One of the more significant features of the Haskell programming language is
its ubiquitous use of higher order functions. What would our little
type-level Prelude be without some higher order functions of our own?

One of the simples and most frequently used higher order functions in standard
Haskell is the dot operator for function composition, so we will define the
type-level equivalent of that first:

```
type family Compose (f :: a -> b) (g :: b -> c) (x :: a) :: c where
Compose f g x = g (f x)
```

An other common higher order Haskell function is the `filter`

function. In order to implement this, we will have to reuse some of the
functionality we implemented previously:

```
type family Filter (predicate :: k -> Bool) (list :: [k]) :: [k] where
Filter predicate '[] = '[]
Filter predicate (x ': xs) =
Catenate (IfThenElse (predicate x) '[x] '[]) (Filter predicate xs)
```

Similarly we can define type level analogues of the standard
functions `fold`

and `map`

.
```
type family Map (f :: a -> b) (xs :: [a]) :: [b] where
Map f '[] = '[]
Map f (x ': xs) = (f x) ': (Map f xs)
type family Fold (f :: b -> a -> b) (x :: b) (as :: [a]) :: b where
Fold f x '[] = x
Fold f x (a ': as) = Fold f (f x a) as
```