Haskell 的 DataKinds 扩展是什么？
我试图找到对 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
好吧，让我们从基础开始
种类
种类是类型*的类型，例如
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 将所有内容归为一类。
这是我的看法：
考虑一个长度索引的 Vector 类型：
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 现在具有更受约束的类型签名。
S :: Nat -> Nat被重载，因为它可以将S引用为采用Nat类型参数的数据构造函数或S作为采用Nat类型参数的类型构造函数？您的data Vec :: Nat -> *示例是否应该改为data Vec a :: Nat -> *以反映Vec采用类型参数？Vec单态，如果你愿意，你可以S和Z就不是类型，而只是产生类型Nat的类型构造函数。对于 DataKinds，它们是类型，其种类是Nat。它们以前不是类型的事实意味着以前它们不能在类型签名中被引用，这就是这一切的意义所在。S和Z不是类型，而只是产生类型Nat的类型构造函数”应该是产生类型Nat数据的数据构造函数