如何理解Haskell中的"Proxy Argument Trick"?

01-11

這個應該算做是一種實現技巧，或者pattern? 貌似沒什麼資料很深入地介紹這個東西，目前找到的講得比較多的是這篇SO鏈接(Haskell: Why use Proxy?)
感覺能明白它起什麼用途，但還是沒能完全理解其本質，好處究竟體現在什麼地方？
另外，這裡提到的(http://www.seas.upenn.edu/~cis552/lectures/stub/Persistent.html) Proxy用法好像比較特別點。

評論：只且僅當一個類型的kind為*時，這個類型之下才有值。Proxy譯為代理類型，定義為：

data Proxy (a :: k) = Proxy

意思是說這個類型的值不重要，重要的是類型，它是一個類型的容器，作用就是把類型信息以Proxy這個「無意義」的值在函數中傳遞，這個值是沒有有的，其中的類型的kind可以為實體kind，即kind為*的kind，可以為多態kind，比如k1 -&> *或者(* -&> *)

&> :m +Data.Proxy Data.Typeable &> asProxyTypeOf 4 (Proxy :: Proxy Double) 4.0

正常我們需要寫

&> 4 :: Double

而現在我們把這個 Double的類型信息以值的形式顯式傳入了，Proxy的作用就傳遞類型，無論它是被用在了type family里還是type class中。比如Typeable類型類定義為：

class Typeable a where typeOf :: a -&> TypeRep

會有什麼問題？instance Typeable Int或者Bool、Char都是Ok的，那kind為 * -&> *的Maybe怎麼辦？所有之前就有了：

class Typeable1 t where typeOf1 :: t a -&> TypeRep

那kind為* -&> * -&> *的Either怎麼辦？所以又有了

class Typeable2 t where typeOf2 :: t a b -&> TypeRep

然後依次類推。顯然這對Haskell是不可接受的。

那怎麼辦？我們的類型可能是各種kind，所以需要是：

class Typeable (t :: k) where typeOf :: t -&> TypeRep

但是這是不可能的，因為t的kind可能為* -&> *，這樣的類型是沒有值的，是不能寫在類型簽名里的。這時Proxy的作用就來了，把t包起來，就會得到一個kind為*的類型。所以只要寫成：

class Typeable (t :: k) where typeOf :: Proxy t -&> TypeRep

這樣就可以處理任何kind的類型了。

所以，Proxy類型相當於一個媒介，把值與類型連接起來，這樣我們就可以在函數定義里傳遞類型

id" :: Proxy t -&> t -&> t id" p t = asProxyTypeOf t p

&> id" (Proxy :: Proxy Int) 5 5

這種把類型當為參數輸入id"就是其實System F的工作方式：

{-# OPTIONS_GHC -ddump-simpl #-}

id"" :: t -&> t id"" x = x

id"" :: forall t_aSl. t_aSl -&> t_aSl [GblId, Arity=1, Caf=NoCafRefs, Str=DmdType] id"" = (@ t_aSt) (x_aSm :: t_aSt) -&> x_aSm

其中的@ t_aSt就是id函數的類型，在運行的時候類型是顯示傳遞的：

( (@ t_aSt) (x_aSm :: t_aSt) -&> x_aSm) @Int 5 = ((x_aSm :: Int) -&> x_aSm) 5 = 5

有了Proxy我們的id"可以做類似的事情。

再或者：

&> :m +GHC.TypeLits &> natVal (Proxy :: Proxy 2) &> 2

你看見了么？Proxy 2可是類型，不是值，我們把類型中的2讀成值了。

綜上，Proxy是連接值與類型的橋樑。如果在DP語言里就不會有這種東西了。

有時候，程序員需要指定表達式的類型以確定表達式的結果

比如 read :: String -&> a

在調用Read的時候，如果上下文無法推斷其類型則手工標註

比如 read "123" :: Int

現在的問題是：手工標註類型把類型寫死了，怎樣把類型作為一個參數傳遞給函數，實現參數化的類型呢？

在某些語言（比如coq，agda）裡面，類型是可以直接作為「第一級」參數直接傳遞給函數的，而 Haskell 從一開始就把函數分成值上的函數和類型上的函數，因此對於多態函數來說，類型是一個「不可見」的「隱式」的參數

比如 id 函數，在agda裡面可以這樣，

id : {A : Set} → A → A

id {A} a = a

id的參數a的類型A是直接作為參數輸入的

但是在Haskell裡面id是這樣，參數b的類型a是隱式的，直接由參數b所推導而來

id :: a -&> a

id b = b

因此在Haskell裡面要繞個彎，使用 undefined 這個可以為任意類型的特殊的值，通過 undefined 把類型作為參數傳遞過去，這樣就可以定義一個新的多態函數了，比如read可以這樣

polyRead :: (Read b) =&> String -&> b -&> b

polyRead s ty = read s

prt1 = polyRead "123" (undefined :: Int)

現在新的問題是，undefined 其上所攜帶的類型參數是有限制的，其kind必須為*。因為在 (-&>) 類型構造子兩邊，只能是Kind為 * 的類型。也即是，undefined 不可以是 Maybe 或者 Either 這種 (* -&> *), (* -&> * -&> *) 類型，可是很多時候，這樣的類型作為參數非常合理，因此有必要擴展undefined的容納能力

所以出現了Proxy，你可以把它視為undefined的Kind多態版本

為了滿足 (-&>) 的Kind約束，Proxy值構造子的類型是Proxy t，t可以為任意Kind的類型

但不管t是什麼Kind，Proxy t的Kind總是*

newtype ExamPass = ExamPass Bool deriving (Show)

type DoYouLoveMe = Maybe Bool

-- 以下a的kind可以是*，也可以是(*-&>*)

class YesOrNo a where

yn :: Bool -&> Proxy a -&> String

instance YesOrNo ExamPass where

yn b p = show $ ExamPass b

instance YesOrNo Maybe where

yn b p = show $ Just b

ynt1 = yn True (Proxy :: Proxy ExamPass)

ynt2 = yn True (Proxy :: Proxy Maybe)

總結

01 因為Haskell裡面沒有「顯式」的類型參數，所以我們要通過undefined來把類型作為參數傳入

02 因為undefined的類型限制為Kind *，所以要加一個升級版Proxy，實現多態Kind

歡迎討論