Lean 语言参考

4.3. 宇宙🔗

类型按 universes 进行分类。 宇宙也称为 sorts。 每个宇宙都有一个 level， 是自然数。 Sort 运算符从给定级别构造一个 Universe。 如果一个宇宙的层次小于另一个宇宙的层次，则称宇宙本身较小。 除了命题（本章稍后描述）之外，给定宇宙中的类型只能对较小宇宙中的类型进行量化。 Sort 0 是命题的类型，而每个 Sort (u + 1) 是描述数据的类型。

每个宇宙都是下一个更大宇宙的元素，因此 Sort 5 包括 Sort 4。 这意味着以下示例被接受：

example : Sort 5 := Sort 4 example : Sort 2 := Sort 1

另一方面，Sort 3 不是 Sort 5 的元素：

example : Sort 5 := Type mismatch Type 2 has type Type 3 of sort `Type 4` but is expected to have type Type 4 of sort `Type 5`Sort 3 
Type mismatch
  Type 2
has type
  Type 3
of sort `Type 4` but is expected to have type
  Type 4
of sort `Type 5`

同样，由于 Unit 在 Sort 1 中，因此它不在 Sort 2 中：

example : Sort 1 := Unit example : Sort 2 := Type mismatch Unit has type Type of sort `Type 1` but is expected to have type Type 1 of sort `Type 2`Unit 
Type mismatch
  Unit
has type
  Type
of sort `Type 1` but is expected to have type
  Type 1
of sort `Type 2`

由于命题和数据的用途不同，受不同的规则管辖，为了方便区分，提供缩写Type和Prop。 Type u 是 Sort (u + 1) 的缩写，因此 Type 0 为 Sort 1，Type 3 为 Sort 4。 Type 0 也可以缩写为 Type，即 Unit : Type 和 Type : Type 1。 Prop 是 Sort 0 的缩写。

4.3.1. 预测性🔗

每个宇宙都包含依赖函数类型，这些函数类型还代表全称量化和含义。 函数类型的范围由其参数和返回类型的范围决定。 具体规则取决于函数的返回类型是否是命题。

谓词是返回命题的函数（即，函数的结果是 Prop 中的某种类型）可以在任何宇宙中具有参数类型，但函数类型本身仍保留在 Prop 中。 换句话说，命题具有 impredicative 量化的特征，因为命题本身可以是关于所有命题（以及所有其他类型）的陈述。

Impredicativity

证明无关性可以写成一个对所有命题进行量化的命题：

example : Prop := ∀ (P : Prop) (p1 p2 : P), p1 = p2

命题还可以在任何给定级别量化所有类型：

example : Prop := ∀ (α : Type), ∀ (x : α), x = x example : Prop := ∀ (α : Type 5), ∀ (x : α), x = x
Live ↪

对于 级别 1 及更高级别（即 Type u 层次结构）的 Universe，量化为 predicative。 对于这些全域，函数类型的全域是参数和返回类型的全域的最小上限。

Universe levels of function types

这两种类型都在 Type 2 中：

example (α : Type 1) (β : Type 2) : Type 2 := α → β example (α : Type 2) (β : Type 1) : Type 2 := α → β
Live ↪
Predicativity of Type

该示例不被接受，因为 α 的级别大于 1。换句话说，带注释的 Universe 小于函数类型的 Universe：

example (α : Type 2) (β : Type 1) : Type 1 := Type mismatch α → β has type Type 2 of sort `Type 3` but is expected to have type Type 1 of sort `Type 2`α → β 
Type mismatch
  α → β
has type
  Type 2
of sort `Type 3` but is expected to have type
  Type 1
of sort `Type 2`

Lean 的 Universe 不是 累积； Type u 中的类型不会自动出现在 Type (u + 1) 中。 每种类型都恰好栖息在同一个宇宙中。

No cumulativity

此示例不被接受，因为带注释的 Universe 大于函数类型的 Universe：

example (α : Type 2) (β : Type 1) : Type 3 := Type mismatch α → β has type Type 2 of sort `Type 3` but is expected to have type Type 3 of sort `Type 4`α → β 
Type mismatch
  α → β
has type
  Type 2
of sort `Type 3` but is expected to have type
  Type 3
of sort `Type 4`

4.3.2. 多态性🔗

Lean 支持 universe 多态性、 ，这意味着 Lean 环境中定义的常量可以采用 universe 参数。 当使用常量时，可以使用 宇宙层级 实例化这些参数。 Universe 参数写在花括号中，常量名称后面紧跟一个点。

Universe-polymorphic identity function

当完全显式时，恒等函数采用全域参数 u。它的签名是：

id.{u} {α : Sort u} (x : α) : α

Universe 变量还可能出现在 宇宙层级 表达式 中，其在定义中提供特定的 宇宙层级。 当用具体级别实例化多态定义时，这些 宇宙层级 表达式也会被评估以产生具体级别。

Universe level expressions

在此示例中，Codec 所在的 Universe 比它包含的类型的 Universe 大 1：

structure Codec.{u} : Type (u + 1) where type : Type u encode : Array UInt32 → type → Array UInt32 decode : Array UInt32 → Nat → Option (type × Nat)

Lean 自动推断大多数电平参数。 在以下示例中，无需将类型注释为 Codec.{0}，因为 Char 的类型为 Type 0，因此 u 必须为 0：

def Codec.char : Codec where type := Char encode buf ch := buf.push ch.val decode buf i := do let v ← buf[i]? if h : v.isValidChar then let ch : Char := ⟨v, h⟩ return (ch, i + 1) else failure
Live ↪

宇宙多态定义实际上创建了一个可以在各种级别实例化的示意性定义，并且宇宙的不同实例化创建了不兼容的值。

Universe polymorphism and definitional equality

这可以在以下示例中看到，其中 T 是一个无偿宇宙多态函数，它始终返回 true。 由于它被标记为 Lean.Parser.Command.declaration : commandopaque，因此 Lean 无法通过展开定义来检查相等性。 T 的两个实例都具有相同的参数和类型，但它们不同的 Universe 实例使它们不兼容。

opaque T.{u} (_ : Nat) : Bool := (fun (Variable name `α` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`α : Sort u) => true) PUnit.{u} set_option pp.universes true def Not a definitional equality: the left-hand side T.{u} 0 is not definitionally equal to the right-hand side T.{v} 0test.{u, v} : T.{u} 0 = T.{v} 0 := Type mismatch rfl.{?u.5} has type Eq.{?u.5} ?m.7 ?m.7 but is expected to have type Eq.{1} (T.{u} 0) (T.{v} 0)rfl 
Type mismatch
  rfl.{?u.5}
has type
  Eq.{?u.5} ?m.7 ?m.7
but is expected to have type
  Eq.{1} (T.{u} 0) (T.{v} 0)

自动绑定的隐式参数尽可能具有全域多态性。 定义恒等函数如下：

def id' (x : α) := x

签名结果：

id'.{u} {α : Sort u} (x : α) : α
Universe monomorphism in auto-bound implicit parameters

另一方面，由于 Nat 在全域 Type 0 中，因此该函数自动以 α 的具体 宇宙层级 结束，因为 m 应用于 Nat 和 α，因此两者必须具有相同的类型，因此处于相同的类型宇宙：

partial def count [Monad m] (p : α → Bool) (act : m α) : m Nat := do if p (← act) then return 1 + (← count p act) else return 0
Live ↪

4.3.2.1. 级别表达式🔗

定义中出现的级别不仅限于变量和常量的添加。 可以使用级别表达式来定义宇宙之间更复杂的关系。

Level ::= 0 | 1 | 2 | ...  -- Concrete levels
        | u, v             -- Variables
        | Level + n        -- Addition of constants
        | max Level Level  -- Least upper bound
        | imax Level Level -- Impredicative LUB

给定级别变量分配给具体数字，评估这些表达式遵循通常​​的算术规则。 imax 操作定义如下：

\mathtt{imax}\ u\ v = \begin{cases}0 & \mathrm{when\ }v = 0\\\mathtt{max}\ u\ v&\mathrm{otherwise}\end{cases}

imax 用于实现 Prop 的 指示 量化。 特别是，如果 A : Sort u 和 B : Sort v，则 (x : A) → B : Sort (imax u v)。 如果是 B : Prop，则函数类型本身就是 Prop；否则，功能类型的级别为u 和v 中的最大值。

4.3.2.2. Universe 变量绑定🔗

宇宙多态定义绑定宇宙变量。 这些绑定可以是显式的，也可以是隐式的。 显式 Universe 变量绑定和实例化作为定义名称的后缀出现。 Universe 参数是通过在常量名称后加上句点 (.) 后跟大括号之间以逗号分隔的 Universe 变量序列来定义或提供的。

Universe-polymorphic map

以下 map 声明声明了两个 Universe 参数（u 和 v），并依次实例化每个多态 List：

def map.{u, v} {α : Type u} {β : Type v} (f : α → β) : List.{u} α → List.{v} β | [] => [] | x :: xs => f x :: map f xs
Live ↪

正如 Lean 自动实例化隐式参数一样，它也会自动实例化 Universe 参数。 当启用 自动隐式参数插入（即 autoImplicit 选项设置为 true，这是默认值）时，无需显式绑定 Universe 变量；它们会自动插入。 当它设置为 false 时，必须显式添加它们或使用 universe 命令声明它们。

Automatic Implicit Parameters and Universe Polymorphism

当 autoImplicit 为 true（这是默认设置）时，即使不绑定其 Universe 参数，也会接受此定义：

set_option autoImplicit true def map {α : Type u} {β : Type v} (f : α → β) : List α → List β | [] => [] | x :: xs => f x :: map f xs

当 autoImplicit 为 false 时，定义将被拒绝，因为 u 和 v 不在范围内：

set_option autoImplicit false def map {α : Type unknown universe level `u`u} {β : Type unknown universe level `v`v} (f : α → β) : List α → List β | [] => [] | x :: xs => f x :: map f xs 
unknown universe level `u`
unknown universe level `v`

除了使用 autoImplicit 之外，还可以使用 universe 命令将特定标识符声明为特定 节范围 中的 Universe 变量。

syntaxUniverse Parameter Declarations
command ::= ...
    | Declares one or more universe variables.

`universe u v`

`Prop`, `Type`, `Type u` and `Sort u` are types that classify other types, also known as
*universes*. In `Type u` and `Sort u`, the variable `u` stands for the universe's *level*, and a
universe at level `u` can only classify universes that are at levels lower than `u`. For more
details on type universes, please refer to [the relevant chapter of Theorem Proving in Lean][tpil
universes].

Just as type arguments allow polymorphic definitions to be used at many different types, universe
parameters, represented by universe variables, allow a definition to be used at any required level.
While Lean mostly handles universe levels automatically, declaring them explicitly can provide more
control when writing signatures. The `universe` keyword allows the declared universe variables to be
used in a collection of definitions, and Lean will ensure that these definitions use them
consistently.

[tpil universes]: https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html#types-as-objects
(Type universes on Theorem Proving in Lean)

```lean
/- Explicit type-universe parameter. -/
def id₁.{u} (α : Type u) (a : α) := a

/- Implicit type-universe parameter, equivalent to `id₁`.
  Requires option `autoImplicit true`, which is the default. -/
def id₂ (α : Type u) (a : α) := a

/- Explicit standalone universe variable declaration, equivalent to `id₁` and `id₂`. -/
universe u
def id₃ (α : Type u) (a : α) := a
```

On a more technical note, using a universe variable only in the right-hand side of a definition
causes an error if the universe has not been declared previously.

```lean
def L₁.{u} := List (Type u)

-- def L₂ := List (Type u) -- error: `unknown universe level 'u'`

universe u
def L₃ := List (Type u)
```

## Examples

```lean
universe u v w

structure Pair (α : Type u) (β : Type v) : Type (max u v) where
  a : α
  b : β

#check Pair.{v, w}
-- Pair : Type v → Type w → Type (max v w)
```
universe ident ident*

为当前范围的范围声明一个或多个 Universe 变量。

正如 variable 命令导致特定标识符被视为具有特定类型的参数一样，universe 命令导致后续标识符在提及它们的声明中隐式量化为 Universe 参数，即使选项 autoImplicit 是 false。

The universe command when autoImplicit is false
set_option autoImplicit false universe u def id₃ (α : Type u) (a : α) := a

由于自动隐式参数功能仅插入声明的 header 中使用的参数，因此仅出现在定义右侧的 Universe 变量不会作为参数插入，除非已使用 universe 声明它们，即使 autoImplicit 为 true 也是如此。

Automatic universe parameters and the universe command

接受带有显式 Universe 参数的定义：

def L.{u} := List (Type u)

即使使用自动隐式参数，此定义也会被拒绝，因为标头中未提及 u，该标头位于 := 之前：

set_option autoImplicit true def L := List (Type unknown universe level `u`u) 
unknown universe level `u`

通过 Universe 声明，即使在右侧，​​u 也被接受为参数：

universe u def L := List (Type u)

L 的最终定义是全域多态的，其中 u 作为全域参数插入。

如果 universe 命令范围内的声明或其他自动插入的参数中未出现 Universe 变量，则该声明不会成为多态。

universe u def L := List (Type 0) L : Type 1#check L
Live ↪

4.3.2.3. 宇宙提升🔗

当一种类型的 Universe 小于某些上下文中预期的 Universe 时，universe lift 运算符可以弥补这一差距。 这些是给定类型术语的包装器，它们位于比包装类型更大的宇宙中。 起重操作员有两名：

  • PLift 可以将任何类型（包括 命题）提升一级。它可用于在数据结构（例如列表）中包含证明。

  • ULift 可以将任何非命题类型提升任意数量的级别。

🔗structure
PLift.{u} (α : Sort u) : Type u
PLift.{u} (α : Sort u) : Type u

Lifts a proposition or type to a higher universe level.

PLift α wraps a proof or value of type α. The resulting type is in the next largest universe after that of α. In particular, propositions become data.

The related type ULift can be used to lift a non-proposition type by any number of levels.

Examples:

Constructor

PLift.up.{u}

Wraps a proof or value to increase its type's universe level by 1.

Fields

down : α

Extracts a wrapped proof or value from a universe-lifted proposition or type.

🔗structure
ULift.{r, s} (α : Type s) : Type (max s r)
ULift.{r, s} (α : Type s) : Type (max s r)

Lifts a type to a higher universe level.

ULift α wraps a value of type α. Instead of occupying the same universe as α, which would be the minimal level, it takes a further level parameter and occupies their maximum. The resulting type may occupy any universe that's at least as large as that of α.

The resulting universe of the lifting operator is the first parameter, and may be written explicitly while allowing α's level to be inferred.

The related type PLift can be used to lift a proposition or type by one level.

Examples:

Constructor

ULift.up.{r, s}

Wraps a value to increase its type's universe level.

Fields

down : α

Extracts a wrapped value from a universe-lifted type.