An important device in the tool belt I carry around everyday is type class reflection. I don’t reach for it often, but it can be very useful. Reflection is a little known device. And for some reason it is often spoken of with a hint of fear.

In this post, I want to convince you that reflection is not hard and that you ought to know about it. To that end, let me invite you to join me on a journey to sort a list:

sortBy :: (a->a->Ordering) -> [a] -> [a]

What is reflection?

Type class reflection is an extension of Haskell which makes it possible to use a value as a type class instance. There is a package on Hackage, implementing type class reflection for GHC, which I will use for this tutorial. Type class reflection being an extension of Haskell (that is, it can’t be defined from other Haskell features), this implementation is GHC-specific and will probably not work with another compiler.

Literate Haskell

This blog post was generated from literate Haskell sources. You can find an extracted Haskell source file here.

There is a bit of boilerplate to get out of the way before we start.

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}

module Reflection where

import Data.Proxy
import Data.Reflection

UndecidableInstances… scary, I know. It is unfortunately required. It means that we could technically send the type checker into an infinite loop. Of course, we will be careful not to introduce such loops.

Sorted lists

My goal, today, is to sort a list. In order to make the exercise a tiny bit interesting, I will use types to enforce invariants. I’ll start by introducing a type of sorted lists.

newtype SortedList a = Sorted [a]

Obviously, a SortedList is a list: we can just forget about its sortedness.

forget :: SortedList a -> [a]
forget (Sorted l) = l

But how does one construct a sorted list? Well, at the very least, the empty lists and the lists of size 1 are always sorted.

nil :: SortedList a
nil = Sorted []

singleton :: a -> SortedList a
singleton a = Sorted [a]

What about longer lists though? We could go about it in several ways. Let’s decide to take the union of two sorted list:

merge :: Ord a => SortedList a -> SortedList a -> SortedList a
merge (Sorted left0) (Sorted right0) = Sorted $ mergeList left0 right0
  where
    -- 'mergeList l1 l2' returns a sorted permutation of 'l1++l2' provided
    -- that 'l1' and 'l2' are sorted.
    mergeList :: Ord a => [a] -> [a] -> [a]
    mergeList [] right = right
    mergeList left [] = left
    mergeList left@(a:l) right@(b:r) =
        if a <= b then
          a : (mergeList l right)
        else
          b : (mergeList left r)

We need Ord a to hold in order to define merge. Indeed, type classes are global and coherent: there is only one Ord a instance, and it is guaranteed that merge always uses the same comparison function for a. This enforces that if Ord a holds, then SortedList a represents lists of a sorted according to the order defined by the unique Ord a instance. In contrast, a function argument defining an order is local to this function call. So if merge were to take the ordering as an extra argument, we could change the order for each call of merge; we couldn’t even state that SortedList a are sorted.

If it weren’t for you meddling type classes

That’s it! we are done writing unsafe code. We can sort lists with the SortedList interface: we simply need to split the list in two parts, sort said parts, then merge them (you will have recognised merge sort).

fromList :: Ord a => [a] -> SortedList a
fromList [] = nil
fromList [a] = singleton a
fromList l = merge orderedLeft orderedRight
  where
    orderedLeft = fromList left
    orderedRight = fromList right
    (left,right) = splitAt (div (length l) 2) l

Composing with forget, this gives us a sorting function

sort :: Ord a => [a] -> [a]
sort l = forget (fromList l)

Though that’s not quite what we had set out to write. We wanted

sortBy :: (a->a->Ordering) -> [a] -> [a]

It is easy to define sort from sortBy (sort = sortBy compare). But we needed the type class for type safety of the SortedList interface. What to do? We would need to use a value as a type class instance. Ooh! What may have sounded eccentric when I first brought it up is now exactly what we need!

As I said when I discussed the type of merge: one property of type classes is that they are globally attached to a type. It may seem impossible to implement sortBy in terms of sort: if I use sortBy myOrd :: [a] -> [a] and sortBy myOtherOrd :: [a] -> [a] on the same type, then I am creating two different instances of Ord a. This is forbidden.

So what if, instead, we created an entirely new type each time we need an order for a. Something like

newtype ReflectedOrd a = ReflectOrd a

Except that we can’t do a newtype every time we call sortBy. So let’s make one newtype once and for all, with an additional parameter.

newtype ReflectedOrd s a = ReflectOrd a

-- | Like `ReflectOrd` but takes a `Proxy` argument to help GHC with unification
reflectOrd :: Proxy s -> a -> ReflectedOrd s a
reflectOrd _ a = ReflectOrd a

unreflectOrd :: ReflectedOrd s a -> a
unreflectOrd (ReflectOrd a) = a

Now, we only have to create a new parameter s locally at each sortBy call. This is done like this:

reifyOrd :: (forall s. Ord (ReflectedOrd s a) => …) -> …

What is happening here? The reifyOrd function takes an argument which works for any s. In particular, if every time we called reifyOrd we were to actually use a different s then the program would be correctly typed. Of course, we’re not actually creating types: but it is safe to reason just as if we were! For instance if you were to call reifyOrd (reifyOrd x) then x would have two distinct parameters s1 and s2: s1 and s2 behave as names for two different types. Crucially for us, this makes ReflectedOrd s1 a and ReflectedOrd s2 a two distinct types. Hence their Ord instance can be different. This is called a rank 2 quantification.

In order to export a single reify function, rather than one for every type class, the reflection package introduces a generic type class so that you have:

reify :: forall d r. d -> (forall s. Reifies s d => Proxy s -> r) -> r

Think of d as a dictionary for Ord, and Reifies s d as a way to retrieve that dictionary. The Proxy s is only there to satisfy the type-checker, which would otherwise complain that s does not appear anywhere. To reiterate: we can read s as a unique generated type which is valid only in the scope of the reify function. For completeness, here is the the Reifies type class, which just gives us back our d:

class Reifies s d | s -> d where
  reflect :: proxy s -> d

The | s -> d part is called a functional dependency. It is used by GHC to figure out which type class instance to use; we won’t have to think about it.

Sorting with reflection

All that’s left to do is to use reflection to give an Ord instance to ReflectedOrd. We need a dictionary for Ord: in order to build an Ord instance, we need an equality function for the Eq subclass, and a comparison function for the instance proper:

data ReifiedOrd a = ReifiedOrd {
  reifiedEq :: a -> a -> Bool,
  reifiedCompare :: a -> a -> Ordering }

Given a dictionary of type ReifiedOrd, we can define instances for Eq and Ord of ReflectedOrd. But since type class instances only take type class instances as an argument, we need to provide the dictionary as a type class. That is, using Reifies.

instance Reifies s (ReifiedOrd a) => Eq (ReflectedOrd s a) where
  (==) (ReflectOrd x) (ReflectOrd y) =
    reifiedEq (reflect (Proxy :: Proxy s)) x y

instance Reifies s (ReifiedOrd a) => Ord (ReflectedOrd s a) where
  compare (ReflectOrd x) (ReflectOrd y) =
    reifiedCompare (reflect (Proxy :: Proxy s)) x y

Notice that because of the Reifies on the left of the instances GHC does not know that it will for sure terminate during type class resolution (hence the use of UndecidableInstances). However, these are indeed global instances: by definition, they are the only way to have an Ord instances on the ReflectedOrd type! Otherwise GHC would complain.

We are just about done: if we reify a ReifiedOrd a, we have a scoped instance of Ord (ReflectedOrd s a) (for some locally generated s). To sort our list, we simply need to convert between [a] and ReflectedOrd s a.

sortBy :: (a->a->Ordering) -> [a] -> [a]
sortBy ord l =
  reify (fromCompare ord) $ \ p ->
    map unreflectOrd . sort . map (reflectOrd p) $ l

-- | Creates a `ReifiedOrd` with a comparison function. The equality function
--   is deduced from the comparison.
fromCompare :: (a -> a -> Ordering) -> ReifiedOrd a
fromCompare ord = ReifiedOrd {
  reifiedEq = \x y -> ord x y == EQ,
  reifiedCompare = ord }

Wrap up & further reading

We’ve reached the end of our journey. And we’ve seen along the way that we can enjoy the safety of type classes, which makes it safe to write function like merge in Haskell, while still having the flexibility to instantiate the type class from a function argument, such as options from the command line. Since type class instances are global, such local instances are defined globally for locally generated types. This is what type class reflection is all about.

If you want to delve deeper into the subject of type class reflection, let me, as I’m wrapping up this tutorial, leave you with a few pointers to further material:

• A talk by Edward Kmett, the author of the reflection package, on the importance of the global coherence of type classes and about reflection
• There is no built-in support for reflection in GHC, this tutorial by Austin Seipp goes over the very unsafe, internal compiler representation dependent, implementation of the library
• John Wiegley discusses an application of reflection in relation with QuickCheck.
• You may have noticed, in the definition of sortBy, that we map the reflectOrd and unreflectOrd in order to convert between a and ReflectedOrd s a. However, while, reflectOrd and unreflectOrd, have no computational cost, using them in combination with map will traverse the list. If you are dissatisfied with this situation, you will have to learn about the Coercible type class. I would start with this video from Simon Peyton Jones.