理解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类型系列的一部分,但我在链接页面上没有看到任何相关信息,而且在Google中搜索语法相当困难.

• 除了避免拳击之外,使用newtype带有元组的声明(而不是data带有两个字段的声明)是否有任何意义HCons1？

Answer 1

首先,您缺少定义的一部分:data family声明本身.

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

这称为a data family(在TypeFamilies扩展名下可用).

pattern HCons x xs = HCons1 (x, xs)

这是双向模式(在PatternSynonyms扩展名下可用).

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

当您'在构造函数前面看到标记时,它表示它们提升的类型级别对应项.作为一种语法方便,提升列表和元组也只需要额外的滴答(我们仍然可以'[]为空类型列表和类型级别的列表编写':.所有这些都可以通过DataKinds扩展来获得.

newtype除了避免拳击之外,使用带有元组的声明(而不是带有两个字段的数据声明)是否有任何意义HCons1？

是的,这是为了确保它HList具有代表性角色,这意味着你可以在HLists ¹之间强制执行.这个问题有点过于简单,只能在答案中解释,但这里有一个例子,说明当我们拥有的东西没有按照我们想要的那样去

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

而不是newtype instance(没有模式).考虑以下newtypeS的是代表性地相当于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用于角色.(更多的是在这里.)

¹从技术上讲,没有作用的data family整体:角色可以为每个不同的instance/ newtype-在这里我们只真正需要的HCons情况下是代表性的,因为就是这样被裹挟着一个.看看这张Trac票.