`Data.Proxy`的目的是什麼？

Question

Proxy從Data.Proxy似乎沒有什麼比一個單純的

data Proxy s 

什麼時候需要這樣一個無人居住的類型或者更確切地說，是什麼使我不能做，否則，當它簡化事情比較到其他方法，以及它在實踐中如何使用？

Answer 1

我經常使用Proxy與其合作伙伴Data.Tagged作爲documentation表示，以避免不安全地傳遞虛擬參數。

例如，

data Q 

class Modulus a where 
    value :: Tagged a Int 

instance Modulus Q where 
    value = Tagged 5 

f x y = (x+y) `mod` (proxy value (Proxy::Proxy Q)) 

的另一種方式來寫，沒有Tagged是

data Q 

class Modulus a where 
    value :: Proxy a -> Int 

instance Modulus Q where 
    value _ = 5 

f x y = (x+y) `mod` (value (Proxy::Proxy Q)) 

在兩個例子中，我們還可以刪除Proxy類型和只是使用一個undefined :: Q在傳遞幻影類型。但是，使用未定義的是generally frowned upon，因爲如果曾經評估過該值，則可能會出現問題。考慮以下幾點：

data P = Three 
     | Default 

instance Modulus P where 
    value Three = 3 
    value _ = 5 

f x y = (x+y) `mod` (value (undefined :: P)) 

這是寫的實例有效的方式，如果我用Default構造，程序會崩潰，因爲我想評價undefined。因此，Proxy類型爲幻像類型提供了類型安全性。

編輯

卡爾指出的，Proxy另一個好處是比*其他類型的假體類型的能力。例如，我瞎搞類型列表：

{-# LANGUAGE KindSignatures, DataKinds, TypeOperators, 
    MultiParamTypeClasses, PolyKinds, FlexibleContexts, 
    ScopedTypeVariables #-} 

import Data.Tagged 
import Data.Proxy 

class Foo (a::[*]) b where 
    foo:: Tagged a [b] 

instance Foo '[] Int where 
    foo = Tagged [] 

instance (Foo xs Int) => Foo (x ': xs) Int where 
    foo = Tagged $ 1 : (proxy foo (Proxy :: Proxy xs)) -- xs has kind [*] 

toUnary :: [Int] 
toUnary = proxy foo (Proxy :: Proxy '[Int, Bool, String, Double, Float]) 

然而，由於undefined是值，它的類型必須有一種*或#。如果我想在我的例子使用undefined，我需要像undefined :: '[Int, Bool, String, Double, Float]，這會導致編譯錯誤：

Kind mis-match 
    Expected kind `OpenKind', 
    but '[Int, Bool, String, Double, Float] has kind `[*]' 

更多關於種，檢查this出來。鑑於錯誤信息，我希望能夠編寫undefined :: Int#，但我仍然得到了錯誤Couldn't match kind # against *，所以顯然這是一個糟糕的GHC錯誤信息或我的一個簡單的錯誤的情況。