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
reify
. maybe I'm missing something simple about order of evaluation, but it looks like unsafeCoerce::a->b
is applied to three arguments.unsafeCoerce
?k
actually evaluated in the definition of reify
?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))
Where/what is the phantom reified type?
newtype Magic
?Type class reflection is an extension of Haskell which makes it possible to use a value as a type class instance.
() is very often used as the result of something that has no interesting result. For example, an IO action that is supposed to perform some I/O and terminate without producing a result will typically have type IO () .
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:
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
.
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
.
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.
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)
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.
The magic was in your function all along.
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.
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)
Reifies
defined, and the constructor uses an existential type. The way that existential type is actually occupied appears to occur via the unsafeCoerce
.const a
. This bit I understand the least.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.Magic
is the reified type as a Proxy
, I think.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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With