对DataKinds扩展感到困惑 [英] Confused on DataKinds extension

问题描述

我从 Haskell中的基本类型级别编程学习了Haskell的类型编程. >，但是当它引入DataKinds扩展名时，该示例似乎有些令人困惑:

I learn type programming of Haskell from Basic Type Level Programming in Haskell but when it introduce DataKinds extension, there are something seems confusing from the example:

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

现在，Nat被提升为Kind，没关系.但是Zero和Succ呢?

Now, Nat is promoted to Kind, it is okay. But how about Zero and Succ?

我尝试从GHCi获取一些信息，所以我输入:

I try to get some information from GHCi, so I type:

:kind Zero

它给出了

Zero :: Nat

没关系，Zero是类型为Nat的类型，对吗?我尝试:

that is okay, Zero is a type has kind Nat, right? and I try:

:type Zero

它仍然给出:

Zero :: Nat

表示Zero具有类型Nat，这是不可能的，因为Nat是一种类型而不是类型，对吗? Nat既是类型又是类型??

that means Zero has type Nat, that is impossible, since Nat is a kind not type, right? Does Nat is both a type and a kind ??

另一个令人困惑的事情是，上面的博客还提到，当创建Nat类型时，有两种新类型:'Zero和'Succ是自动创建的.当我再次从GHCi尝试它时:

And other confusing thing is, above blog also mentioned that, when create Nat kind, there are two new types: 'Zero and 'Succ are created automatically. When I try it from GHCi again:

:kind 'Zero

给予

'Zero :: Nat

和

:type 'Zero

给予

 Syntax error on 'Zero

好的，它证明'Zero是一种类型.但是创建'Zero和'Succ' ??

Okay, it proves that 'Zero is a type. but what is the purpose of creating 'Zero and 'Succ'??

推荐答案

在未扩展的Haskell中，声明

In unextended Haskell, the declaration

data A = B

定义两个新实体，在计算和类型级别分别为一个:

defines two new entities, one each at the computation and type level:

1. 在类型级别上，一个名为A(类型为*)的新基本类型，以及
2. 在计算级别上，一个名为B(类型为A)的新基础计算.

1. At the type level, a new base type named A (of kind *), and
2. At the computation level, a new base computation named B (of type A).

打开DataKinds时，声明

data A = B

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

now defines four new entities, one at the computation level, two at the type level, and one at the kind level:

1. 在种类级别上，新的基本种类A
2. 在类型级别上，一个新的基本类型'B(类型为A)
3. 在类型级别上，一个新的基本类型A(类型为*)，并且
4. 在计算级别，一个新的基础计算B(类型为A).

1. At the kind level, a new base kind A,
2. At the type level, a new base type 'B (of kind A),
3. At the type level, a new base type A (of kind *), and
4. At the computation level, a new base computation B (of type A).

这是我们以前拥有的严格的超集:旧的(1)现在是(3)，旧的(2)现在是(4).

This is a strict superset of what we had before: the old (1) is now (3), and the old (2) is now (4).

这些新实体说明了您描述的以下互动:

These new entities explain the following interactions you described:

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

我认为很清楚如何解释前两个.它解释的最后一个是因为'Zero是类型级别的东西-您不能要求类型的类型，而只能要求计算的类型！

I think it's clear how it explains the first two. The last one it explains because 'Zero is a type-level thing -- you can't ask for the type of a type, only the type of a computation!

现在，在Haskell中，每个出现名称的地方，从周围的语法中都可以清楚地看出该名称是要用作计算级名称，类型级名称还是种类级名称.因此，在类型级别必须在'B中包含对号是有点烦人的-毕竟，编译器知道我们在类型级别，因此不能是指未提升的计算级别B.因此，为方便起见，允许您在明确的刻度线上留下勾号.

Now, in Haskell, every place where a name occurs, it is clear from the surrounding syntax whether that name is intended to be a computation-level name, a type-level name, or a kind-level name. For this reason, it is somewhat annoying to have to include the tick mark in 'B at the type level -- after all, the compiler knows we're at the type level and therefore can't be referring to the unlifted computation-level B. So for convenience, you are permitted to leave off the tick mark when that is unambiguous.

从现在开始，我将区分后端"和表面语法"，在后端"中只有上述四个实体，它们始终是唯一的；表面语法"是您在文件中键入的内容并传递到包含歧义但更方便的GHC.使用这种术语，在表面语法中，可以编写以下内容，其含义如下:

From now on, I will distinguish between the "back end" -- where there are only the four entities described above and which are always unambiguous -- and the "surface syntax", which is the stuff you type into a file and pass off to GHC that includes ambiguity but is more convenient. Using this terminology, in the surface syntax, one may write the following things, with the following meanings:

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

这说明了您进行的首次互动(以及上面唯一一个未解释的互动):

This explains the first interaction you had (and the only one left unexplained above):

:kind Zero
Zero :: Nat

因为必须将:kind应用于类型级别的事物，所以编译器知道表面语法名称Zero必须是类型级别的事物.由于没有类型级别的后端名称Zero，因此它将尝试使用'Zero并获得成功.

Because :kind must be applied to a type-level thing, the compiler knows the surface syntax name Zero must be a type-level thing. Since there is no type-level back end name Zero, it tries 'Zero instead, and gets a hit.

怎么可能是模棱两可的?好吧，请注意，上面我们用一个声明在类型级别定义了两个个新实体.为了简化介绍，我将等式左侧和右侧的新实体命名为不同的东西.但是让我们看看如果我们稍微调整一下声明会发生什么:

How can it be ambiguous? Well, notice above that we defined two new entities at the type level with one declaration. For simplicity of introduction, I named the new entities on the left- and right-hand side of the equation different things. But let's see what happens if we just tweak the declaration slightly:

data A = A

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

We still introduce four new back end entities:

1. 种类A
2. 类型'A(类型为A)
3. 类型A(类型为*)和
4. 计算A(类型为A).

1. Kind A,
2. Type 'A (of kind A),
3. Type A (of kind *), and
4. Computation A (of type A).

哇！现在在类型级别上同时有一个'A和A.如果您在表面语法中不打勾，它将使用(3)，而不是(2)－您可以使用表面语法'A明确选择(2).

Whoops! There is now both an 'A and an A at the type level. If you leave off the tick mark in the surface syntax, it will use (3), and not (2) -- and you can explicitly choose (2) with the surface syntax 'A.

更重要的是，这不必从单个声明中全部发生.一个声明可能会产生已打勾的版本，而另一个则可能会产生未打勾的版本；例如

What's more, this doesn't have to happen all from a single declaration. One declaration may produce the ticked version and another the non-ticked version; for example

data A = B
data C = A

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

will introduce a type-level back end name A from the first declaration and a type-level back end name 'A from the second declaration.

这篇关于对DataKinds扩展感到困惑的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！