哈斯克爾反射中的黑魔法

我曾希望有人能夠在Data.Reflection的黑魔法中發現一點點光芒。相關的片段是：哈斯克爾反射中的黑魔法

{-# 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。也許我錯過了簡單的評估順序，但看起來像unsafeCoerce::a->b適用於三個參數。
unsafeCoerce中使用的同構類型是什麼？
功能k在reify的定義中實際評估的功能在哪裏？
Reifes的任何實例在哪裏？例如，我可以在GHCi中運行以下行，只加載Data.Reflection和Data.Proxy（並設置-XScopedTypeVariables）:.

reify (3::Int) (\(_:: Proxy q) -> print $ reflect (Proxy :: Proxy q))
凡/什麼是幻物化類型？
newtype Magic是什麼「魔法」？

來源

2013-07-22 crockeea

在理解此實現之前，您應該瞭解API。原始想法（反映指向類型級別的任意指針）在this paper中進行了說明，該工具在reflection的「slow」版本中實現。所以我會假設你已經知道它是如何工作的，以及如何使用API。「fast」是同一個API的另一個實現，它使用GHC特有的技巧來加快速度。所以：

unsafeCoerce :: a -> b確實適用於三個參數，這意味着b必須是兩個參數的函數的類型。具體而言，此unsafeCoerce的類型類似於：Magic a r -> (Proxy s -> a) -> Proxy s -> r。
heh。「同構」。

更嚴重：瞭解GHC的類型類實現很重要，它涉及字典傳遞。當你有像
```
class Num a where 
    plus :: a -> a -> a 
    negate :: a -> a 
foo :: Num a => a -> a 
foo x = plus x (negate x) 
```
它被翻譯成類似
```
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) 
```
隨着GHC找出基於類型通過該字典，當你使用foo。注意一個單參數函數如何變成雙參數函數。

因此，類型類的實現是傳遞一個額外的字典參數。但請注意，作爲優化，當類只有一種方法時，我們可以使用newtype而不是data。例如。
```
class Default a where 
    def :: a 
doubleDef :: Default a => (a, a) 
doubleDef = (def, def) 
```
變成
```
newtype Default a = Default { def :: a } 
doubleDef :: Default a -> (a, a) 
doubleDef dict = (def dict, def dict) 
```
但這產生def可操作unsafeCoerce。

Magic k是k，只是具有不同的類型。所以功能unsafeCoerce (Magic k)是功能k，其類型已修改。這是完全相同的功能。所以我們來考慮一下這個類是如何編譯的（我將使用大寫P來切換到Proxy以簡化事情）。

class Reifies s a | s -> a where 
    reflect :: Proxy s -> a 
foo :: Reifies s a => ...

變成

newtype Reifies s a = Reifies { reflect :: Proxy s -> a } 
foo :: Reifies s a -> ... 
-- which is unsafeCoerce-compatible with 
foo :: (Proxy s -> a) -> ...

因此，操作上，

newtype Magic a r = Magic (forall s. Reifies s a => Proxy s -> r)

是unsafeCoerce兼容與

newtype Magic a r = Magic (forall s. (Proxy s -> a) -> Proxy s -> r)

所以，現在，我們可以看到這是如何工作：

reify獲取兩個參數，值:: a和函數:: forall s. Reifies s a => Proxy s -> r。由於該函數的形狀與Magic的形狀相同，因此我們將其轉化爲值:: Magic a r。操作上，Magic a r大致同樣的事情forall s. (Proxy s -> a) -> Proxy s -> r，所以我們可以越過我們的手指和unsafeCoerce它。當然，(Proxy s -> a) -> Proxy s -> r同構於a -> r，所以我們只需要在正確的函數（const a）和Proxy值傳遞，我們就大功告成了。
神奇的是你的功能一直。

來源

2013-07-22 18:34:56 shachaf

我猜B.o.B. *是正確的。 – crockeea

我仍然在消化這個答案，但是我沒有看到任何關於他缺少'reflect'的實現。 – crockeea

查看4的結尾。我們'unsafeCoerce'是一個帶有一個約束和一個參數的函數，帶有兩個參數。 – shachaf

shachaf的答案是不僅比我好，但也是正確的，但是我在這裏讓我的思念留給後人。

這是高於我，但這裏是我的答案無論如何。

Magic是2個參數的構造，並且被unsafeCoerce脅迫Magic k，這是r -> Magic a r類型的到的const a類型。它在這裏做的是強制一種功能從一種類型轉變爲另一種類型。所以第三個「說法」到unsafeCoerce我懷疑其實是被傳遞到的unsafeCoerce (Magic k :: Magic a r) (const a)
它看起來像極了黑魔法是一個事實，即有定義的構造函數使用的Reifies沒有實例，結果論證一種存在型。存在類型實際佔用的方式似乎通過unsafeCoerce發生。
它在構造函數的層次中定義爲與const a類型相同。這一點我明白至少。
據我所知，實例並不存在 - 由於unsafeCoerce說服存在類型似乎佔據了類型系統，即是否存在任何實例，因此已創建類型爲Magic a r的值。無論這種類型是否存在，它似乎都是僞造的，就像在僞造品中一樣，而不是在金屬加工中。
Magic的第一個參數是作爲Proxy的通用類型，我想。
新類型Magic中的魔法就在這個位：(forall (s :: *). Reifies s a => Proxy s -> r)這就是Magic環繞的東西的類型。它指定Proxy,s的參數是Reifies的存在類型，或者可以這麼說，類型系統知道的唯一事實是它是Reifies的實例。所以它知道無論s是什麼，它必須是Reifies的一個實例，它可以使用該實例，但這就是它的全部能力。這就像類型系統已經清除了所有類型的知識，只知道對於Proxy的值，它可以使用其上的功能reflect - 就是這樣。但reflect恢復值和類型，因爲類型編碼Magic和reflect似乎只是功能const aunsafeCoerce。或者至少，這是我收集的。

這可能是完全錯誤的，但這似乎是如何拼湊在一起。或者至少，它對我有意義。

來源

2013-07-22 17:43:16

哈斯克爾反射中的黑魔法

回答

相關問題