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 Either a b = Left a | Right b

• 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]

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)

> :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.

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

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