haskell - 对 DataKinds 扩展感到困惑

Question

我从Basic Type Level Programming in Haskell学习Haskell的类型编程但是当它引入 DataKinds 扩展时，示例中有些东西似乎令人困惑:

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

现在，Nat提升为Kind，没关系。但是 Zero 和 Succ 怎么样？

我尝试从 GHCi 获取一些信息，因此我输入:

:kind Zero

它给出

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'的目的是什么？？

Answer 1

在未扩展的 Haskell 中，声明

data A = B

定义了两个新实体，计算和类型级别各一个:

1. 在类型级别，名为 A 的新基本类型(属于 * 类型)，以及
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，
2. 输入'A(类型为A)，
3. 类型 A(类型 *)，并且
4. 计算A(类型为A)。

哎呀!现在，类型级别同时存在 'A 和 A。如果您在表面语法中省略勾号，它将使用 (3)，而不是 (2) - 并且您可以使用表面语法 'A 显式选择 (2)。

此外，这不必全部通过单个声明来实现。一个声明可能产生打勾版本，另一个声明可能产生非打勾版本；例如

data A = B
data C = A

将引入第一个声明中的类型级后端名称 A 和第二个声明中的类型级后端名称 'A。