Haskell的DataKinds扩展是什么？

Question

我正在尝试找到一个关于DataKinds扩展的解释，以便我从只读过Learn You a Haskell的情况下理解。是否有一个标准的来源可以让我用我所学的少量知识来理解？

编辑：例如documentation中所说：

通过-XDataKinds，GHC会自动将每个适当的数据类型提升为一种(kind)，并将其(value)构造函数提升为类型构造函数。以下是示例。

data Nat = Ze | Su Nat

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

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

我不明白重点在哪里。虽然我不理解BOX是什么意思，但Ze :: Nat和Su :: Nat -> Nat这两个语句似乎已经陈述了Ze和Su是正常的数据构造函数，就像你在ghci中看到的那样。

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

- user782220

Answer 1

好的，让我们从基础知识开始

种类

种类是类型的类型，例如

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

注意，-> 在种类层面上也被重载成表示“函数”。所以*是普通 Haskell 类型的种类。

我们可以使用:k命令在 GHCi 中打印某个东西的种类。

数据种类

现在这并不是很有用，因为我们没有办法创建自己的种类！使用DataKinds后，当我们写下：

 data Nat = S Nat | Z

GHC将进行升级以创建相应的类型Nat。

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

因此，DataKind 使类型系统可扩展。

用途

让我们使用GADTs进行原型种类示例。

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

现在我们看到，我们的Vec类型是由长度索引的。

那是基本的，10,000英尺的概述。

*实际上，这还有继续，Values: Types: Kinds: Sorts ...一些语言（Coq、Agda等）支持这个无限的宇宙层次结构，但Haskell将所有内容都归为一个类别。

- Daniel Gratzer

---

这是否意味着表达式 S :: Nat -> Nat 是重载的，因为它可以引用 S 作为一个取一个类型为 Nat 的参数的数据构造函数或者引用 S 作为一个取一个种类为 Nat 的参数的类型构造函数？你的 data Vec :: Nat -> * 的例子应该改为 data Vec a :: Nat -> * 来反映 Vec 接受一个类型参数吗？ - user782220

@user782220 1. 是的 2. 不，我故意让 Vec 单态化，如果您愿意可以这样做。 - daniel gratzer

我认为在所有这些中最容易被忽视的是，如果没有DataKinds，S和Z不是类型，而只是生成类型Nat的类型构造函数。有了DataKinds，它们就成为类型，其种类为Nat。它们以前不是类型的事实意味着以前不能在类型签名中引用它们，而这正是这一切的关键所在。 - Jules

@Jules，这个评论应该是一个回答！通常情况下，当我看到使用 -XDataKinds 时，是因为某些东西需要函数签名中的构造函数（或者反过来，当您想知道如何在函数签名中放置构造函数时，- XDataKinds 是答案）。 - unhammer

“S”和“Z”不是类型，而只是产生类型“Nat”的类型构造函数，应该是产生类型为“Nat”的数据构造函数。 - stevemao

Answer 2

以下是我的观点：

考虑一个类型为长度索引向量的结构：

data Vec n a where
  Vnil  :: Vec Zero a
  Vcons :: a -> Vec n a -> Vec (Succ n) a

data Zero
data Succ a

在这里，我们有一个名为 Vec :: * -> * -> * 的类型。你可以通过以下方式表示一个长度为零的 Int 向量：

Vect Zero Int

你还可以声明无意义的类型，例如：

Vect Bool Int

这意味着我们可以在类型级别进行无类型的函数式编程。因此，通过引入数据类型，我们消除了这种歧义，并可以拥有这样一种类型：

Vec :: Nat -> * -> *

现在我们的Vec有了一个名为Nat的DataKind，我们可以声明如下：

datakind Nat = Zero | Succ Nat

通过引入一个新的数据类型，现在 Vec 拥有了一个更加严格的类型声明，这样就不会出现无意义的类型声明。

- aycanirican

---

“类型水平上的非类型化函数式编程”是一个很有见地的观察。 - dmvianna

这正是Simon Peyton Jones在他的一次讲座中所说的。请参见https://youtu.be/brE_dyedGm0?list=TLPQMTMwNTIwMjGbmPzQCvHwyQ&t=3092。 - Wong Jia Hau