对DataKinds扩展感到困惑

Question

我从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) - 并且您可以使用表面语法明确选择(2)'A.

更重要的是,这不一定只发生在一个声明中.一个声明可能产生勾选的版本而另一个声明可能产生未勾选的版本; 例如

data A = B
data C = A

A将从第一个声明引入一个类型级别的后端名称,并'A从第二个声明中引入一个类型级别的后端名称.

Answer 2

{-# LANGUAGE DataKinds #-}不会改变data关键字通常的作用：它仍然创建一个类型Nat和两个值构造函数Zeroand 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