2017-12-09 25 views
7

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:Czy możliwe jest zaimplementowanie sztuczki Data.Reflection za pomocą rodzin typów zamiast podpowiedzi?

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?

Odpowiedz

6

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 
+0

Po pisałem to pytanie, Zerknąłem na rdzeniu i odkrytych, ku mojemu zaskoczeniu, że równości typu mają świadków uruchomieniowe przynajmniej na poziomie podstawowym. Czy są jakieś informacje o tym, jak działają świadkowie ds. Równości? Czy mogę (nie tylko) zapewnić coś innego zamiast świadka równości? Zmieniając nieco mój kod do "unsafeCoerce (Magic k :: Magic a r) (const a)() działa Proxy", ale obawiam się, że to nie zawsze działa. –

+0

@AlexisKing, to dobre pytanie, na które nie znam odpowiedzi. – dfeuer

+0

@AlexisKing, inna opcja (jak sądzę) może polegać na "odbiciu" zwracającym GADT dającym dowód, że 'a ~ odzwierciedla s'. Nie przepracowałem tego jeszcze. – dfeuer

Powiązane problemy