Haskell 的 DataKinds 扩展是什么？

Question

我试图找到对 DataKinds 扩展的解释，这对我来说是有意义的，因为我只阅读了Learn You a Haskell。有没有一个标准的资源对我来说是有意义的？

编辑：例如documentation 说

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

并举例说明

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

Answer 1

让我们从基础开始

种类

种类是类型*的类型，例如

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

请注意，-> 也被重载为类型级别的“功能”。所以* 是一种普通的 Haskell 类型。

我们可以要求 GHCi 打印带有:k 的东西。

数据种类

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

 data Nat = S Nat | Z

GHC 将为此创建相应的Nat 和

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

所以DataKinds 使 kind 系统可扩展。

用途

让我们使用 GADT 来做原型种类示例

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

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

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

* 这实际上还在继续，Values : Types : Kinds : Sorts ... 一些语言（Coq、Agda ..）支持这种无限的宇宙堆栈，但 Haskell 将所有内容归为一类。

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

这里我们有一个 Kind Vec :: * -> * -> *。由于您可以通过以下方式表示零长度的 Int 向量：

Vect Zero Int

你也可以声明无意义的类型说：

Vect Bool Int

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

Vec :: Nat -> * -> *

所以现在我们的Vec 获得了一个名为Nat 的DataKind，我们可以将其声明为：

datakind Nat = Zero | Succ Nat

通过引入一种新的数据类型，没有人可以声明无意义的类型，因为 Vec 现在具有更受约束的类型签名。