# Kinds and Type Level Programming 3

Written 2019-12-31

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.

A series of pattern matches is expressed by a `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)) :->
(:|)``````

### Conclusion

In this post, a solution to the expression problem is developed. There are other previous solutions, for example by Oleg Kiselyov. One interesting aspect of the developed solution is that it does not utilize overlapping type class instances, which I personally find to be weird. Furthermore a way to do pattern matching on open unions is developed which allows for both total and partial matches.