HListのこの定義の理解

Question

私は比較的新しいHaskellです。HListの定義の1つを理解しようとしています。

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

私はカップルの具体的な質問があります。

• を私は見ている'[]と(x ': xs)構文は何ですか？ Variadic型のパラメータではパターンマッチングのように見えますが、以前はこの構文を見たことがなく、Haskellのvariadic型のパラメータにも精通していません。私はこれがGHC's Type Familiesの一部だと推測しますが、リンク先のページでこれについて何も表示されません.Googleで構文を検索するのは難しいです。

• はHCons1のボクシングを避けることに加えて（代わりに2つのフィールドを持つdata宣言の）タプルと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となります。構文の便宜上、このすべてがDataKinds拡張を介して利用可能である。promoted lists and tuplesまた、単に余分なダニを必要とする（と我々はまだ空のタイプレベルのリストとタイプレベルの短所について':ため'[]を書くことを得る。

はい、それはHListは具象的roleを持っていることを確認することですHCons1？

のボクシングを避ける以外に（代わりに、2つのフィールドを持つデータ宣言の）タプルとnewtype宣言を使用して任意のポイントは、どのありあなたが元気にできることを意味します（HLists ）の間にある。これはちょうど答えで説明するの少しも関与しているが、ここでは代わりにnewtype instance（無パターン）の

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

を持っているとき、私たちが望むようなものが行かないところの一例です。次newtype representationally Intと同等であり、S、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 1。 （その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]の場合です。すべてが1つずつシフトします。 HList (x ': xs)、xとxs試合中のSO

二つのタイプ：xは、「正常な」種類*のタイプ（例えばInt）とxsマッチ種類'[*]別のタイプレベルのリストに一致します。右側は、(x, HList xs)のパラメータを持つコンストラクタHCons1を持つ（newtype）データ型を定義します。私はそれは次のように表されている理由について、あなたの2番目の質問に良い答えを持っていない

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

：

例として

、我々は、パターン同義語を使用して、

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

を持っているか、することができますタプルを持つnewtype。