haskell - Haskell 的 DataKinds 扩展是什么？

Question

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

编辑：例如文档说

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

并给出了例子

data Nat = Ze | Su Nat

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

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

我不明白这一点。虽然我不明白什么BOX意思，但这些陈述似乎说明了 ZeZe :: Nat和Su :: Nat -> NatSu 是正常的数据构造函数的情况，正如您期望在 ghci 中看到的那样

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

score 72 · Accepted Answer

好吧，让我们从基础开始

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

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 将所有内容归为一类。

score 52 · Accepted Answer

这是我的看法：

考虑一个长度索引的 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得到一个名为的 DataKind Nat，我们可以声明为：

datakind Nat = Zero | Succ Nat

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

2 回答 2