对 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

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

Answer 2

在未扩展的Haskell中，声明

data A = B

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

在类型级别，一个名为 A 的新基类型（属于 * 类型），以及
在计算级别，一个名为 B（类型 A）的新基础计算。

开启DataKinds时，声明

data A = B

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

在种类级别，新的基本种类 A，
在类型级别，一个新的基本类型 'B（A 类型），
在类型级别，一个新的基本类型 A（* 类型），并且
在计算级别，新的基础计算 B（类型 A）。

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

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

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

我认为它对前两个的解释很清楚。它解释的最后一个是因为 'Zero 是类型级的东西——你不能要求类型的类型，只能要求计算的类型！

现在，在 Haskell 中，每个出现名称的地方，从周围的语法中可以清楚地看出该名称是计算级名称、类型级名称还是种类- 级别名称。出于这个原因，不得不在类型级别的 'B 中包含刻度线有点烦人——毕竟，编译器知道我们处于类型级别因此不能指未提升的计算级别 B。因此，为方便起见，您可以在明确的情况下不打勾。

从现在开始，我将区分 "back end" - 只有上述四个实体并且始终明确 - 和 "surface syntax"，这是你的东西输入一个文件并传递给包含歧义但更方便的 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

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

善良A,
类型 'A（类型 A），
键入 A（类型 *），并且
计算 A（类型 A）。

糟糕！现在在类型级别有一个 'A 和一个 A。如果您在表面语法中省略刻度线，它将使用 (3) 而不是 (2) - 您可以使用表面语法 'A.

明确选择 (2)

更重要的是，这不必通过一个声明全部发生。一份声明可能会产生勾选版本，而另一份声明可能会产生非勾选版本；例如

data A = B
data C = A

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

对 DataKinds 扩展感到困惑

Confused on DataKinds extension

haskell

types

data-kinds