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

Answer 2

{-# LANGUAGE DataKinds #-} 不会改变 data 关键字通常所做的事情：它仍然创建一个类型 Nat 和两个值构造函数 Zero 和 Succ。这个扩展的作用是，它允许你像使用种类一样使用类型，像使用类型一样使用值。

因此，如果您在类型级表达式中使用Nat，它只会将其用作无聊的 Haskell98 类型。只有在明确的 kind 级表达式中使用它时，才会得到 kind 版本。

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

{-# 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