对DataKinds扩展感到困惑

Question

我从《在Haskell中学习类型编程》了解到了Haskell的类型编程，但当介绍DataKinds扩展时，有些例子似乎令人困惑：

{-# LANGUAGE DataKinds #-}
data Nat = Zero | Succ Nat

现在，Nat 已经被提升为 Kind，没问题。但是 Zero 和 Succ 呢？

我试图从 GHCi 中获取一些信息，所以我输入了：

:kind Zero

IT技术提供了

Zero :: Nat

没问题，Zero是一种类型，属于Nat类型，对吗？我试了一下：

:type Zero

它仍然会给出：

Zero :: Nat

这意味着Zero有类型Nat，但这是不可能的，因为Nat是一种而不是类型，对吧？Nat是类型和种类两者兼备吗？

还有一个令人困惑的问题是，在上面的博客中也提到，创建Nat种类时，会自动创建两个新类型：'Zero和'Succ。当我再次尝试从GHCi执行它时：

:kind 'Zero

提供

'Zero :: Nat

并且

:type 'Zero

提供

 Syntax error on 'Zero

好的，这证明了'Zero'是一种类型。但是创建'Zero'和'Succ'的目的是什么？

- JoeChoi

Answer 1

在未扩展的 Haskell 中，声明

data A = B

定义了两个新实体，一个在计算级别，一个在类型级别：

1. 在类型级别上，定义了一个名为A的新基础类型（kind为*），
2. 在计算级别上，定义了一个名为B的新基础计算（类型为A）。

当您开启 DataKinds 时，该声明生效。

data A = B

现在定义了四个新实体，一个在计算级别，两个在类型级别和一个在类别级别：

1. 在类别级别，有一个新的基本类别 A，
2. 在类型级别，有一个新的基本类型 'B（属于类别 A），
3. 在类型级别，有一个新的基本类型 A （属于类别 *），以及
4. 在计算级别，有一个新的基本计算 B（类型为 A）。

这是我们之前拥有的严格超集：旧的 (1) 现在是 (3)，旧的 (2) 现在是 (4)。

这些新实体解释了您所描述的以下交互作用：

:type Zero
Zero :: Nat
:kind 'Zero
'Zero :: Nat
:type 'Zero
Syntax error on 'Zero

我认为它很清楚地解释了前两个。它解释了最后一个的原因是因为'Zero是一种类型级别的东西——你不能询问一个类型的类型，只能询问一个计算的类型！

现在，在Haskell中，每当一个名称出现时，从周围的语法中就可以清楚地知道该名称是计算级别的名称、类型级别的名称还是种级别的名称。因此，必须在类型级别上包含'B中的撇号，这有点麻烦——毕竟，编译器知道我们处于类型级别，因此不能引用未提升的计算级别的B。因此，为了方便起见，当这是明确的时候，可以省略撇号。

从现在开始，我将区分“后端”——那里只有上述四个实体，而且始终不含歧义——和“表面语法”，即您键入到文件中并传递给GHC的东西，包括歧义，但更方便。使用这个术语，可以写出以下内容，具有以下含义：

Surface syntax    Level           Back end
Name              computation     Name
Name              type            Name if that exists; 'Name otherwise
'Name             type            'Name
Name              kind            Name
---- all other combinations ----  error

这解释了你所经历的第一个互动（也是上面未解释的唯一一个）：

:kind Zero
Zero :: Nat

由于:kind必须应用于类型级别的事物，编译器知道表面语法名称Zero必须是类型级别的事物。由于没有类型级别的后端名称Zero，它尝试使用'Zero，并成功匹配。

那么它为什么会出现歧义呢？好的，注意上面我们通过一次声明在类型级别定义了两个新实体。为了方便介绍，我给等式左右的新实体命名不同的内容。但如果我们稍微调整一下声明，会发生什么呢：

data A = A

我们仍然引入了四个新的后端实体:

1. 类型为 A 的种类 A,
2. 类型为 A（属于种类为 A）的类型 'A,
3. 类型为 * 的种类 A 的类型 A，以及
4. 类型为 A 的计算 A。

糟糕！在类型层面上现在有一个 'A 和一个 A。如果在表面语法中省略了撇号，它将使用(3)，而不是(2) -- 您可以通过表面语法 'A 明确选择 (2)。

更重要的是，这不必全部发生在单个声明中。一条声明可以生成带撇号的版本，另一条声明可以生成不带撇号的版本；例如：

data A = B
data C = A

本文将介绍第一个声明中的类型级后端名称A和第二个声明中的类型级后端名称'A。

- Daniel Wagner

---

谢谢你的回答，这里的棘手之处在于编译器尝试在类型级别中使用 :kind 'Zero 而不是 :kind Zero。每当名称 Zero 出现在类型级别中时，编译器都会将其替换为 'Zero？ - JoeChoi

@JoeChoi 不是“任何时候”，正如我在答案中所解释的那样：编译器首先检查Zero是否存在，只有当它不存在时才会检查'Zero是否存在。 - Daniel Wagner

@JoeChoi 我已经添加了一些关于这个问题的精度，区分了后端，其中名称始终是不含糊的，以及我们用来与编译器通信的表面语法。特别是请参阅以“Surface syntax Level Back end”开头的新ASCII艺术表。在这种术语下，表面语法Zero可能对应于后端的Zero或'Zero，具体取决于何种声明在范围内。 - Daniel Wagner

非常感谢！现在我终于明白为什么在leftaroundabout的答案中添加data Zero声明会导致名称冲突，如果不使用'Zeor而是使用Zero。 - JoeChoi

Answer 2

{-# LANGUAGE DataKinds #-}并不改变data关键字通常的作用：仍然会创建一个类型Nat和两个值构造器Zero和Succ。这个扩展的作用是允许您将此类类型用作种类，并将值用作类型。

因此，如果您在类型级别表达式中使���Nat，则它将仅将其用作单调乏味的Haskell98类型。只有在您在明确定义的kind-level表达式中使用它时，您才会获得种类版本。

因此，自动提升有时可能会导致名称冲突，这就是我认为引入'语法的原因：

{-# LANGUAGE DataKinds #-}
data Nat = Zero | Succ Nat
data Zero

现在，Zero本身是纯（空）数据类型Zero :: *，因此

*Main> :k Zero
Zero :: *

原则上，由于 DataKinds 的存在，Zero 现在也是从值构造器 Zero :: Nat 提升出来的一种类型，但这被 data Zero 遮盖了。因此引用语法总是指向提升的类型而不是直接定义的类型：

*Main> :k 'Zero
'Zero :: Nat

- leftaroundabout

---

冲突在(a,b) :: *与'(a,b) :: (*, *)之间也特别明显。对于[a] :: *与'[a] :: [*]也是如此（即使这些是特殊的语法情况）。 - chi

@leftaroundabout 谢谢你的回答，这是否意味着当上下文需要 Nat 作为一种类型时，Nat 就是类型，而 Zero 和 Succ 则是构造函数。而当上下文需要 Nat 作为一种种类时，Nat 就变成了种类，而 Zero 和 Succ 变成了类型？否则，我仍然不明白为什么我们需要 'Zero。在什么情况下，你在回答中提到的冲突会发生？ - JoeChoi

@JoeChoi 是的，你所说的一切都是正确的。但是你的问题让我感到困惑；难道答案不已经给出了一个明确的例子，说明名称冲突可能发生吗？ - Daniel Wagner

@JoeChoi 这是因为我定义了一个名为 Zero 的数据类型和一个名为 Zero 的值构造函数，所以它们发生了冲突。在正常的 Haskell2010 中，它们不会发生冲突，因为类型级语言和值级语言是完全分离的，但 -XDataKinds 将值级别的 Zero “复制”到类型级别的语言中，因此在类型级别上下文中，Zero 现在是有歧义的。为了防止 DataKinds 破坏任何现有代码，他们将其默认为 Haskell2010 的含义，即 Zero :: *。因此，要同时访问晋升到类型的值级构造函数的新含义，我们需要使用 ' 语法。 - leftaroundabout

@leftaroundabout 感谢您的进一步解释，我仍然无法理解，也许我需要花更多的时间来学习它。 - JoeChoi