haskell - Haskell 的 DataKinds 扩展是什么？

Question

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

编辑:例如 documentation说

With -XDataKinds, GHC automatically promotes every suitable datatype to be a kind, and its (value) constructors to be type constructors. The following types

并给出示例

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 使种类系统可扩展。

用途

让我们使用 GADT 来做原型(prototype)类型示例

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

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

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

* 这实际上还在继续，Values : Types : Kinds : Sorts ... 一些语言(Coq、Agda ..)支持这种无限的宇宙堆栈，但 Haskell 将所有内容集中到一种排序中。