瞭解`GHC.TypeLits`

Question

我試圖圍繞GHC擴展KindSignatures和DataKinds包裹我的頭。縱觀Data.Modular包，我大致明白這

newtype i `Mod` (n :: Nat) = Mod i deriving (Eq, Ord) 

是有點相當於宣告C++模板<typename T, int N>（與構造函數只服用一種類型T的說法）。然而，看着GHC.TypeLits包，我不明白大部分發生的事情。關於這個包的任何一般性解釋都會有幫助。在此之前，問題得到儘管標記爲題外話，下面是一些具體的子問題：

• 一個KnownNat類是有道理的，有需要的功能，讓你提取從類型變量類型，但到底是什麼natVal做的，什麼是proxy類型變量？
• 您會在哪裏使用someNatVal？
• 最後，什麼是SomeNat - 類型級別數字如何未知？是不是編譯時已知的爲的類型級別編號的整點？

Answer 1

這個問題相當廣泛 - 我只會談到幾點。

proxy類型變量只是類型變量* -> *，即類型構造函數的類型。實際上，如果你有一個功能

foo :: proxy a -> ... 

你可以傳遞給它的值例如選擇proxy = Maybe和a = Int。您也可以傳遞[] Char（也寫爲[Char]）的值。或者，更常見的是，Proxy Int類型的值，其中Proxy是被定義爲

data Proxy a = Proxy 

即不攜帶任何運行信息的數據類型的數據類型（有它的單個值！），但其中攜帶編譯時信息（幻像類型變量a）。

假設N是一種類型Nat - 一個編譯時自然。我們可以寫一個函數

bar :: N -> ... 

但調用這需要我們建立N類型的值 - 這是無關緊要的。類型N的目的僅僅是攜帶編譯時信息，其運行時間值不是我們真正想要使用的。實際上，N根本沒有值，除了底部。我們可能呼叫

bar (undefined :: N) 

但是這看起來奇怪。讀這個，我們必須認識到bar它的第一個參數是懶惰的，它不會導致嘗試使用它的分歧。問題在於bar :: N -> ...類型的簽名具有誤導性：它聲稱結果可能取決於類型爲N的參數的值，但實際情況並非如此。相反，如果我們使用

baz :: Proxy N -> ... 

的意圖是明確的 - 有隻有一個運行時間值是：Proxy :: Proxy N。同樣清楚的是，N值僅在編譯時存在。

有時候，而是採用了特定Proxy N，代碼稍微推廣到

foo :: proxy N -> ... 

其達到同樣的目的，但也允許不同類型的Proxy。 （就我個人而言，我不是非常興奮的這種推廣。）

回到問題：natVal是一個函數，它只將編譯時自然轉換爲運行時值。即它將Proxy N轉換爲Int，只返回常量。

如果您使用類型模板參數來模擬編譯時自然，那麼您與C++模板的類比可能會更接近。例如。

template <typename N> struct S { using pred = N; }; 
struct Z {}; 

template <typename N> int natVal(); 
template <typename N> int natVal() { return 1 + natVal<typename N::pred>(); } 
template <>   int natVal<Z>() { return 0; } 

int main() { 
    cout << natVal<S<S<Z>>>() << endl; // outputs 2 
    return 0; 
} 

只是假裝有用於S和Z沒有公共構造：它們的運行時間值是不重要的，只是他們的編譯時間信息的事項。