理解 HList 的这个定义答案

【问题标题】：Understanding this definition of HList理解 HList 的这个定义
【发布时间】：2017-04-29 08:19:49
【问题描述】：

我对 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 中搜索语法相当困难。
除了避免HCons1 的装箱之外，使用带有元组的newtype 声明（而不是带有两个字段的data 声明）还有什么意义？

【问题讨论】：

标签： haskell types ghc type-level-computation data-kinds

【解决方案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 也只需要额外的勾号（我们仍然可以为空类型级列表编写'[]，为类型级缺点编写':。所有这些都可以通过@987654339 获得@扩展。

除了避免HCons1 的装箱之外，使用带有元组的newtype 声明（而不是带有两个字段的数据声明）还有什么意义？

是的，这是为了确保HList 具有代表性role，这意味着您可以在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，因为角色不同。（更多关于here。）

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

【讨论】：

(l :: [*]) 是否意味着类型参数l 被限制为类型[*]？
@Textfield 没错！具有的类型参数是类型的提升列表。想一想，要编译它可能还需要打开KindSignatures，也可能需要导入Data.Kind……只要按照GHC 的建议去做。 :)

【解决方案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]

关于为什么它被表示为带有元组的新类型，我对你的第二个问题没有很好的答案。

【讨论】：