Haskell 的 DataKinds 扩展是什么? [英] What is the DataKinds extension of Haskell?

问题描述

我试图找到对 DataKinds 扩展的解释，这对我来说很有意义，因为我只阅读了Learn You a Haskell.有没有一个标准来源可以让我对我所学到的一点点有意义?

I am trying to find an explanation of the DataKinds extension that will make sense to me having come from only having read Learn You a Haskell. Is there a standard source that will make sense to me with what little I've learned?

例如文档说

使用 -XDataKinds，GHC 会自动提升每种合适的数据类型是一种，它的(值)构造函数是类型构造函数.以下类型

With -XDataKinds, GHC automatically promotes every suitable datatype to be a kind, and its (value) constructors to be type constructors. The following types

并给出例子

data Nat = Ze | Su Nat

产生以下种类和类型构造函数:

give rise to the following kinds and type constructors:

Nat :: BOX
Ze :: Nat
Su :: Nat -> Nat

我没听明白.虽然我不明白 BOX 是什么意思，但是语句 Ze :: Nat 和 Su :: Nat ->Nat 似乎说明了 Ze 和 Su 是正常数据构造函数的正常情况，正如您期望看到的 ghci

I am not getting the point. Although I don't understand what BOX means, the statements Ze :: Nat and Su :: Nat -> Nat seem to state what is already normally the case that Ze and Su are normal data constructors exactly as you would expect to see with ghci

Prelude> :t Su
Su :: Nat -> Nat

推荐答案

好吧，让我们从基础开始

Well let's start with the basics

Kinds 就是类型的类型*，例如

Kinds are the types of types*, for example

Int :: *
Bool :: *
Maybe :: * -> *

请注意，-> 在种类级别也被重载以表示功能".所以 * 是一种普通的 Haskell 类型.

Notice that -> is overloaded to mean "function" at the kind level too. So * is the kind of a normal Haskell type.

我们可以让 GHCi 用 :k 打印某种东西.

We can ask GHCi to print the kind of something with :k.

现在这不是很有用，因为我们无法制作自己的种类！使用DataKinds，当我们写

Now this not very useful, since we have no way to make our own kinds! With DataKinds, when we write

 data Nat = S Nat | Z

GHC 将促进此创建相应的种类 Nat 和

GHC will promote this to create the corresponding kind Nat and

 Prelude> :k S
 S :: Nat -> Nat
 Prelude> :k Z
 Z :: Nat

所以 DataKinds 使种类系统具有可扩展性.

So DataKinds makes the kind system extensible.

让我们用 GADTs 做原型种类的例子

Let's do the prototypical kinds example using GADTs

 data Vec :: Nat -> * where
    Nil  :: Vec Z
    Cons :: Int -> Vec n -> Vec (S n)

现在我们看到我们的 Vec 类型是按长度索引的.

Now we see that our Vec type is indexed by length.

这是基本的 10k 英尺概览.

That's the basic, 10k foot overview.

* 这实际上还在继续，Values : Types : Kinds : Sorts ... 一些语言(Coq、Agda ..)支持这个无限的宇宙堆栈，但 Haskell 将所有东西归为一类.

* This actually continues, Values : Types : Kinds : Sorts ... Some languages (Coq, Agda ..) support this infinite stack of universes, but Haskell lumps everything into one sort.

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