Geek Answers Handbook

Is it possible to implement the Data.Reflections trick using type families and not using drives?

Executing the GHC Data.Reflection from reflection uses a trick involving unsafeCoerce , which uses the way the GHC compiles type classes using dictionary passing. The implementation is short, so I can reproduce it in its entirety here:

 class Reifies sa | s -> a where reflect :: proxy s -> a newtype Magic ar = Magic (forall (s :: *). Reifies sa => Proxy s -> r) reify :: forall a r. a -> (forall (s :: *). Reifies sa => Proxy s -> r) -> r reify ak = unsafeCoerce (Magic k :: Magic ar) (const a) Proxy

This allows you to confirm the value at the type level, and then reflect it:

 ghci> reify (42 :: Integer) (\p -> reflect p) :: Integer 42

I was interested in using this technique, but I thought that for my purposes it would be convenient to use a type family with Reifies instead of a functional dependency, so I tried to rewrite the implementation using the usual conversion:

 class Reifies s where type Reflects s reflect :: Proxy s -> Reflects s newtype Magic ar = Magic (forall (s :: *). (Reifies s, Reflects s ~ a) => Proxy s -> r) reify :: forall a r. a -> (forall (s :: *). (Reifies s, Reflects s ~ a) => Proxy s -> r) -> r reify ak = unsafeCoerce (Magic k :: Magic ar) (const a) Proxy

Unfortunately, this no longer works! This greatly facilitates compilation to break the unsafeCoerce trick:

 ghci> reify (42 :: Integer) (\p -> reflect p) :: Integer 2199023255808

However, I am not familiar with how the GHC works to understand why. Is it possible to implement Data.Reflection using a bound type instead of a functional dependency? If so, what needs to be changed? If not, why not?

+7
haskell
source share
1 answer

The unsafeCoerce trick uses the fact that

 Reifies sa => Proxy s -> r

has exactly the same runtime view as

 a -> Proxy s -> r

Increasing the limit to (Reifies sa, a ~ Reflects s) , you violate this critical assumption. There are several ways to fix this. Here is one:

 {-# language MultiParamTypeClasses, TypeFamilies, PolyKinds, KindSignatures, RankNTypes, ScopedTypeVariables, TypeOperators #-} module TFReifies where import Data.Proxy import Unsafe.Coerce import Data.Type.Equality class Reifies sa where type Reflects s :: * reflect' :: proxy s -> a reflect :: (Reifies sa, a ~ Reflects s) => proxy s -> a reflect = reflect' newtype Magic ar = Magic (forall (s :: *). (Reifies sa) => Proxy s -> r) reify' :: forall a r. a -> (forall (s :: *). (Reifies sa) => Proxy s -> r) -> r reify' ak = unsafeCoerce (Magic k :: Magic ar) (const a) Proxy reify :: forall a r. a -> (forall (s :: *). (Reifies sa, a ~ Reflects s) => Proxy s -> r) -> r reify af = reify' a (\(p :: Proxy s) -> case unsafeCoerce Refl :: a :~: Reflects s of Refl -> fp)

Here's the version closer to yours:

 class Reifies s where type Reflects s :: * reflect :: proxy s -> Reflects s newtype Magic ar = Magic (forall (s :: *). (Reifies s) => Proxy s -> r) reify :: forall a r. a -> (forall (s :: *). (Reifies s, a ~ Reflects s) => Proxy s -> r) -> r reify af = reify' a (\(p :: Proxy s) -> case unsafeCoerce Refl :: a :~: Reflects s of Refl -> fp) where -- This function is totally bogus in other contexts, so we hide it. reify' :: forall a r. a -> (forall (s :: *). (Reifies s) => Proxy s -> r) -> r reify' ak = unsafeCoerce (Magic k :: Magic ar) (const a) Proxy
+6
source share

More articles:


All Articles