Black Magic in Haskell Reflection

Question

I was hoping someone could shed a little light on the black magic in Data.Reflection. The pertinent snippet is:

{-# LANGUAGE CPP #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE KindSignatures #-}

module Data.Reflection
    (
      Reifies(..)
    , reify
    ) where

import Data.Proxy
import Unsafe.Coerce

class Reifies s a | s -> a where
  -- | Recover a value inside a 'reify' context, given a proxy for its
  -- reified type.
  reflect :: proxy s -> a

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

-- | Reify a value at the type level, to be recovered with 'reflect'.
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

1. I can't parse the definition for reify. maybe I'm missing something simple about order of evaluation, but it looks like unsafeCoerce::a->b is applied to three arguments.
2. What are the isomorphic types used in the unsafeCoerce?
3. Where is the function k actually evaluated in the definition of reify?

4. Where are any instances for Reifes? For example, I can run the following line in GHCi only loading Data.Reflection and Data.Proxy (and setting -XScopedTypeVariables):.

   reify (3::Int) (\(_:: Proxy q) -> print $ reflect (Proxy :: Proxy q))

5. Where/what is the phantom reified type?

6. What is the "magic" in newtype Magic?

Answer 1

Before understanding this implementation, you should understand the API. The original idea (reflecting an arbitrary pointer to the type level) is explained in this paper, which is implemented in the "slow" version of reflection. So I'll assume you already know how that works, and how the API is used. "fast" is another implementation of the same API, which uses a somewhat GHC-specific trick to speed things up. So:

1. unsafeCoerce :: a -> b is indeed applied to three arguments, which means that b must be the type of a two-argument function. In particular, the type of this unsafeCoerce is something like: Magic a r -> (Proxy s -> a) -> Proxy s -> r.

2. Heh. "isomorphic".

   More seriously: It's important to understand GHC's implementation of type classes, which involves dictionary passing. When you have something like

   class Num a where
     plus :: a -> a -> a
     negate :: a -> a
   foo :: Num a => a -> a
   foo x = plus x (negate x)
   

   It gets translated into something like

   data Num a = Num { plus :: a -> a -> a, negate :: a -> a }
   foo :: Num a -> a -> a
   foo dict x = plus dict x (negate dict x)
   

   With GHC figuring out which dictionary to pass in based on the type when you use foo. Note how a one-argument function turned into a two-argument function.

   So the implementation of a type class is to pass an extra dictionary argument. But note that as an optimization, we can use newtype instead of data when the class only has one method. E.g.

   class Default a where
     def :: a
   doubleDef :: Default a => (a, a)
   doubleDef = (def, def)
   

   turns into

   newtype Default a = Default { def :: a }
   doubleDef :: Default a -> (a, a)
   doubleDef dict = (def dict, def dict)
   

   But this generated def is operationally unsafeCoerce.

3. Magic k is k, just with a different type. So the function unsafeCoerce (Magic k) is the function k, with its type modified. It's all the same function.

4. So let's think about how this class gets compiled (I'm going to switch to Proxy with a capital P to simplify things).

   class Reifies s a | s -> a where
     reflect :: Proxy s -> a
   foo :: Reifies s a => ...
   

   turns into

   newtype Reifies s a = Reifies { reflect :: Proxy s -> a }
   foo :: Reifies s a -> ...
   -- which is unsafeCoerce-compatible with
   foo :: (Proxy s -> a) -> ...
   

   So, operationally,

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

   is unsafeCoerce-compatible with

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

5. So now we can see how this works:

   reify gets two arguments, a value :: a and a function :: forall s. Reifies s a => Proxy s -> r. Since the function is conveniently the same shape as Magic, we turn it into a value :: Magic a r. Operationally, Magic a r is roughly the same thing as forall s. (Proxy s -> a) -> Proxy s -> r, so we can cross our fingers and unsafeCoerce it. Of course, (Proxy s -> a) -> Proxy s -> r is isomorphic to a -> r, so we just need to pass in the right function (const a) and Proxy value, and we're done.

6. The magic was in your function all along.

Answer 2

shachaf's answer is not only better than mine but also correct, however I'm keeping my thoughts here for posterity.

---

This is way above me, but here is my answer anyhow.

1. Magic is a constructor of 2 parameters, and unsafeCoerce is coercing Magic k, which is of type r -> Magic a r to the type of const a. What it's doing here is coercing a function to be from one type to another. So the third 'argument' to unsafeCoerce I suspect is actually the argument being passed to the result of the unsafeCoerce (Magic k :: Magic a r) (const a)
2. It looks like most of the black magic is in the fact that there are no instances of Reifies defined, and the constructor uses an existential type. The way that existential type is actually occupied appears to occur via the unsafeCoerce.
3. It's defined in the coersion of the constructor to the same as being of type const a. This bit I understand the least.
4. The instances don't exist as far as I can tell - the existential type appears to be occupied by virtue of unsafeCoerce convincing the type system that, whether any instances exist or not, that a value of type Magic a r has been created. Whether that type exists or not, it appears to have been "forged" into existence, as in forgery, not as in metalworking.
5. The first parameter to Magic is the reified type as a Proxy, I think.
6. The magic in the newtype Magic is in this bit: (forall (s :: *). Reifies s a => Proxy s -> r) That's the type of the thing Magic wraps around. It specifies that the argument to Proxy, s, is an existential type of Reifies, or so to speak, the only fact the typesystem knows about it is that it is an instance of Reifies. So it knows that whatever s is, it must be an instance of Reifies and it can use that instance, but that's all it can do. It is like the type system has scrubbed all other knowledge of what that type is, and only knows that for the value the Proxy holds, it can use the function reflect on it - and that's it. But reflect recovers the value and type because the type was encoded in Magic and reflect appears to be just an unsafeCoerce of the function const a. Or at least, that's what I gather.

This may be totally wrong, but that seems to be how the pieces glue together. Or at least, how it made sense to me.