# Type Level Programming

Type level programming is about encoding more information in our types, so make them more descriptive. The more descriptive types are, the easier it is to avoid runtime errors, as the type checker can do more at compile time.

The GHC language extensions used here are:

`-XDataKinds`

`-XGATDs`

`-XKindSignatures`

`-XScopedTypeVariables`

`-XTypeFamilies`

## Type Promotion

As we already know, types have kinds:

`Bool :: *`

`Maybe :: * -> *`

`[] :: * -> *`

`State :: * -> * -> *`

Also recall that we have to partially apply type constructors with kinds greater than `* -> *`

to use them as monads:

```
-- Maybe :: * -> *
instance Monad Maybe where
...
-- State :: * -> * -> *
instance Monad (State s) where
...
-- Either :: * -> * -> *
instance Monad Either where
... -- type error
instance Monad (Either e) where
... -- works
```

**Type Promotion** is used to define our own kinds. The DataKinds extension allows for this. Without DataKinds, `data Bool = True | False`

gives us two constructors, `True`

and `False`

. At the three levels in haskell:

- At the kind-level:
`*`

- At the type-level
`Bool`

- At the value-level:
`True`

or`False`

With DataKinds, we also get the following two new types, both of kind `Bool`

:

`'True :: Bool`

`'False :: Bool`

The value constructors `True`

and `False`

have been promoted to the type level as `'True`

and `'False`

. A new kind is introduced too, `Bool`

instead of just `*`

. We now have booleans at the type level.

**DataKinds promotes all value constructors to type constructors, and all type constructors to kinds.**

Another example, recursively defined natural numbers. `Zero`

is 0, and `Succ Nat`

is `Nat + 1`

.

```
data Nat = Zero | Succ Nat
-- values :: types
Zero :: Nat
Succ :: Nat -> Nat
-- types :: kinds
'Zero :: Nat
'Succ :: Nat -> Nat
```

## Generalised Algebraic Data Types

GADTs allow for more expressive type definitions. Normal ADT syntax:

```
data Bool = True | False
-- gives two values
True :: Bool
False :: Bool
```

Usually, we define the type and its values, which yields two value constructors. With a GADT, we explicitly specify the type of each data constructor:

```
data Bool where
True :: Bool
False :: Bool
data Nat where
Zero :: Nat
Succ :: Nat -> Nat
```

The example below defines a recursively defined `Vector`

type.

```
-- Normally
data Vector a = Nil | Cons a (Vector a)
-- GADT
data Vector a where
Nil :: Vector a
Cons :: a -> Vector a -> Vector a
```

## Example: A Safe Vector

The vector definition above can use another feature, called KindSignatures, to put more detail into the type of the GADT definition:

```
data Vector (n :: Nat) a where
Nil :: Vector n a
Cons :: a -> Vector n a -> Vector n a
```

This definition includes an `n`

to encode the size of the vector in the type. `n`

is a type of kind `Nat`

, as defined above. The values and types were promoted using DataKinds. The type variable `n`

can also be replaced with concrete types:

```
data Vector (n :: Nat) a where
Nil :: Vector `Zero a
Cons :: a -> Vector n a -> Vector (`Succ n) a
-- example
cakemix :: Vector ('Succ ('Succ Zero)) String
cakemix = Cons "Fish-Shaped rhubarb" (Cons "4 large eggs" Nil)
```

This further constrains the types to make the types more expressive. Now we have the length of the list expressed at type level, we can define a safer version of the head function that rejects zero-length lists at compile time.

```
vhead :: Vector ('Succ n) a -> a
-- this case will throw an error at compile time as it doesn't make sense
vhead Nil = undefined
vhead (Cons x xs) = x
```

Can also define a zip function for the vector type that forces inputs to be of the same length. The type variable `n`

tells the compiler in the type signature that both vectors should have the same length.

```
vzip :: Vector n a -> Vector n b -> Vector n (a,b)
vzip Nil Nil = Nil
vzip (Cons x xs) (Cons y ys) = Cons (x,y) (vzip xs ys)
```

## Singleton types

Singletons are types with a 1:1 correspondence between types and values. Every type has only a single value constructor. The following GADT is a singleton type for natural numbers. The `(n :: Nat)`

in the type definition annotates the type with it's corresponding value at type level. The type is parametrised over `n`

, where `n`

is the value of the type, at type level.

```
data SNat (n :: Nat) where
SZero :: SNat 'Zero
SSucc :: Snat n -> SNat ('Succ n)
-- there is only one value of type SNat 'Zero
szero :: SNat 'Zero
szero = SZero
-- singleton value for one and it's type
sone :: SNat ('Succ 'Zero)
sone = SSucc SZero
stwo :: SNat ('Succ ('Succ Zero))
sone = SSucc sone
```

**There is only one value of each type**. The data is stored at both the value and type level.

This can be used to define a replicate function for the vector:

```
vreplicate :: SNat n -> a -> Vector n a
vreplicate SZero x = Nil
vreplicate (SSucc n) x = Cons x (vreplicate n x)
```

The length of the vector we want is `SNat n`

at type level, which is a singleton type. This allows us to be sure that the vector we are outputting is the same size as what we told it, making sure this type checks.

## Proxy Types & Reification

We are storing data at the type level, which allows us to access the data at compile time and statically check it. If we want to access that data at runtime, for example to find the length of a vector, we need a *proxy type*. Proxy types allow for turning type level data to values, ie turning a type level natural number (`Nat`

) into an `Int`

. Haskell has no types at runtime (due to type erasure), so proxies are a hack around this.

```
-- a type NatProxy parametrised over some type a of kind Nat
data NatProxy (a :: Nat) = MkProxy
-- NatProxy :: Nat -> *
-- MkProxy :: NatProxy a
```

This proxy type is parametrised over some value of type `a`

with kind `Nat`

, but there is never actually any values of type `a`

involved, the info is at the type level. `a`

is a phantom type.

```
zeroProxy :: NatProxy 'Zero
zeroProxy = MkProxy
oneProxy :: NatProxy ('Succ 'Zero)
oneProxy = MkProxy
```

These two proxies have the same value, but different types. The `Nat`

type is in the phantom type `a`

at type level.

We can then define a type class, called `FromNat`

, that is parametrised over some type `n`

of kind `Nat`

:

```
class FromNat (n :: Nat) where
fromNat :: NatProxy n -> Int
```

The function `fromNat`

takes a `NatProxy`

, our proxy type, and converts it to an int. Instances can be defined for the two types of `Nat`

to allow us to covert the type level `Nat`

s to `Int`

s.

```
-- instance for 'Zero
instance FromNat 'Zero where
-- fromNat :: NatProxy 'Zero -> int
fromNat _ = 0
instance FromNat n => FromNat ('Succ n) where
fromNat _ = 1 + fromNat (MkProxy :: NatProxy n)
```

The arguments to these functions are irrelevant, as the info is in the types. The variable `n`

refers to the same type variable as in the instance head, using scoped type variables. This hack allows for passing types to functions using proxies, and the converting them to values using reification.

## Type Families

Type families allow for performing computation at the type level. A type family can be defined to allow addition of two type-level natural numbers:

```
type family Add (n :: Nat) (m :: Nat) :: Nat where
Add 'Zero m = m
Add ('Succ n) m = 'Succ (Add n m)
-- alternatively
type family (n :: Nat) + (m :: Nat) :: Nat where
'Zero + m = m
'Succ n + m = 'Succ (n + m)
```

The type family for `(+)`

is whats known as a closed type family: once it's defined it cannot be redfined or added to. This type family can be used to define an append function for our vector:

```
vappend :: Vector n a -> Vector m a -> Vector (n+m) a
vappend Nil ys = ys
vappend (Cons x xs) ys = Cons x (vappend xs ys)
```

Importing `GHC.TypeLits`

allows for the use of integer literals at type level instead of writing out long recursive type definitions for `Nat`

. This means we can now do:

```
data Vector (n :: Nat) a where
Nil :: Vector 0 a
Cons :: a -> Vector n a -> Vector (n+1) a
vappend Nil Nil :: Vector 0 a
vappend (Cons 4 Nil) Nil :: Vector 1 Int
vappend (Cons 4 Nil) (Cons 8 Nil) :: Vector 2 Int
```

### Associated (Open) Type Families

The definition below defines a typeclass for a general collection of items:

```
class Collection c where
empty :: c a
insert :: a -> c a -> c a
member :: a -> c a -> Bool
instance Collection [] where
empty = []
insert x xs = x : xs
member x xs = x `elem` xs
```

However, the list instance will throw an error, as `elem`

has an `Eq`

constraint on it, while the `member`

type from the typeclass doesn't. Another example, defining the red-black tree as an instance of `Collection`

(the tree is defined in one of the lab sheets):

```
instance Collection Tree where
empty = empty
insert x t = insert t x
member x t = member x t
```

This will raise two type errors, as both `insert`

and `member`

for the tree need `Ord`

constraints, which `Collection`

doesn't have.

To fix this, we can attach an associated type family to a type class.

```
class Collection c where
type family Elem c :: *
empty :: c
insert :: a -> c -> c
member :: a -> c -> Bool
```

For an instance of `Collection`

for some type `c`

, we must also define a case for c for a type level function `Elem`

, this establishing a relation between `c`

and some type of kind `*`

.

We can now define instance for list and tree, where `Eq`

and `Ord`

constraints are placed in instance definition.

```
instance Eq a => Collection [a] where
type Elem [a] = a
empty = []
insert x xs = x : xs
member x xs = x `elem` xs
instance Ord a => Collection (L.Tree a) where
type Elem (L.Tree a) = a
empty = L.Leaf
insert x t = L.insert t x
member x t = L.member x t
```