是否可以使用类型系列而不是fundeps来实现Data.Reflection的技巧？

Question

Data.Reflection来自reflection包的GHC实现使用了一种技巧unsafeCoerce,它利用了GHC使用字典传递编译类型类的方式.实现很简短,所以我可以在这里完整地重现它:

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

这样就可以在类型级别重新赋值,然后将其反射回来:

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

我有兴趣使用这种技术,但我认为使用类型系列Reifies而不是函数依赖项对我的目的来说很方便,所以我尝试使用通常的转换来重写实现:

class Reifies s where
  type Reflects s
  reflect :: Proxy s -> Reflects s

newtype Magic a r = 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 a k = unsafeCoerce (Magic k :: Magic a r) (const a) Proxy

然而,遗憾的是,这不再有效!这会大大改变编译,以打破这个unsafeCoerce伎俩:

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

但是,我对GHC如何解释原因并不熟悉.是否可以Data.Reflection使用关联类型而不是函数依赖项来实现？如果是这样,需要改变什么？如果没有,为什么不呢？

Answer 1

该unsafeCoerce技巧需要的事实优势

Reifies s a => Proxy s -> r

在运行时具有完全相同的表示形式

a -> Proxy s -> r

通过扩大约束(Reifies s a, a ~ Reflects s),你违反了这个关键假设.有几种方法可以解决这个问题.这是一个:

{-# language MultiParamTypeClasses, TypeFamilies, PolyKinds, KindSignatures,
       RankNTypes, ScopedTypeVariables, TypeOperators #-}
module TFReifies where
import Data.Proxy
import Unsafe.Coerce
import Data.Type.Equality

class Reifies s a where
  type Reflects s :: *
  reflect' :: proxy s -> a

reflect :: (Reifies s a, a ~ Reflects s) => proxy s -> a
reflect = reflect'


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

reify :: forall a r. a -> (forall (s :: *). (Reifies s a, a ~ Reflects s) => Proxy s -> r) -> r
reify a f = reify' a (\(p :: Proxy s) -> case unsafeCoerce Refl :: a :~: Reflects s of Refl -> f p)

这是一个离您更近的版本:

class Reifies s where
  type Reflects s :: *
  reflect :: proxy s -> Reflects s

newtype Magic a r = 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 a f = reify' a (\(p :: Proxy s) -> case unsafeCoerce Refl :: a :~: Reflects s of Refl -> f p)
  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' a k = unsafeCoerce (Magic k :: Magic a r) (const a) Proxy