haskell - 理解 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 中搜索语法相当困难。

使用 newtype 有什么意义吗？除了避免装箱 data 之外，还使用元组声明(而不是带有两个字段的 HCons1 声明) ?

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 扩展名下可用)。

What is the '[] and (x ': xs) syntax I'm seeing?

当你看到 '构造函数前面的标记，表示他们的 promoted type-level counterparts .为了语法方便， promoted lists and tuples还只需要额外的勾号(我们仍然可以为空的类型级别列表写 '[]，为类型级别的缺点写 ':。所有这些都可以通过 DataKinds 扩展获得。

Is there any point in using a newtype declaration with a tuple (instead of a data declaration with two fields) besides avoiding boxing of HCons1?

是的，就是确保 HList有代表性 role ，这意味着您可以在 HList 之间进行强制s1。这有点过于复杂，无法仅用一个答案来解释，但这里有一个例子，说明当我们有

 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 。)

1 从技术上讲， data family 没有作用整体而言:每个人的角色可以不同 instance/ newtype - 这里我们只需要 HCons案例具有代表性，因为那是被胁迫的。 Check out this Trac ticket .