Haskell中的“*”到底是什么？

Question

在 Haskell 中，（值级）表达式分为 类型，可以用:: 表示，如下所示：3 :: Int、"Hello" :: String、(+ 1) :: Num a => a -> a。类似地，类型被分类为种类。在 GHCi 中，您可以使用命令 :kind 或 :k 来检查类型表达式的种类：

> :k Int
Int :: *
> :k Maybe
Maybe :: * -> *
> :k Either
Either :: * -> * -> *
> :k Num
Num :: * -> Constraint
> :k Monad
Monad :: (* -> *) -> Constraint

有一些定义表明* 是一种“具体类型”或“值”或“运行时值”。例如，参见Learn You A Haskell。这有多真实？我们有 a few questions about kinds 顺便解决了这个话题，但如果能对 * 有一个规范和准确的解释，那就太好了。

*究竟是什么意思？它与其他更复杂的种类有什么关系？

另外，DataKinds 或 PolyKinds 扩展是否会改变答案？

Answer 1

首先，* 不是通配符！它通常也发音为“star”。

Bleeding edge note：截至 2015 年 2 月有 a proposal to simplify GHC's subkind system (in 7.12 or later)。该页面包含对 GHC 7.8/7.10 故事的精彩讨论。展望未来，GHC 可能会放弃类型和种类之间的区别，* :: *。见Weirich, Hsu, and Eisenberg, System FC with Explicit Kind Equality。

标准：类型表达式的描述。

Haskell 98 报告defines * in this context as：

符号*代表所有空类型构造函数的种类。

在这种情况下，“nullary”只是意味着构造函数不带参数。 Either 是二进制的；它可以应用于两个参数：Either a b。 Maybe 是一元的；它可以应用于一个参数：Maybe a。 Int 为空；它可以应用于 no 参数。

这个定义本身有点不完整。包含完全应用的一元、二元等类型构造函数的表达式也有种类*，例如Maybe Int :: *.

在 GHC 中：包含值的东西？

如果我们翻阅 GHC 文档，我们会发现更接近“可以包含运行时值”的定义。 GHC Commentary page "Kinds" 声明“'*' 是一种装箱值。像Int 和Maybe Float 这样的东西有一种*。”另一方面，GHC user's guide for version 7.4.1 表示* 是一种“提升类型”。 （当该部分被修改时，该段落没有保留 PolyKinds.)

盒装值和提升类型有点不同。根据GHC Commentary page "TypeType"，

一个类型被拆箱，当且仅当它的表示不是一个指针。未装箱的类型也未提升。

一个类型被提升当它有底部作为一个元素。闭包总是具有提升类型：即 Core 中的任何 let-bound 标识符都必须具有提升类型。在操作上，提升的物体是可以进入的。只有提升的类型可以与类型变量统一。

所以ByteArray#，原始内存块的类型，是装箱，因为它表示为一个指针，但unlifted，因为底部不是一个元素。

> undefined :: ByteArray#
Error: Kind incompatibility when matching types:
   a0 :: *
   ByteArray# :: #

因此，旧用户指南的定义似乎比 GHC 评论中的定义更准确：* 是 提升 类型。（相反， # 是那种 unlifted 类型。）

请注意，如果类型* 总是被提升，对于任何类型t :: *，您可以使用undefined :: t 或其他一些机制来构造一个“值”来创建底部。因此，即使像 Void 这样的“逻辑上无人居住”的类型也可以有一个值，即底部。

所以看起来，是的，* 代表可以包含运行时值的类型，如果 undefined 是您对运行时值的想法。 （我不认为这不是一个完全疯狂的想法。）

GHC 扩展？

有几个扩展使善良系统活跃了一点。其中一些是平凡的：KindSignatures 让我们编写种类注解，就像类型注解一样。

ConstraintKinds 添加了Constraint 类型，大致就是=> 左侧的类型。

DataKinds 让我们引入除了* 和# 之外的新类型，就像我们可以通过data、newtype 和type 引入新类型一样。

使用DataKinds，每个data 声明（可能适用条款和条件）都会生成一个提升的种类声明。所以

 data Bool = True | False

介绍常用的值构造函数和类型名称；此外，它还产生一个新的种类，Bool，以及两种类型：True :: Bool 和False :: Bool。

PolyKinds 引入了种类变量。这只是一种说“对于任何类型k”的方式，就像我们在类型级别说“对于任何类型t”一样。至于我们的朋友* 以及它是否仍然意味着“具有值的类型”，我想你可以说一个类型t :: k 其中k 是一种类型的变量可以包含值，如果@987654376 @ 或k ~ #。

Answer 2

在 kind 语言的最基本形式中，只有 kind * 和 kind 构造函数 ->，那么 * 是可以与值处于 type-of 关系的那种东西;没有任何不同种类的东西可以是一种值。

存在用于对值进行分类的类型。出于类型检查的目的，所有具有相同类型的值都是可互换的，因此类型检查器只需要关心类型，而不是特定的值。所以我们有所有实际值所在的“值级别”，以及它们的类型所在的“类型级别”。 “type-of”关系形成两个级别之间的联系，单一类型是（通常）许多值的类型。 Haskell 使这两个级别非常明确。这就是为什么你可以有像data Foo = Foo Int Chat Bool这样的声明，你已经声明了一个类型级别的东西Foo（一个类型为*的类型）和一个值级别的东西Foo（一个类型为Int -> Char -> Bool -> Foo的构造函数） .所涉及的两个Foos 只是指代不同级别的不同实体，而 Haskell 将它们完全分开，以至于它总能分辨出您所指的级别，因此可以允许（有时令人困惑）不同级别的事物具有同名。

但是，一旦我们引入本身具有结构的类型（例如 Maybe Int，这是一个类型构造函数 Maybe 应用于类型 Int），那么我们就有了在类型级别存在但不存在的东西实际上与任何值都有一种类型的关系。没有类型只是Maybe 的值，只有Maybe Int 类型的值（以及Maybe Bool、Maybe ()，甚至Maybe Void 等）。因此，我们需要对类型级别的事物进行分类，原因与我们需要对值进行分类的原因相同；只有某些类型表达式实际上代表了可以作为值类型的东西，但它们中的许多可以互换地用于“种类检查”（无论它是值级别事物的 正确 类型）它被声明为的类型是不同级别的问题）。¹

所以*（通常发音为“type”）是基本类型；它是所有类型级别的东西，可以说是值的类型。 Int 有值；因此它的类型是*。 Maybe 没有值，但它接受一个参数并产生一个有值的类型；这让我们有点像___ -> *。我们可以通过观察Maybe的参数作为出现在Just a中的值的类型来填空，所以它的参数也必须是值的类型（类型为*），所以@ 987654346@必须有种* -> *。以此类推。

当您处理只涉及星形和箭头的种类时，只有种类 * 的类型表达式才是值的类型。任何其他类型（例如* -> (* -> * -> *) -> (* -> *)）仅包含其他“类型级实体”，它们不是包含值的实际类型。

PolyKinds，据我所知，并没有真正改变这张图片。它只允许您在种类级别进行多态声明，这意味着它向我们的种类语言添加了变量（除了星形和箭头）。所以现在我可以考虑类型级别的东西k -> *；这可以实例化为* -> * 或(* -> *) -> * 或(* -> (* -> *)) -> *。我们获得了与 (a -> b) -> [a] -> [b] 在类型级别获得我们获得的完全相同的力量；我们可以编写一个包含变量类型的map 函数，而不必分别编写每个可能的映射函数。但是仍然只有一种包含类型级别的东西，即值的类型：*。

DataKinds 还为亲切的语言引入了新事物。实际上，它的作用是让我们声明包含新类型级实体的任意新类型（就像普通的data 声明允许我们声明包含新值级实体的任意新类型一样）。但是它不允许我们用所有 3 个级别的实体的对应关系来声明事物；如果我有 data Nat :: Z | S Nat 并使用 DataKinds 将其提升到 kind 级别，那么我们在类型级别上存在两个名为 Nat 的不同事物（作为 value-level Z 的类型，S Z 、S (S Z) 等），以及在种类级别（如 type-level Z、S Z、S (S Z) 的种类）。 type-level Z 虽然不是任何值的类型； 值 Z 存在于类型级别 Nat（这又是一种*），而不是类型级别Z。所以DataKinds 在 kind 语言中添加了新的用户定义的东西，它可以是类型级别的新的用户定义的东西，但仍然是唯一可以作为值类型的类型级别的东西是那种*。

我知道真正改变这种语言的唯一补充是@ChristianConkle 的回答中提到的类型，例如#（我相信现在还有更多？我不是非常了解“低级”类型，例如ByteArray#）。这些类型的类型具有 GHC 需要知道以区别对待的值（例如不假设它们可以被装箱和延迟评估），即使涉及多态函数，所以我们不能只附加它们需要的知识区别对待这些值的类型，否则在对它们调用多态函数时会丢失。

---

¹ 因此，“类型”这个词可能有点令人困惑。有时它用于指代与价值级别的事物实际上处于类型关系的事物（这是人们说“Maybe 不是类型，而是类型构造函数”）。有时它用于指代存在于类型级别的任何事物（在这种解释下，Maybe 实际上是一种类型）。在这篇文章中，我试图非常明确地提及“类型级别的事物”，而不是使用“类型”作为简写。

Answer 3

对于尝试了解种类的初学者（您可以将它们视为类型的类型），我推荐Learn you a Haskell 书中的这一章。

我个人认为种类是这样的：

你有具体的类型，例如Int、Bool、String、[Int]、Maybe Int 或 Either Int String。

所有这些都有*。为什么？因为它们不能再接受任何类型作为参数；一个Int，是一个Int； Maybe Int 是 Maybe Int。不过，Maybe 或 [] 或 Either 呢？

当你说Maybe 时，你没有具体的类型，因为你没有指定它的参数。 Maybe Int 或 Maybe String 不同，但都有 * 种类，但 Maybe 正在等待种类类型 * 返回种类 *。为了澄清，让我们看看 GHCI 的 :kind 命令可以告诉我们什么：

Prelude> :kind Maybe Int
Maybe Int :: *
Prelude> :kind Maybe
Maybe :: * -> *

列表也一样：

Prelude> :k [String]
[String] :: *
Prelude> :k []
[] :: * -> *

Either 呢？

Prelude> :k Either Int String
Either Int String :: *
Prelude> :k Either Int
Either Int :: * -> *

您可以直观地将Either 视为一个接受参数的函数，但参数是类型：

Prelude> :k Either Int
Either Int :: * -> *

表示Either Int 正在等待类型参数。