瞭解HList的這個定義

Question

我對Haskell比較新，我想了解HList的定義之一。

data instance HList '[] = HNil 
newtype instance HList (x ': xs) = HCons1 (x, HList xs) 
pattern HCons x xs = HCons1 (x, xs) 

我有幾個具體的問題：

• 什麼是'[]和(x ': xs)語法我看到？它幾乎看起來像是在可變參數類型參數上的模式匹配，但是我從未見過這種語法，也不熟悉Haskell中的可變參數類型參數。我想這是GHC's Type Families的一部分，但我在鏈接頁面上看不到任何關於此的內容，而且在Google中搜索語法相當困難。

• 是否有使用帶有一個元組（而不是data聲明有兩個字段）除了避免HCons1拳擊newtype聲明任何一點？

Answer 1

首先，您缺少部分定義：data family聲明本身。

data family HList (l :: [*]) 
data instance HList '[] = HNil 
newtype instance HList (x ': xs) = HCons1 (x, HList xs) 

這被稱爲data family（下TypeFamilies擴展可用）。

pattern HCons x xs = HCons1 (x, xs) 

這是一個雙向模式（可在PatternSynonyms擴展名下獲得）。

什麼是我看到的'[]和(x ': xs)語法？

當您在構造函數前面看到'標記時，表示它們的標記爲promoted type-level counterparts。作爲一個語法上的方便，promoted lists and tuples也只需要額外的蜱（我們仍然可以編寫'[]爲類型級別利弊空類型級列表和':。所有這一切都可以通過DataKinds擴展。

是否有除了避免HCons1拳擊？

是的，這是確保HList有代表性role，在使用了元組（而不是有兩個字段的數據聲明）一newtype聲明的任何點，這意味着你可以控制ce HList s 。這是一個有點太參與只是一個答案來解釋，但在這裏是那裏的東西不要去，因爲我們希望，當我們有

data instance HList (x ': xs) = HCons x (HList xs) 

代替newtype instance（無圖案）的例子。考慮以下newtype S的都是表象等同於Int，Bool和()分別

newtype MyInt = MyInt Int 
newtype MyBool = MyBool Bool 
newtype MyUnit = MyUnit() 

回想一下，我們可以使用coerce包或自動解開這些類型。好了，我們希望能夠做同樣的事情，但對於整個HList：

ghci> l = (HCons 3 (HCons True (HCons() HNil))) :: HList '[Int, Bool, ()] 
ghci> l' = coerce l        :: HList '[MyInt, MyBool, MyUnit] 

這工作與newtype instance變種，但不是因爲角色的data instance之一。 （更多關於該here）

---

技術上，有一個data family作爲一個整體沒有任何作用：角色可以爲每個instance/newtype不同 - 這裏我們只真正需要的HCons情況具有代表性，因爲那是被強制執行的。 Check out this Trac ticket。

Answer 2

'[]

和(x ': xs)是類型級列表語法在這個意義上，DataKinds language extension allows promoting types to kinds and constructors to types;即如果k是某種，那麼'[k]也是一種，並且'[]是'[k]的一種類型，並且如果t :: k和ts :: '[k]，則t ': ts :: '[k]。一切都變了一個。

所以在HList (x ': xs)，x和xs匹配兩種類型：x相匹配的「正常」的類型的種類*（例如Int）和xs匹配的樣'[*]另一種類型的級列表。右側定義了一個（newtype）數據類型，該數據類型的構造函數HCons1的參數類型爲(x, HList xs)。

舉個例子，我們可以有

HCons1 (1, HCons1 (True, HNil)) :: HList '[Int, Bool] 

或者使用模式同義詞：

1 `HCons` True `HCons` HNil :: HList '[Int, Bool] 

我沒有一個很好的答案，您對爲什麼它表示爲第二個問題帶元組的新類型。