# Kinds and Type Level Programming 3

In this post, the small type-level Prelude developed in the last two posts will be put to practical use to solve a problem for which standard Haskell doesn't have quite satisfactorily solutions. You can find the previous posts, introducing type level programming and showing some of it's capabilities, in these two links.

*
TL;DR: The complete Haskell code built in this post is available in
this gist
*

### The expression problem

Data types are modeled in Haskell via algebraic data types (ADTs) as a collection of cases (sum type). Let's consider a very simple sum type that is commonly used in Haskell:`data Either a b = Left a | Right b`

In order to work with some type, one generally wants to do one of two things:
- Write new functions using values of the type
- Add a new case to our sum type

Adding new functions that use the type is very easy to do, it isn't even
necessary to recompile code other than the one in which the new function was
implemented. Adding an alternative to the type, however, is a very different
problem. Imagine you wanted to add another alternative to
the `Either`

type. This very simple change would break code in lots
of places. For example case matches like the following would no longer be total.

```
case value of
Right a -> persistToDb a
Left b -> logError b
```

### Open Unions

The solution to the expression problem developed in this post is known
as *Open Unions*. A good intuition for thinking about open unions is to
consider them a way to track alternatives in the type system. An open union is a
set of types, where each value is a members of an element of this set.
To model these sets, type level lists will be used. The `Either`

type
could, for example, be transformed into something like this:

```
newtype Left a = Left a
newtype Right a = Right a
type Either a = '[Left a, Right a]
```

In this setting adding an alternative to the `Either`

type would be
as simple as declaring
```
newtype Middle a = Middle a
type ThreeWayEither a = (Middle a) ': (Either a)
```

This covers the general idea of how to handle open unions on the type level. What is required, however, is a representation on the value level. This is achieved using the the following GADT:

```
data Union (a :: [k]) where
Union :: Int -> b -> Union (a :: [k])
```

This `Union`

type has one constructor with two arguments. One is an
existential, `b`

, that is the actual value of interest. The
other is an `Int`

that gives the index of the type of `b`

in the type level list `a`

, which is a type parameter
of `Union`

.

### Reifying type level values

In order to work with the index of a type in a type level list at runtime, it first has to be identified it at compile time. This is done using a closed type family and the natural number type defined before:

```
data Nat = Z | S Nat
type family ElemIndexF (x :: a) (xs :: [a]) :: Nat where
ElemIndexF a '[] = TypeError (Text "Not a member of list")
ElemIndexF a (a ': xs) = Z
ElemIndexF a (b ': xs) = S (ElemIndexF a xs)
```

You can try this in ghci:
```
> :set -XDataKinds
> :kind! ElemIndexF Int [String, Bool, Int, IO String]
ElemIndexF Int [String, Bool, Int, IO String] :: Nat
= 'S ('S 'Z)
```

Next these values will be "pulled down" from the type level to the value
level. This is done by using a combination of `newtype`

and type
classes. First a `newtype`

wrapper `N`

around `Int`

is defined:

```
newtype N a = N Int
deriving Show
```

This newtype wrapper is given meaning by the following type class:

```
class NatToInt (a :: Nat) where
reifyNat :: N a
instance NatToInt 'Z where
reifyNat = N 0
instance (NatToInt a) => NatToInt ('S a) where
reifyNat =
let N n = reifyNat :: N a
in N (1 + n)
```

The above code is pretty neat. So far all type level computation in the previous posts was separate from the value level, where it can actually be put to use. You can try this in ghci as follows:

```
> reifyNat :: N (ElemIndexF Int [String, Bool, Int, IO String])
N 2
```

Using `NatToInt`

and `ElemIndexF`

a solution can be built,
again using `newtype`

to obtain the index of a type in a type level
list at runtime:

```
class ElemIndex a b where
elemIndex :: ListIndex a b
instance (NatToInt k, k ~ ElemIndexF a b) => ElemIndex a b where
elemIndex = let N n = reifyNat :: N k
in ListIndex n
```

### Putting together a working Open Union implementation

Now all the pieces required to build a working implementation of open unions are in place. In order to keep the following code more readable, a type synonym for an important constraint is defined:

```
type Member x xs = NatToInt (ElemIndexF x xs)
```

This constraint informs programmers that the type x is a member of the
type-level set xs. Using this constraint two functions `inject`

and `project`

, that either wrap a value in an open union or get a
value out of one, can be defined. The first will be `inject`

:

```
-- | Wrap a value in an open union.
inject :: forall a b . Member a b => a -> Union (b :: [*])
inject x =
let N n = reifyNat :: N (ElemIndexF a b)
in Union n x
```

This function is fairly straightforward, it takes a value and uses its types
index in the resulting unions list of types to create a `Union`

value. The trickier part is to retrieve values from
a `Union`

. Unfortunately `unsafeCoerce`

has to be used
here to deal with the existential constructor field in `Union`

:

```
-- | Get a value of a concrete type from an open union. This will be nothing if
-- the value in the union is not actually of type 'a'.
project :: forall a b . Member a b => Union b -> Maybe a
project (Union k v) =
let N n = reifyNat :: N (ElemIndexF a b)
in if k == n
then Just (unsafeCoerce v)
else Nothing
```

You can try these basic functions, again, in ghci:

```
> :t inject (5 :: Int) :: Union '[String, Int, Bool]
inject (5 :: Int) :: Union '[String, Int, Bool]
:: Union '[String, Int, Bool]
> project (inject (5 :: Int) :: Union '[String, Int, Bool]) :: Maybe Int
Just 5
```

### Pattern matching open unions

The open union implementation as laid out so far lacks some of the usability of
conventional ADTs. With vanilla data types `case`

expressions can be
used for pattern matching. Thus far, the open union implementation doesn't allow
for pattern matching. It is possible, however, to implement pattern matching on
open unions with compile-time totality checks.

`Matches b (xs :: [*])`

type, which is denoted to mean a set of functions, each transforming values of
one type out of `xs`

to `b`

.
```
infixr 6 :->
data Matches b (xs :: [*]) where
(:->) :: (a -> b) -> Matches b xs -> Matches b (a ': xs)
(:|) :: Matches b '[]
```

To proceed, two constraint type families are required, one stating, that a
type-level list is non-empty and one to check if two type level sets have the
same elements.
```
type family IsNonEmpty xs :: Constraint where
IsNonEmpty (a ': b) = ()
IsNonEmpty '[] = TypeError (Text "Type list is empty!")
type family SetEquality xs ys :: Constraint where
SetEquality xs ys = ( IsNonEmpty xs
, IsNonEmpty ys
, Members xs ys
, Members ys xs)
```

The last required piece to build up a pattern matcher is an `indexIn`

function, which returns the index of the argument type at the current head of
the `Matches`

value in the type level list of a given open union. A
nice thing about this code is that the function is total due to
the `Member`

constraint in the type signature.

```
indexIn :: forall a b xs ys . (Member a ys)
=> Matches b (a ': xs) -> Union ys -> Int
indexIn ms u =
let N n = reifyNat :: N (ElemIndexF a ys)
in n
```

This function can be used to step through a list of matches and detect when the
current head of the sequence of matches is a function that is suitable to turn the
current `Union`

value into `b`

.

```
matchTotal :: (SetEquality as xs) => Union as -> Matches b xs -> b
matchTotal u m =
case matchPartial u m of
Nothing -> error "This case is precluded by the type system"
Just x -> x
matchPartial :: (Members xs as) => Union as -> Matches b xs -> Maybe b
matchPartial u (:|) = Nothing
matchPartial u@(Union k v) m@(f :-> ms) =
let n = indexIn m u
in if n == k
then Just (f (unsafeCoerce v))
else matchPartial u ms
demoMatchTotal :: (SetEquality '[A Int, B String] as) => Union as -> Int
demoMatchTotal u = matchTotal u $
(\ (A x) -> x + 1) :->
(\ (B xs) -> length (xs :: String)) :->
(:|)
```