Czy możliwe jest zaimplementowanie sztuczki Data.Reflection za pomocą rodzin typów zamiast podpowiedzi?

Question

Implementacja GHC Data.Reflection z pakietu wykorzystuje sztuczkę obejmującą unsafeCoerce, która wykorzystuje sposób, w jaki GHC kompiluje typologie przy użyciu przekazywanych słowników. Realizacja jest krótki, więc mogę odtworzyć go w całości tutaj:

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 

To sprawia, że ​​możliwe zreifikować wartość na poziomie typu, a następnie odbić go z powrotem:

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

jestem zainteresowany w stosowaniu tej techniki, ale pomyślałem, że byłoby wygodne dla moich celów korzystania rodzinę typ z Reifies zamiast zależności funkcjonalnej, więc próbowała przepisać realizacji przy użyciu zwykłych transformacja:

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 

Niestety, to już nie działa! To zmienia kompilację na tyle znacząco, aby przełamać unsafeCoerce trick:

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

Jednak nie jestem wystarczająco zaznajomieni z jak działa GHC zrozumieć dlaczego. Czy możliwe jest zaimplementowanie Data.Reflection przy użyciu skojarzonego typu zamiast zależności funkcjonalnej? Jeśli tak, to co trzeba zmienić? Jeśli nie, dlaczego nie?

Answer 1

unsafeCoerce trik wykorzystuje fakt, że

Reifies s a => Proxy s -> r 

ma dokładnie taką samą reprezentację, w czasie wykonywania, jak

a -> Proxy s -> r 

Poprzez rozszerzenie ograniczenia do (Reifies s a, a ~ Reflects s), naruszenia ta krytyczna założenie. Istnieje kilka sposobów, aby to naprawić. Oto jeden:

{-# 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) 

---

Oto wersja bliżej Ciebie:

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