对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:
- 在类型级别上,一个名为
A
(类型为*
)的新基本类型,以及 - 在计算级别上,一个名为
B
(类型为A
)的新基础计算.
- At the type level, a new base type named
A
(of kind*
), and - At the computation level, a new base computation named
B
(of typeA
).
打开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:
- 在种类级别上,新的基本种类
A
- 在类型级别上,一个新的基本类型
'B
(类型为A
) - 在类型级别上,一个新的基本类型
A
(类型为*
),并且 - 在计算级别,一个新的基础计算
B
(类型为A
).
- At the kind level, a new base kind
A
, - At the type level, a new base type
'B
(of kindA
), - At the type level, a new base type
A
(of kind*
), and - At the computation level, a new base computation
B
(of typeA
).
这是我们以前拥有的严格的超集:旧的(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:
- 种类
A
- 类型
'A
(类型为A
) - 类型
A
(类型为*
)和 - 计算
A
(类型为A
).
- Kind
A
, - Type
'A
(of kindA
), - Type
A
(of kind*
), and - Computation
A
(of typeA
).
哇!现在在类型级别上同时有一个'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屋!