宇宙

为了简化，本书到目前为止略去了 Lean 的一个重要特性：宇宙 (Universes)。宇宙是一种对其他类型进行分类的类型。其中两个是我们熟悉的：Type 和 Prop。 Type 分类了普通类型，例如 Nat、String、Int → String × Char 和 IO Unit。 Prop 分类了可能为真或假的命题，例如 "nisse" = "elf" 或 3 > 2。 Prop 的类型是 Type：

#check Prop

Prop : Type

出于技术原因，我们需要比这两个更多的宇宙。具体而言，Type 本身不能是一个 Type。这会导致逻辑悖论的产生，并削弱 Lean 作为定理证明器的实用性。

对此的正式论证被称为 吉拉德悖论 (Girard's Paradox)。它与一个更著名的悖论有关，称为 罗素悖论 (Russell's Paradox)，该悖论用于展示早期版本的集合论是不一致的。在这些集合论中，一个集合可以通过一个属性来定义。例如，所有红色事物的集合，所有水果的集合，所有自然数的集合，甚至所有集合的集合。给定一个集合，可以询问一个给定的元素是否被包含在其中。例如，一只蓝色的鸟不会被包含在所有红色事物的集合中，但所有红色事物的集合被包含在所有集合的集合中。实际上，所有集合的集合甚至包含其自身。

那么，所有不包含自身的集合的集合呢？它包含所有红色事物的集合，因为所有红色事物的集合本身并不是红色的。它不包含所有集合的集合，因为所有集合的集合包含自身。但它是否包含自身呢？如果它包含自身，那么它就不能包含自身。但如果它不包含自身，那么它就必须包含自身。

这是一个矛盾，表明了初始的假设存在问题。具体而言，允许通过提供任意属性来构造集合的做法过于强大。集合论的后续版本限制了集合的构造以消除这种悖论。

在那些可以将类型 Type 分配给 Type的 依赖类型理论 (Dependent Type Theory) 的版本中，可以构建一个相关的悖论。为了确保 Lean 具有自洽的逻辑基础并且能够被用作数学工具，Type 需要有其他类型。这个类型称为 Type 1：

#check Type

Type : Type 1

类似地，Type 1 是一个 Type 2， Type 2 是一个 Type 3， Type 3 是一个 Type 4，等等。

函数类型占据了可以同时包含参数类型和返回类型的最小宇宙。这意味着 Nat → Nat 是一个 Type，Type → Type 是一个 Type 1，而 Type 1 → Type 2 是一个 Type 3。

这个规则有一个例外。如果一个函数的返回类型是 Prop，那么即使参数在更大的宇宙中，例如 Type 或甚至 Type 1，整个函数类型也在 Prop 中。具体而言，这意味着具有普通类型的值的谓词在 Prop 中。例如，类型 (n : Nat) → n = n + 0 表示了从一个 Nat 到它等于自身加零的证据的函数。尽管 Nat 在 Type 中，根据这个规则，这个函数类型在 Prop 中。同样，尽管 Type 在 Type 1 中，函数类型 Type → 2 + 2 = 4 仍在 Prop 中。

用户定义类型

结构体和归纳数据类型可以声明为存在于特定的宇宙中。 Lean 随后会检查每个数据类型是否通过位于足够大的宇宙中来避免悖论，从而防止它包含其自身的类型。例如，在以下声明中，MyList 被声明为驻留在 Type 中，而它的类型参数 α 也是如此：

inductive MyList (α : Type) : Type where
  | nil : MyList α
  | cons : α → MyList α → MyList α

MyList 本身是一个 Type → Type。这意味着它不能用于包含实际类型，因为那样的话它的参数将会是 Type，也就是一个 Type 1。

def myListOfNat : MyList Type :=
  .cons Nat .nil

application type mismatch
  MyList Type
argument
  Type
has type
  Type 1 : Type 2
but is expected to have type
  Type : Type 1

更新 MyList 使其参数为一个 Type 1，这会导致该定义被 Lean 拒绝：

inductive MyList (α : Type 1) : Type where
  | nil : MyList α
  | cons : α → MyList α → MyList α

invalid universe level in constructor 'MyList.cons', parameter has type
  α
at universe level
  2
it must be smaller than or equal to the inductive datatype universe level
  1

发生此错误的原因是，类型为 α 的 cons 的参数来自一个比 MyList 更大的宇宙。将 MyList 本身置于 Type 1 中可以解决这个问题，但代价是 MyList 本身在需要 Type 的内容中变得不便使用。

决定某种数据类型是否被允许的具体规则有些复杂。通常来说，最简单的方法是，从其最大的参数所属的宇宙与自身所属的宇宙相同的数据类型开始。然后，如果 Lean 拒绝了该定义，那就将其层级增加一级，这通常会奏效。

宇宙多态

在特定的宇宙中定义一个数据类型可能会导致代码重复。将 MyList 置于 Type → Type 中意味着它不能被用于实际的类型列表。将它放在 Type 1 → Type 1 内意味着它不能用于类型列表的列表。与其复制粘贴数据类型以在 Type、Type 1、Type 2 等中创建不同版本，不如使用一种称为 宇宙多态 的特性来编写单个可以在任意这些宇宙中实例化的定义。

普通的多态类型在定义中使用变量来表示类型。这使得 Lean 可以以不同的方式填充这些变量，从而使这些定义可以与各种类型一起使用。同样，宇宙多态性允许变量在定义中表示宇宙，使得 Lean 可以以不同的方式去填充它们，以便可以用于各种宇宙。正如类型参数通常用希腊字母命名一样，宇宙参数通常命名为 u、v 和 w。

MyList 的这个定义没有指定特定的宇宙层级，而是使用变量 u 来表示任意层级。如果最终的数据类型与 Type 一起使用，那么 u 是 0；如果与 Type 3 一起使用，那么 u 是 3：

inductive MyList (α : Type u) : Type u where
  | nil : MyList α
  | cons : α → MyList α → MyList α

通过这个定义，MyList 的相同定义可以用于包含实际的自然数以及自然数类型本身：

def myListOfNumbers : MyList Nat :=
  .cons 0 (.cons 1 .nil)

def myListOfNat : MyList Type :=
  .cons Nat .nil

它甚至可以包含其自身：

def myListOfList : MyList (Type → Type) :=
  .cons MyList .nil

这似乎使得写出一个逻辑悖论成为可能。毕竟，宇宙系统的全部意义在于排除自指类型。然而，在幕后，每次出现 MyList 时都会提供一个宇宙层级的参数。本质上，MyList 的宇宙多态定义在每个层级创建了数据类型的一个副本，层级参数选择要使用哪个副本。这些层级参数使用一个点和大括号书写，例如 MyList.{0} : Type → Type，MyList.{1} : Type 1 → Type 1，和 MyList.{2} : Type 2 → Type 2。

明确地写出所有层次，之前的例子变成了：

def myListOfNumbers : MyList.{0} Nat :=
  .cons 0 (.cons 1 .nil)

def myListOfNat : MyList.{1} Type :=
  .cons Nat .nil

def myListOfList : MyList.{1} (Type → Type) :=
  .cons MyList.{0} .nil

当一个宇宙多态定义接受了多个类型作为参数时，最好给每个参数赋予其自己的层级变量，以实现最大的灵活性。例如，一个带有单个层级参数的 Sum 版本可以写成如下形式：

inductive Sum (α : Type u) (β : Type u) : Type u where
  | inl : α → Sum α β
  | inr : β → Sum α β

这个定义可以在多个层级上使用：

def stringOrNat : Sum String Nat := .inl "hello"

def typeOrType : Sum Type Type := .inr Nat

但是，它要求两个参数位于同一个宇宙内：

def stringOrType : Sum String Type := .inr Nat

application type mismatch
  Sum String Type
argument
  Type
has type
  Type 1 : Type 2
but is expected to have type
  Type : Type 1

通过为两个类型参数的宇宙层级使用不同的变量，并声明生成的数据类型是两者中最大的层级，这可以使该数据类型更加灵活：

inductive Sum (α : Type u) (β : Type v) : Type (max u v) where
  | inl : α → Sum α β
  | inr : β → Sum α β

这使得 Sum 可以与来自不同宇宙的参数一起使用：

def stringOrType : Sum String Type := .inr Nat

在 Lean 需要宇宙层级的位置，以下任意一种都是被允许的：

具体的层级，如 0 或 1
代表层级的变量，如 u 或 v
两个层级的最大值，写作 max 应用于这些层级
层级增加，写作 + 1

编写宇宙多态定义

到目前为止，本书中定义的每种数据类型都在 Type 中，即最小的数据宇宙。在展示 Lean 标准库中的多态数据类型时，例如 List 和 Sum，本书创建了它们的非宇宙多态的版本。实际的版本使用了宇宙多态性来实现类型层级和非类型层级程序之间的代码复用。

在编写宇宙多态类型时，有一些通用的指导准则需要遵守。首先，独立的类型参数应具有不同的宇宙变量，这使得多态定义能够与更多种类的参数一起使用，从而增加代码复用的可能性。其次，整个类型本身通常要么位于所有宇宙变量的最大值，要么位于比这个最大值大一的层级。先尝试使用两者中较小的那个。最后，最好将新类型放在一个尽可能小的宇宙中，这使得它在其他内容中可以更灵活地使用。非多态类型，如 Nat 和 String，可以直接放在 Type 0 中。

`Prop` 和多态

就像 Type、Type 1 等描述了对程序和数据进行分类的类型一样，Prop 则用于对逻辑命题进行分类。 Prop 中的类型描述了什么可以作为令人信服的证据以证明一个陈述的真。命题在许多方面与普通类型相似：它们可以被归纳地声明，它们可以有构造子，并且函数也可以将命题作为参数。然而，与数据类型不同的是，通常来说，为证明陈述的真实性所提供的那个证据的具体内容并不重要，重要的是提供了那个证据。另一方面，程序不仅要返回一个 Nat，而且要返回 正确的 Nat，这一点非常重要。

Prop 位于宇宙层级体系的底部，且 Prop 的类型是 Type。这意味着 Prop 适合作为 List 的一个参数，原因和 Nat 一样。命题列表的类型是 List Prop：

def someTruePropositions : List Prop := [
  1 + 1 = 2,
  "Hello, " ++ "world!" = "Hello, world!"
]

显式地填写宇宙参数表明了 Prop 是一个 Type：

def someTruePropositions : List.{0} Prop := [
  1 + 1 = 2,
  "Hello, " ++ "world!" = "Hello, world!"
]

在幕后，Prop 和 Type 被统一到一个称为 Sort 的层级体系中。 Prop 与 Sort 0 相同，Type 0 是 Sort 1，Type 1 是 Sort 2，依此类推。实际上，Type u 就是 Sort (u+1)。在使用 Lean 编写程序时，这通常并不相关，但它可能有时会出现在错误消息中，并解释 CoeSort 类的名称。此外，将 Prop 作为 Sort 0 可以使得一个额外的宇宙运算符变得有用。宇宙级别 imax u v 在 v 为 0 时为 0，否则为 u 或 v 中较大的那个。结合 Sort，这使得在编写代码时可以使用一个特殊规则，该规则允许返回 Prop 的函数在 Prop 和 Type 宇宙之间尽可能地具有可移植性。

多态的实际应用

在本书的其余部分，多态数据类型、结构体和类的定义将使用宇宙多态性，以便与 Lean 的标准库保持一致。这将使 Functor、Applicative 和 Monad 类的完整展示与它们的实际定义完全一致。

Lean 函数式编程

宇宙

用户定义类型

宇宙多态

编写宇宙多态定义

Prop 和多态

多态的实际应用

`Prop` 和多态