什么是Haskell的DataKinds扩展？

我试图find一个DataKinds扩展的解释，这对我来说只有阅读了学习你一个Haskell才有意义。有没有一个标准的来源，我会学到什么？

编辑：例如文档说

使用-XDataKinds，GHC会自动将每个合适的数据types提升为一种types，并将其（值）构造函数自动提升为types构造函数。以下types

并举例说明

data Nat = Ze | Su Nat

引起了以下种类和types的构造函数：

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

我没有明白这一点。虽然我不明白BOX是什么意思，但Ze :: Nat和Su :: Nat -> Nat的陈述似乎说明了Ze和Su是正常的数据构造函数，正如你期望用ghci

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

那么让我们从基础开始

种类是types的types*，例如

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

注意->重载也意味着在类层次上的“function”。所以*是一种正常的Haskelltypes。

我们可以要求GHCi打印这样的东西:k 。

现在这不是很有用，因为我们无法做出自己的种类！随着DataKinds ，当我们写

  data Nat = S Nat | Z

GHC将促进这个创造相应的Nat和

  S :: Nat -> Nat Z :: Nat

所以DataKind使类系统具有可扩展性。

我们来做一个使用GADT的原型示例

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

现在我们看到我们的Vectypes是按长度索引的。

这是基本的，10K英尺的概述。

**这实际上继续下去， Values : Types : Kinds : Sorts ...一些语言（Coq，Agda ..）支持这个无限的宇宙堆栈，但是Haskell把所有东西都归结为一类。

这是我的承担：

考虑一个长度索引types的vector：

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

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

 Vect Zero Int

你也可以声明无意义的types：

 Vect Bool Int

这意味着我们可以在types级别进行无types的函数编程。因此，我们通过引入数据types来消除这种模糊性，并且可以有这样的一种：

 Vec :: Nat -> * -> *

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

 datakind Nat = Zero | Succ Nat

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