Reflecting values to types and back

28 Aug 2013 Austin Seipp View Markdown source

As of March 2020, School of Haskell has been switched to read-only mode.

Sections

This week, on /r/haskell:

"I still want a reflection tutorial!" - Oliver Charles

The configurations problem

Several years ago, Oleg Kiselyov and Chung-chieh Shan wrote a paper entitled "Functional Pearl: Implicit configurations". It's actually a very fascinating paper and it's very readable too (I encourage tackling it if you're an intermediate Haskeller.) In the paper, they propose a solution the configurations problem:

The configurations problem is to propagate run-time preferences throughout a program, allowing multiple concurrent configuration sets to coexist safely under statically guaranteed separation...

In our approach, a term expression can refer to run-time configuration parameters as if they were compile-time constants in global scope ... We can propagate any type of configuration data -- numbers, strings, IO actions, polymorphic functions, closures, and abstract data types.

This may remind you of an extension our lovely GHC supports - ImplicitParams - which tries to make this sort of behavior lightweight. Unfortunately, ImplicitParams has a number of drawbacks, one being that they are 'infectuous' in areas like scoping (and they have other concerns too.) The solution in this case is to instead propogate values around via types, rather than the kind of dynamic binding which ImplicitParams gives us.

Well, our very own Edward Kmett of course packaged this up into a library, which he calls reflection. This tutorial going to both show you how it works, and what it allows. NB: This writeup isn't really going to concern itself with Kiselyov's original presentation, and instead focuses on Eds from this point on. (On one hand, this implementation 'cheats' the premise by using unsafe features, where the original paper didn't - and as we will understand, makes our implementation significantly faster. On the other hand it's possibly the only Oleg paper I'm aware of which was reduced to, like, 7 lines of code.)

The reflection API can be boiled down to three very simple things:

-- #1: A 'Proxy' value which we can tag with types.
data Proxy k = Proxy

-- #2: A class to 'reflect' values back into terms
class Reifies s a | s -> a where
  reflect :: proxy s -> a

-- #3: A function to reify values *into* types
-- 
-- NB: refiy's second argument has a rank2 type. The 's' type variable will
-- guarantee that two competing `Proxy s` values cannot unify with each other or be leaked.
reify :: forall a r. a -> (forall (s :: *). Reifies s a => Proxy s -> r) -> r

Here's an example of this:

module Main (main) where
import Data.Reflection

-- show
main :: IO ()
main = print example
  where
    example :: Int
    example = reify 10 $ \p -> (reflect p) + (reflect p)
-- /show

In this example, we reify the value 10 over the enclosed lambda. Inside the lambda, we can reflect the p value to get our 10 :: Int back. But if we look at the type of reify, the lambda accepts a parameter of type Proxy s! And we never had any instances of Reifies for our types. So how does it know what value to return, given the Proxy? What's going on?

(Again, one important thing to note - although we won't mention it anymore - is the rank2 type of reify. This trick is similar to what we do to ST, to ensure we can't 'leak' a reference to a Proxy s and reuse it later.)

A look under the hood

To understand what's going on, the easiest way to look at the source of reify, and see how it elaborates to GHC Core. As a warning, if you consider yourself a very purist Haskeller, the following definition is probably going to make you feel pretty uncomfortable.

Below is an implementation of the entire basic reflection API

import Unsafe.Coerce

data Proxy k = Proxy

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

newtype Magic a r = Magic (forall (s :: *). Reifies s a => Proxy s -> r)

reify :: forall a r. a -> (forall (s :: *). Reifies s a => Proxy s -> r) -> r
reify a k = unsafeCoerce (Magic k :: Magic a r) (const a) Proxy
{-# INLINE reify #-}

Before we can fully understand this though, we need to understand what GHC does when faced with type classes during compilation.

Type-class elaboration and the single-method dictionary

Before we continue, I'd recommend you go ahead and install ghc-core from Hackage, which will make life much easier. It makes the default output of Core much more readable (although we will clean it up even further with a few extra options.) Work along with the examples. Here, I'm using GHC 7.6.3, although the specifics haven't really changed much in the last few versions.

Consider the following program:

module Main (main, test1, test2) where

main :: IO ()
main = return ()

class Foo a where
  bar :: a -> Int
  baz :: a -> Bool

instance Foo Int where
  bar x = x+1
  baz x = x==0

instance Foo Bool where
  bar True  = 0
  bar False = 1
  baz x     = x

lorem :: Foo a => a -> (Int, Bool)
lorem x = (bar x, baz x)
{-# NOINLINE lorem #-}

test1 = lorem (1::Int)
test2 = lorem True

When GHC compiles the definition of lorem, it needs to be able to dispatch calls to bar and baz depending on the argument type. In order to do this, we perform a process called dictionary elaboration, in which we essentially replace a constraint (like Foo a) with a compiler-generated dictionary, which contains the methods to call. So the compiler produces something like this:

foo'Int'bar :: Int -> Int
foo'Int'bar x = x+1

foo'Int'baz :: Int -> Bool
foo'Int'baz x = x==0

foo'Bool'bar :: Bool -> Int
foo'Bool'bar True  = 0
foo'Bool'bar False = 1

foo'Bool'baz :: Bool -> Bool
foo'Bool'baz x     = x

data FooDict a =
  FooDict { fooDict'bar :: a -> Int
          , fooDict'baz :: a -> Bool
          }

lorem :: FooDict a -> a -> (Int, Bool)
lorem dict x = (fooDict'bar dict x, fooDict'baz dict x)

test1 = lorem (FooDict foo'Int'bar foo'Int'baz) 1
test2 = lorem (FooDict foo'Bool'bar foo'Bool'baz) True

As we can see, the type class is totally eliminated and instead replaced by a data type, containing our type class methods (note that FooDict a isomorphic to (a -> Int, a -> Bool)) The compiler then manually plumbs around the correct dictionaries at the call site of lorem.

Let's verify this using ghc-core. Stuff the above code into a file, and compile it like so:

ghc-core --no-asm --no-cast -- -dsuppress-var-kinds -dsuppress-type-applications -dsuppress-uniques Foo.hs

The arguments suppress a lot of the unnecessary output in this case, so the output looks slightly more like 'simple haskell' as opposed to 'compiler intermediate language.' But it's still pretty verbose.

We see output similar to the following:

$fFooBool2 :: Int
$fFooBool2 = I# 1

lorem [InlPrag=NOINLINE]
  :: forall a. Foo a => a -> (Int, Bool)
lorem =
  \ (@ a) ($dFoo :: Foo a) (x :: a) ->
    (bar $dFoo x, baz $dFoo x)

test1 :: (Int, Bool)
test1 = lorem $fFooInt $fFooBool2

test2 :: (Int, Bool)
test2 = lorem $fFooBool True

(Quick tip: in System FC, the GHC Core language, types as well as values are explicit as arguments. The syntax (@ a) does not refer to a value argument - it instead says lorem is a function which takes a singular type argument called a, as well as two value arguments: a dictionary of type Foo a and a value of type a.)

So we see everything is as we expect. Both test1 and test2 pass a dictionary as the first argument to lorem, which dispatches on the Foo a dictionary to call the right functions. (Check the remainder of the output to see the rest, including how $fFooInt for example is actually a dictionary of $fFooInt_$cbar and $fFooInt_$cbaz)

But there is an important special case here: if a type class only has one method, we simply pass around the method itself. This is obvious - if a type class only contains a method foo :: Bar => a -> Int, there is no need to create a data FooDict = FooDict (a -> Int), when instead we can just pass around the (a -> Int) on its own. Let's verify that with the following code:

module Main (main, test1) where

main :: IO ()
main = return ()

class Foobar a where
  foobar :: a -> Int

instance Foobar Int where
  foobar x = x*x

ipsum :: Foobar a => a -> Int
ipsum a = (foobar a) + 10
{-# NOINLINE ipsum #-}

test1 = ipsum (10::Int)

Load it into ghc-core, and we see:


$fFoobarInt_$cfoobar :: Int -> Int
$fFoobarInt_$cfoobar =
  \ (x :: Int) -> $fNumInt_$c* x x

ipsum :: forall a. Foobar a => a -> Int
ipsum =
  \ (@ a) ($dFoobar :: Foobar a) (a :: a) ->
    case ($dFoobar `cast` ...) a of _ { I# x ->
    I# (+# x 10)
    }

test1 :: Int
test1 =
  ipsum ($fFoobarInt_$cfoobar `cast` ...) test2

We see something different here: instead, test1 passes the function $fFoobarInt_$cfoobar as an argument to ipsum, after coercing it using a `cast` expression. ipsum then uses it and applies it as a function to the argument a in the case expression. This shows we are correct: single-method 'dictionaries' for a type class are really just functions by themselves.

Side note: you may be wondering what the deal with cast is. It's a little too complex to go into here, but essentially, GHC Core has a notion of coercion variables which allow us to witness the equivalence between two types. Coercions allow us to establish equality between two types which are not syntactically equal - in the above case, we establish the fact that the dictionary type Foobar Int is the same as the type Int -> Int. If we made another instance, say Foobar Bool, and then somewhere else said ipsum False, we would get a coercion variable that establishes Foobar Bool as equivalent to Bool -> Int. ipsum also uses a coercion variable, more generally stating that Foobar a is equal to a -> Int. This is really about all you need to know.

While this trick is fairly obvious when you think about it, it is critical to the implementation of reflection, as we shall shortly see. (Maybe you already see where this is going...)

From reify to reflect to nothing at all

We're about 80% of the way to understanding reflection. Only 80% left!

The core of it all is this:

newtype Magic a r = Magic (forall (s :: *). Reifies s a => Proxy s -> r)

reify :: forall a r. a -> (forall (s :: *). Reifies s a => Proxy s -> r) -> r
reify a k = unsafeCoerce (Magic k :: Magic a r) (const a) Proxy

The first thing to note is that a newtype has the same representation as its underlying type. That means that in the above case, a value Magic k has the same runtime representation as k by itself. (GHC discharges such newtype-equivalences based on the same coercion variables we mentioned before. Newtypes are turned into coercions very early in the compilation process.)

Second, we must remember that at the Core level, k takes two arguments, not one. After elaboration, the first argument is the 'dictionary', but because Reifies only has one method, the first argument to k will be a function of type proxy s -> a. The second argument is of type Proxy s:

Given:

  k :: forall (s :: *). Reifies s a => Proxy s -> r
= { dictionary elaboration }
  k :: forall (s :: *). Reifies s a -> Proxy s -> r
= { Reifies is a single-method class; thus a dictionary is a fn }
  k :: forall (s :: *). (proxy s -> a) -> Proxy s -> r

So at runtime, k takes two arguments, not one. The trick here is that the types of k and Magic k are different at the Haskell level.

We add a 'layer' of Magic onto the type of k, and then unsafeCoerce it away. In doing so, we basically give k the final type above. By exploiting the fact newtype doesn't really exist at runtime, and Reifies actually becomes an argument, we can use unsafeCoerce to expose the runtime representation of k.

Remember: unsafeCoerce pays no attention to runtime representation. It just sidesteps the typechecker. In this case, however, we are coercing a value for which we are certain of the runtime representation. This lets us get away with 'slipping in' our own argument.

Let's go to our original example and step through it (with slight psuedo-syntax and hand-waving)

Given:

  reify 10 $ \p -> (reflect p) + (reflect p)
= { defn of reify }
  unsafeCoerce (Magic $ \p -> (reflect p) + (reflect p)) (const 10) Proxy
= { dictionary elaboration }
  unsafeCoerce (Magic $ \dReflect p -> (dReflect p) + (dReflect p)) (const 10) Proxy
= { unsafeCoerce Magic elimination }
  (\dReflect p -> (dReflect p) + (dReflect p)) (const 10) Proxy
= { beta reduction }
  (\p -> (const 10 p) + (const 10 p)) Proxy
= { beta reduction }
  (const 10 Proxy) + (const 10 Proxy)
= { defn of const }
  10 + 10
= { addition }
  20

More generally, we can use a similar hand-waving to establish the following: reify a reflect = a:

Given:

  reify a reflect
= { eta expand }
  reify a (\p -> reflect p)
= { defn of reify }
  unsafeCoerce (Magic $ \p -> reflect p) (const a) Proxy
= { dictionary elaboration }
  unsafeCoerce (Magic $ \dReflect p -> dReflect p) (const a) Proxy
= { unsafeCoerce Magic elimination }
  (\dReflect p -> dReflect p) (const a) Proxy
= { beta reduction }
  (\p -> const a p) Proxy
= { beta reduction }
  const a Proxy
= { defn of const }
  a

And that's about it! It should now also be clear why this implementation is so fast: it has almost no extra runtime overhead.

There are some important things to reiterate. By now, you should see why we never need an instance of Reifies for anything: because we create the dictionary ourselves, and use const a in its place. And thus reflect p = const a p = a, where a is the configuration you provided.

Second, it's important to note (as always!) that unsafeCoerce/Magic here really don't have a justifying rule to reason about them with. The above 'proof' is operational and a bit hand-wavy. You can't really apply many deductive reasoning steps like above to such operators. It all simply works because we unsafeCoerce a value with a guaranteed expectation of what it will look like at runtime. We could say that the 'unsafeCoerce Magic elimination' rule above is simply a truth to be assumed - that it will yield an appropriate function.

Third, you may still be wondering about the weird type reflect :: proxy s -> a. The reason for this will become clear, but in a nutshell, we do this because we want to unify the type variable s with the s at a call site, but we don't care about the actual proxy type itself - since reflect never actually uses its argument anyway.

Dynamically constructing type-class instances

With our new power, it's possible to do something we couldn't before. We can create dynamically create type class instances for a given type. The trick is that we wrap our actual values into a newtype, and the instance of that newtype actually uses reflect to pull methods from the scope which reify creates. This allows you to pass in whatever dictionary you want to reify.

Here's an example. We'll create a type over which we can dynamically construct an Ord instance.

{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE UndecidableInstances  #-}
module Main where
import Data.Proxy
import Data.Reflection

-- show
-- Values of type 'a' in our dynamically constructed 'Ord' instance
newtype O a s  = O { runO :: a }
 
-- A dictionary describing an 'Ord' instance.
newtype Ord_ a = Ord_ { compare_ :: a -> a -> Ordering }
 
-- Utility
isEq :: Ordering -> Bool
isEq EQ = True
isEq _  = False
 
instance Reifies s (Ord_ a) => Eq (O a s) where
  a == b = isEq (compare_ (reflect a) (runO a) (runO b))
 
instance (Eq (O a s), Reifies s (Ord_ a)) => Ord (O a s) where
  compare a b = compare_ (reflect a) (runO a) (runO b)
 
-- Dynamically construct an 'Ord' instance out of a comparsion operator.
withOrd :: (a -> a -> Ordering) -> (forall s. Reifies s (Ord_ a) => O a s) -> a
withOrd f v = reify (Ord_ f) (runO . asProxyOf v)
  where
    asProxyOf :: f s -> Proxy s -> f s
    asProxyOf v _ = v

-- Regular ord instance
example1 :: Int
example1 = withOrd compare $ max (O 1) (O 2)

-- Backwards ord instance
example2 :: Int
example2 = withOrd (flip compare) $ max (O 1) (O 2)
 
main :: IO ()
main = print example1 >> print example2
-- /show

The above examples show we can compare these Ord-like values, but change out the actual dictionary at runtime!

Note in the instance declaration, we say reflect a, where a :: O a s. This goes back to what I said earlier about reflect :: proxy s -> a - we want the s type variables to unify, but we don't care that the outer type constructor is O a :: * -> *. In other words, proxy unifies with anything specifically because it's irrelevant as to what it is.

But what about manual dictionaries?

The above might just seem like a parlor trick, although there is real value. Indeed - what about manual dictionaries, you ask yourself? We could feasibly just construct a type where the dictionary argument is explicit and we feed it in. Then we can shuffle it around in the associated type-class instance, and it works similarly to the API above. We construct a dictionary, and scope its use over some computation.

In the following example, Mon1 is a monoid with a manually managed dictionary argument, while Mon2 has its monoid instance managed by reflection instead.

{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE UndecidableInstances  #-}
module Main where
import Data.Proxy
import Data.Monoid
import Data.Reflection

-- show
-- Dynamically constructed monoid values.
data Monoid_ a = Monoid_ { mappend_ :: a -> a -> a, mempty_ :: a }

-- Monoids which explicitly hold their own dictionary
newtype Mon1 a = Mon1 (Monoid_ a -> a)
instance Monoid (Mon1 a) where
  mempty                  = Mon1 mempty_
  Mon1 f `mappend` Mon1 g = Mon1 $ \m -> mappend_ m (f m) (g m)
 
embed1 :: a -> Mon1 a
embed1 x = Mon1 (\_ -> x)
 
run1 :: (a -> a -> a) -> a -> Mon1 a -> a
run1 f z (Mon1 v) = v (Monoid_ f z)

-- Monoids with a reflection-managed dictionary.
newtype Mon2 a s = Mon2 { unMon2 :: a }
instance Reifies s (Monoid_ a) => Monoid (Mon2 a s) where
  mappend a b        = Mon2 $ mappend_ (reflect a) (unMon2 a) (unMon2 b)
  mempty = a where a = Mon2 $ mempty_ (reflect a)
 
embed2 :: a -> Mon2 a s
embed2 x = Mon2 x
 
run2 :: (a -> a -> a) -> a -> (forall s. Reifies s (Monoid_ a) => Mon2 a s) -> a
run2 f z v = reify (Monoid_ f z) (unMon2 . asProxyOf v)
  where
    asProxyOf :: f s -> Proxy s -> f s
    asProxyOf v _ = v
 
-- Examples
sixteen :: Monoid m => m -> m
sixteen one = eight <> eight
  where
    eight   = four <> four
    four    = two  <> two
    two     = one  <> one
{-# INLINE sixteen #-}
 
ex1 :: Int
ex1 = run1 (+) 0 (sixteen $ embed1 2)
 
ex2 :: Int
ex2 = run2 (+) 0 (sixteen $ embed2 2)

main :: IO ()
main = print ex1 >> print ex2
-- /show

The problem with this, though, is sharing. There is a huge difference between ex1 and ex2.

Note the embedding of values into their monoid counterparts:

embed1 :: a -> Mon1 a
embed1 x = Mon1 (\_ -> x)

embed2 :: a -> Mon2 a s
embed2 x = Mon2 x

Given these definitions, the definitions of ex1 and ex2 have very different runtime characteristics. In ex1, we share the lambdas in our computation, not the results. ex2 however, does properly share the results.

We can confirm this with a quick look at the Core. ex1:

ex1_x :: Int
ex1_x = I# 2

$wa1
  :: (Int -> Int -> Int)
     -> Int
$wa1 =
  \ (ww :: Int -> Int -> Int) ->
    ww
      (ww (ww ex1_x ex1_x) (ww ex1_x ex1_x))
      (ww (ww ex1_x ex1_x) (ww ex1_x ex1_x))

ex1 :: Int
ex1 =
  case $wa1 $fNumInt_$c+ of _ { I# x ->
  I# (+# x x)
  }

vs ex2:

ex2_z :: Int
ex2_z = I# 0

ex2_x :: Monoid_ Int
ex2_x = Monoid_ $fNumInt_$c+ ex2_z

ex3 :: Any * -> Monoid_ Int
ex3 = \ _ -> ex2_x

ex2 :: Int
ex2 =
  ((\ (@ s)
      ($dReifies
         :: Data.Reflection.Reifies * s (Monoid_ Int)) ->
      let {
        eight [Dmd=Just L] :: Mon2 Int s

        eight =
          let {
            four [Dmd=Just L] :: Mon2 Int s

            four =
              let {
                two [Dmd=Just L] :: Mon2 Int s

                two =
                  case ($dReifies `cast` ...) (ex1_x `cast` ...)
                  of _ { Monoid_ ds _ ->
                  (ds ex1_x ex1_x) `cast` ...
                  } } in
              case ($dReifies `cast` ...) two of _ { Monoid_ ds _ ->
              (ds (two `cast` ...) (two `cast` ...)) `cast` ...
              } } in
          case ($dReifies `cast` ...) four of _ { Monoid_ ds _ ->
          (ds (four `cast` ...) (four `cast` ...)) `cast` ...
          } } in
      case ($dReifies `cast` ...) eight of _ { Monoid_ ds _ ->
      let {
        a1 [Dmd=Just S] :: Int

        a1 = ds (eight `cast` ...) (eight `cast` ...) } in
      \ _ -> a1
      })
   `cast` ...)
    ex3 (Data.Proxy.Proxy)

None of the work is shared in ex1, but all of it is in ex2.

And looking at embed1, this is rather obvious: we must recompute the lambda for every 'step'. This means that while ex1 takes 16 reductions (one for every instance of one), ex2 only takes 4 reductions thanks to the fact the results are shared. This sharing loss thus explodes pretty quickly.

(Incidentally, this exact problem is the reason Edward wrote reflection in the first place.)

Turning up the magic to over 9000

Finally, we're going to do something even scarier. With our above examples of creating type class instances, one drawback is we have to manually 'annotate' our values by wrapping them in a newtype. The newtype with the phantom s parameter is what A) keeps instance resolution happy, and B) lets us have a modicum of safety by not leaking Proxy values. But that's kind of inconvenient - is there another way?

Of course there is. By the power of ConstraintKinds, TypeFamilies and unsafeCoerce, what could possibly stop us?

First, we'll build some machinery to help abstract out the common patterns of creating these dynamic instances. This will rely on Edward's other package known as constraints. This helps reduce boilerplate and makes usage more consistent. If you're not already familiar with constraints, I have a blog post about the general mechanism, concerning :- (called |- in my article) and Sub/Dict.

Let us first define Lift, which essentially tags a value of type a with an s phantom type (for the rank2 context,) and also a phantom for a Constraint constructor.

newtype Lift (p :: * -> Constraint) (a :: *) (s :: *) = Lift { lower :: a }

Lift p a s describes a value of type a, with associated phantoms s and p. p in this case, is some type constructor which will produce a Constraint when given a type. We'll be applying p to a to yield a Constraint as we'll shortly see.

Now, we can define a type class which will tie a given class Constraint to a representation of its dictionary. We do this using TypeFamilies: for any given instance of the type class, we define a data constructor representing it.

class ReifiableConstraint p where
  data Def (p :: * -> Constraint) (a :: *) :: *
  reifiedIns :: Reifies s (Def p a) :- p (Lift p a s)

We'll get back to reifiedIns in a minute.

ReifiableConstraint makes more sense when you see it being used:

instance ReifiableConstraint Monoid where
  data Def Monoid a = Monoid { mappend_ :: a -> a -> a, mempty_ :: a }
  reifiedIns = Sub Dict

This means that we represent the Monoid constraint (a type constructor of kind * -> Constraint) as a dictionary, containing its mappend and mempty methods, like earlier. Hence, ReifiableConstraint associates a given Constraint with its 'reified form' as a value. Now we can tie Def Monoid a and Lift Monoid a s into an Monoid instance:

instance Reifies s (Def Monoid a) => Monoid (Lift Monoid a s) where
  mappend a b        = Lift $ mappend_ (reflect a) (lower a) (lower b)
  mempty = a where a = Lift $ mempty_ (reflect a)

Finally, we define the general with utility. This can be used to create dynamic instances for any Lifted value which is tied to a ReifiableConstraint.

with :: Def p a -> (forall s. Reifies s (Def p a) => Lift p a s) -> a
with d v = reify d (lower . asProxyOf v)
  where
    asProxyOf :: f s -> Proxy s -> f s
    asProxyOf x _ = x

And now we can say:

with (Monoid (+) 0) $ mempty <> Lift 10 <> Lift 12 -- evaluates to 22
with (Monoid (*) 1) $ mempty <> Lift 10 <> Lift 12 -- evaluates to 120

If we define instances for Eq and Ord, both with and Lift will work perfectly for them, too. If we put all the types together, we can sort of see how this plays out: given a Lift p a s value, over some constraint p, we derive the appropriate Reifies context with the associated Def value, and in the instance itself, we pull the methods from Def and use them, like we did earlier. This is mostly just generalizing out all of the type variables/type constructors we specialized initially.

So that's part one. We have some general machinery to ease implementing these special dictionaries and use them generically. Now we get to the scarier part, and we come back to reifiedIns. Its type is very important. It says:

The type Reifies s (Def p a) entails p (Lift p a s)

So, in any context where p (Lift p a s) occurs as a Constraint, it is safe to replace it with the constraint Reifies s (Def p a). This is because the latter constraint implies the former constraint. However, Lift p a s is really just a wrapper around a value of type a. So in a sense, p a should be able to imply p (Lift p a s) too. By the property of transitivity, this would mean the simple context p a could then imply Reifies s (Def p a).

Using some unsafety, we can create this bridge:

using :: forall p a. ReifiableConstraint p => Def p a -> (p a => a) -> a
using d m = reify d $ \(_ :: Proxy s) ->
  let replaceProof :: Reifies s (Def p a) :- p a
      replaceProof = trans proof reifiedIns
        where proof = unsafeCoerceConstraint :: p (Lift p a s) :- p a
  in m \\ replaceProof

Note carefully the definition here. It basically says, in step:

  • reifiedIns is a proof that the constraint p (Lift p a s) can be replaced by Reifies s (Def p a)
  • proof is an unsafe proof saying that the constraint p a can be replaced by p (Lift p a s)
  • By transitivity of these two proofs, we have proof p a may be replaced by Reifies s (Def p a)
  • Given the term m of type a appears in the context p a, and a proof that Reifies s (Def p a) :- p a, we can replace the context p a => a with Reifies s (Def p a) => a, which is exactly the type reify expects. Note we directly consume the Proxy with ScopedTypeVariables to bring the s type parameter into scope, so we can unify with it.

And with that magic, we can now say:

using (Monoid (+) 0) $ mempty <> 10 <> 12 -- evaluates to 22
using (Monoid (*) 1) $ mempty <> 10 <> 12 -- evaluates to 120

Conclusion

The code from the last section is below for completeness.

Many thanks to Edward for the discussions we had about these libraries, and the tips he gave me when approaching reflection from a pedagogical standpoint. And, of course, for writing the libraries themselves.

-- show
{-# LANGUAGE Rank2Types, FlexibleContexts, UndecidableInstances, TypeFamilies #-}
{-# LANGUAGE ConstraintKinds, KindSignatures, PolyKinds, TypeOperators #-}
{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables #-}
{-# LANGUAGE FunctionalDependencies #-}
module Main where
import Data.Proxy
import Data.Monoid
import Data.Reflection
import Data.Constraint
import Data.Constraint.Unsafe

--------------------------------------------------------------------------------
-- Lift/ReifiableConstraint machinery.
 
newtype Lift (p :: * -> Constraint) (a :: *) (s :: *) = Lift { lower :: a }
 
class ReifiableConstraint p where
  data Def (p :: * -> Constraint) (a :: *) :: *
  reifiedIns :: Reifies s (Def p a) :- p (Lift p a s)
 
with :: Def p a -> (forall s. Reifies s (Def p a) => Lift p a s) -> a
with d v = reify d (lower . asProxyOf v)
  where
    asProxyOf :: f s -> Proxy s -> f s
    asProxyOf x _ = x

--------------------------------------------------------------------------------
-- Kicking it up to over 9000

using :: forall p a. ReifiableConstraint p => Def p a -> (p a => a) -> a
using d m = reify d $ \(_ :: Proxy s) ->
  let replaceProof :: Reifies s (Def p a) :- p a
      replaceProof = trans proof reifiedIns
        where proof = unsafeCoerceConstraint :: p (Lift p a s) :- p a
  in m \\ replaceProof
 
--------------------------------------------------------------------------------
-- Examples of `ReifiableConstraint`

instance ReifiableConstraint Eq where
  data Def Eq a = Eq { eq_ :: a -> a -> Bool }
  reifiedIns = Sub Dict
 
instance Reifies s (Def Eq a) => Eq (Lift Eq a s) where
  a == b = eq_ (reflect a) (lower a) (lower b)
 
instance ReifiableConstraint Ord where
  data Def Ord a = Ord { compare_ :: a -> a -> Ordering }
  reifiedIns = Sub Dict
 
instance Reifies s (Def Ord a) => Eq (Lift Ord a s) where
  a == b = (compare a b == EQ)
 
instance Reifies s (Def Ord a) => Ord (Lift Ord a s) where
  compare a b = compare_ (reflect a) (lower a) (lower b)
 
instance ReifiableConstraint Monoid where
  data Def Monoid a = Monoid { mappend_ :: a -> a -> a, mempty_ :: a }
  reifiedIns = Sub Dict
 
instance Reifies s (Def Monoid a) => Monoid (Lift Monoid a s) where
  mappend a b        = Lift $ mappend_ (reflect a) (lower a) (lower b)
  mempty = a where a = Lift $ mempty_ (reflect a)
-- /show

main :: IO ()
main = return ()