# 翻译-Lean Language Reference-04-类型系统

{{< ctxset prefix="04" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="语法" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="常量" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="定理" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="公理" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="结构" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="选项" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="属性" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="例子" cnt_sect_lv_max="2">}}

项（又称表达式）是构成 Lean 核心语言含义的基本单位。
它们是由[阐释器](https://lean-lang.org/doc/reference/latest/Terms/#--tech-term-elaborator)
根据用户编写的语法生成的。
Lean 的类型系统会将项与它们的类型关联起来。
类型本身也是项，可以被视作是集合的表示，而
项则对应这些集合里的个体元素。
如果项的类型能通过基于 Lean 的类型论规则的推理获得，
那么它就是**类型良好的 Well-Typed**。只有类型良好的项才有意义。

项是一种依值类型 λ-演算：它们包括
  函数抽象、
  函数应用、
  变量和
  `let` 绑定。
除了变量绑定之外，项语言中的变量也可以指代
  [构造器](https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#--tech-term-constructors)，
  [类型构造器](https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#--tech-term-type-constructors)，
  [递归器](https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#--tech-term-recursor)，
  已声明常量或
  不透明常量。
其中
  构造器、
  类型构造器、
  递归器和
  不透明常量
不参与替换，而
  已声明常量
可以被替换为对应的定义。

一个类型良好的项的推导需要非常明确（显式）地指明所使用的推理规则。
隐晦（隐式）地说，类型良好的项可直接充当其自身类型良好的推导证明。
Lean 的类型论足够清晰明确，以至于
基于类型良好的项我们可以直接重建其完整的类型推导过程。
这就极大地减少了存储完整推导树所带来的系统开销，
同时它依然具备强大的表达能力来表示现代数学研究。
这意味着，证明项就是定理真实性的充分证据，
并且极易于进行独立验证。

除了拥有类型之外，项还通过**定义等价性 Definitional Equality** 相互关联：
这是一种可通过机器检查的关系，可以
在语法层面上将项等同起来并
模（等价 / 忽略）掉项的计算行为。
定义等价性包括以下几种形式的归约：

- **β（beta）**

  通过替换变量受缚出现来应用被构造的函数表达式。

- **δ（delta）**

  将[已声明常量](https://lean-lang.org/doc/reference/latest/The-Type-System/#--tech-term-defined-constants)的出现替换为其对应定义。

- **ι（iota）**

  对目标为构造器的递归器（即原始递归）进行归约。

- **ζ（zeta）**

  将 `let` 绑定的变量替换为其对应定义。

- **Quotient reduction**

  在[商类型的函数提升算子](https://lean-lang.org/doc/reference/latest/The-Type-System/Quotients/#quotient-model)被应用于商元素时，
  对其进行归约。

被完全归约的项称为**范式 Normal Form**。

定义等价还涵盖了
  函数以及
  只有单个构造器的归纳类型的
**η（eta）等价 η-Equivalence**：比如说
  `fun x => f x` 与 `f` 就是定义等价的，或者说
  给定一个拥有字段 `f1` 和 `f2` 的结构 `S`， 
  `S.mk x.f1 x.f2` 与 `x` 就是定义等价的。
它还具有**证明无关性 Proof Irrelevance**：
同一命题的任意两个证明都是定义等价的。
这种等价性具有自反性、对称性，但却没有传递性。

定义等价可用于类型转换：
如果有两个项定义等价，
并且给定的项以其中一个项作为其类型，
那么它也可以以另一个作为其类型。
这是因为定义等价性涵盖了归约，
类型可以通过对数据进行计算而得出。

{{< labelindex 
  type="例子" 
  summary="类型计算"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类型计算" 
  open=false
>}}
函数 `LengthList` 在被应用于一个自然数实参时
会计算出一个类型，该类型对应于一个拥有具体元素数目的向量：

```lean {wrapper=false, lineNos=false}
def LengthList (α : Type u) : Nat → Type u
  | 0 => PUnit
  | n + 1 => α × LengthList α n
```

由于 Lean 的元组是右结合的，
多个嵌套的括号可以被省略：

```lean {wrapper=false, lineNos=false}
example : LengthList Int 0 := ()

example : LengthList String 2 :=
  ("Hello", "there", ())
```

如果向量的长度与元素数量不匹配，
那么计算出的类型就无法与项匹配：

```lean {wrapper=false, lineNos=false}
example : LengthList String 5 :=
  ("Wrong", "number", ())
-- Application type mismatch: The argument
--   ()
-- has type
--   Unit
-- but is expected to have type
--   LengthList String 3
-- in the application
--   ("number", ())
```
{{< /admonition >}}

Lean 里面基本的类型有
  [宇宙](https://lean-lang.org/doc/reference/latest/The-Type-System/Universes/#--tech-term-universes)、
  [函数](https://lean-lang.org/doc/reference/latest/The-Type-System/Functions/#--tech-term-Functions)、
  [商类型构造器 `Quot`](https://lean-lang.org/doc/reference/latest/The-Type-System/Quotients/#Quot) 以及
  [归纳类型](https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#--tech-term-Inductive-types)的[类型构造器](https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#--tech-term-type-constructors)。
  [已声明常量](https://lean-lang.org/doc/reference/latest/The-Type-System/#--tech-term-defined-constants)、
  [递归器](https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#--tech-term-recursor)应用、
  函数应用、
  [公理](https://lean-lang.org/doc/reference/latest/Axioms/#--tech-term-Axioms)、
  [不透明常量](https://lean-lang.org/doc/reference/latest/Definitions/Definitions/#--tech-term-Opaque-constants)
也可以额外地产生类型，
正如它们能够产生其他类型下的项一样。

## 04.01. 函数类型 Functions {#S4-1}
{{< ctx level="2" >}}

函数类型为 Lean 的内置功能。
函数会将
  一种类型（定义域）下的值映射到
  另一种类型（陪域）下的值，并且
函数类型会指定函数的定义域和陪域。

函数类型有以下两种：

- **依值的 Dependent**

  依值函数类型显式地命名形参，并且
  函数的陪域可以显式地调用这个名称。
  由于类型可以通过值计算出来，
  因此依值函数基于不同的实参
  可能返回任意数量不同类型下的值。

  > 依值函数类型有时也被称为*依值积 Dependent Products*，
  > 因为它们对应于一族集合的索引积。

- **非依值的 Non-Dependent**

  非依值函数类型不包含形参的名称，并且
  陪域不会基于所提供的具体实参而变化。

{{< labelindex 
  type="例子" 
  summary="依值函数构造"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：依值函数类型" 
  open=false
>}}
函数 `two` 可能返回不同类型的值，
具体取决于它在应用时被传入的实参：

```lean {wrapper=false, lineNos=false}
def two : (b : Bool) → if b then Unit × Unit else String :=
  fun b =>
    match b with
    | true => ((), ())
    | false => "two"
```

函数体无法被写成 `if...then...else...` 的形式，
因为它不会像 `match` 那样对类型进行细分 Refine。
{{< /admonition >}}

在 Lean 的核心语言中，所有函数类型都是依值的：
非依值函数类型是依值函数类型的一种特例，
其中形参的名称不会出现在陪域中。此外，
两个依值函数类型如果形参名称不同也可以是定义等价的，
只要能通过重命名形参使它们相等。
然而，Lean 的阐释器并不会
为非依值函数的形参引入局部绑定。

{{< labelindex 
  type="例子" 
  summary="（非）依值函数的定义等价"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：（非）依值函数的定义等价" 
  open=false
>}}
类型 
  `(x : Nat) → String` 和 
  `Nat → String`
是定义等价的：

```lean {wrapper=false, lineNos=false}
example : ((x : Nat) → String) = (Nat → String) :=
  rfl
```

类似地，类型
  `(n : Nat) → n + 1 = 1 + n` 和 
  `(k : Nat) → k + 1 = 1 + k`
也是定义等价的：

```lean {wrapper=false, lineNos=false}
example : ((n : Nat) → n + 1 = 1 + n) = ((k : Nat) → k + 1 = 1 + k) :=
  rfl
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="非依值函数类型不绑定变量"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：非依值函数类型不绑定变量" 
  open=false
>}}
要描述“数组中的所有元素都非零”
需要用到一个依值函数：

```lean {wrapper=false, lineNos=false}
def AllNonZero (xs : Array Nat) : Prop :=
  (i : Nat) → (lt : i < xs.size) → xs[i] ≠ 0
```

这是因为负责数组访问的阐释器需要用到“索引在界内”的证明。
非依值版本的陈述不会引入这个假设：

```lean {wrapper=false, lineNos=false}
def AllNonZero (xs : Array Nat) : Prop :=
  (i : Nat) → (i < xs.size) → xs[i] ≠ 0
-- failed to prove index is valid, possible solutions:
--   - Use `have`-expressions to prove the index is valid
--   - Use `a[i]!` notation instead, runtime check is performed, and 
--     'Panic' error message is produced if index is not valid
--   - Use `a[i]?` notation instead, result is an `Option` type
--   - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
-- xs:Array Nati:Nat
-- ⊢ i < xs.size
```
{{< /admonition >}}

尽管核心类型论并不包含隐式参数，
函数类型确实包含了一个指示形参是否为隐式的标记。
尽管这个信息被 Lean 的阐释器所使用，但是其
  并不影响核心理论中的类型检查或定义等价性，并且
  在仅分析核心类型论的时候可以被忽略。

{{< labelindex 
  type="例子" 
  summary="显式 / 隐式函数类型的定义等价"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：显式 / 隐式函数类型的定义等价" 
  open=false
>}}
类型
  `{α : Type} → (x : α) → α` 和 
  `(α : Type) → (x : α) → α`
是定义等价的，
即便首个形参
  在一个当中是隐式的，而
  在另一个里却是显式的：

```lean {wrapper=false, lineNos=false}
example :
    ({α : Type} → (x : α) → α)
    =
    ((α : Type) → (x : α) → α)
  := rfl
```
{{< /admonition >}}

### 04.01.01. 函数构造 Function Abstraction {#S4-1-1}
{{< ctx level="3" >}}

在 Lean 的类型论中，函数的创建是通过
一个绑定变量的函数抽象表达式来完成的。

> 函数抽象在其他社群中也被称作 *lambda*，
>   源于 Alonzo Church 为其创建的记号；
> 又或者被称作是匿名函数，
>   因为它们不需要在全局环境中被命名。

当函数被应用时，表达式的结果是通过
[β-归约](https://lean-lang.org/doc/reference/latest/The-Type-System/#--tech-term-___) 求得的：
此过程中实参会被拿去替换变量的受缚出现。
在编译后的代码中这个过程会严格发生，
  实参必须已经变成一个值；
然而在类型检查时就没有这样的限制，
  与定义等价有关的方程理论
  允许对任意项进行 β-归约。

在 Lean 的[项语言](https://lean-lang.org/doc/reference/latest/Terms/Functions/#function-terms)中，
函数抽象表达式可以
  声明多个形参，或者是
  使用模式匹配。
这些特性会被翻译为核心语言，
当中所有函数抽象都只接收一个实参。
并非所有函数都源于函数抽象：
  [类型构造器](https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#--tech-term-type-constructors)、
  [构造器](https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#--tech-term-constructors)以及
  [递归器](https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#--tech-term-recursor)
都可能具有函数类型，
但它们不能单独依靠函数抽象来创建。

### 04.01.02. 函数柯里化 Currying {#S4-1-2}
{{< ctx level="3" >}}

在 Lean 的核心类型论中，
每个函数都会将
  [定义域](https://lean-lang.org/doc/reference/latest/The-Type-System/Functions/#--tech-term-domain)里的每个元素都映射到
  [陪域](https://lean-lang.org/doc/reference/latest/The-Type-System/Functions/#--tech-term-codomain)里的单个元素。
换句话说，每个函数都只期望接收一个实参。
多参函数是通过构造高阶函数来实现的，
  当提供第一个实参时，
  它会返回一个新的函数，该函数期望接收剩余的实参。
这种编码方式被称为**柯里化 Currying**，
由 Haskell B. Curry 推广并以其命名。
Lean 里面关于
  函数构造、
  函数类型指定以及
  函数应用
的语法造就了一种多参函数的错觉，
但其实阐释的结果只有单形参函数。

### 04.01.03. 函数外延性 Extensionality {#S4-1-3}
{{< ctx level="3" >}}

函数的定义等价性在 Lean 里面是**内涵的 Intensional**。这意味着
定义等价性是在语法层面上定义的 ——
前提是忽略受缚变量的重命名与[归约](https://lean-lang.org/doc/reference/latest/The-Type-System/#--tech-term-reduction)。
粗略地说，只要两个函数实现了相同的算法，
那么它们就是定义等价的；
这有别于数学中通常描述的相等（即
只要两个函数能够将
  [定义域](https://lean-lang.org/doc/reference/latest/The-Type-System/Functions/#--tech-term-domain)中同一个元素映射到
  [陪域](https://lean-lang.org/doc/reference/latest/The-Type-System/Functions/#--tech-term-codomain)中的同一个元素，
那么它们就是相等的）。

定义等价性会被类型检查器所使用，因此它必须是可被预测的。
内涵等价性的语法特性意味着对其进行检查的算法是可被切实可行地设计并规范化的。
外延等价性的检查本质上涉及到证明与函数相等有关的任意定理，并且
外延等价性的检查算法并不存在一个清晰的规范；
这使得其对于类型检查器是一个糟糕的选择。因此，
函数的外延等价性在这里被作为一种推理原则提供，
在涉及到证明两个函数相等的[命题](https://lean-lang.org/doc/reference/latest/The-Type-System/Propositions/#--tech-term-Propositions)的时候就可以调用它。

除了归约和受缚变量的重命名，
定义等价性还支持一种有限形式的外延性，
即 [η-等价](https://lean-lang.org/doc/reference/latest/The-Type-System/#--tech-term-___-equivalence)；
在这种等价中，函数等价于
在函数体中将自身应用到形参的抽象。举个例子：
给定 `f`，其具有类型为 `(x : α) → β x`，
那么 `f` 与 `fun x => f x` 就是定义等价的。

在对函数进行推理的时候，
  定理 [`funext`](https://lean-lang.org/doc/reference/latest/The-Type-System/Functions/#funext) 或者
  相应的策略 `funext` 或 `ext` 
可被用于证明两个函数相等——
只要这两个函数能够将相等的输入映射到相等的输出。

> 不同于其他内涵性的类型论，
> `funext` 在 Lean 里是一个定理。
> 它的证明可以通过[商类型](https://lean-lang.org/doc/reference/latest/The-Type-System/Quotients/#quotient-funext)来完成。

{{< labelindex 
  type="定理" 
  id_alias="funext"
>}}
函数外延性的证明
{{< /labelindex >}}
{{< admonition 
  type=info
  title="定理：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
funext.{u, v} {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}
  (h : ∀ (x : α), f x = g x) : f = g
```

**函数外延性 Function Extensionality**：
对于每个可以接收的实参，
如果两个函数返回的结果都相等，
那么两个函数相等。

之所以称作“外延性”是因为其提供了一种
  基于底层数学函数的性质来证明两个对象相等的方法，而不是
  基于表示它们的语法。
函数外延性是一个定理，
可以通过[商类型](https://lean-lang.org/doc/reference/latest/The-Type-System/Quotients/#quotient-funext)来证明。
{{< /admonition >}}

### 04.01.04. 函数完全性与停机性 Totality and Termination {#S4-1-4}
{{< ctx level="3" >}}

函数可以通过 `def` 来递归定义。
从 Lean 的逻辑角度来看，所有函数都是**完全的 Total**，
意味着它们会在有限时间内
  将定义域中的每个元素
  映射到陪域中的一个元素上。

> 某些编程语言社群在术语“完全 Total”的使用上可能有差异。
> 在那里函数被视作是完全的，
> 只要它们能满足不会因为未处理的情况而崩溃即可。
> 不停机的要求则被忽略。

完全函数的在所有类型正确的实参下的值都是定义好的，并且
它们不会因为模式匹配中情况缺失而无法停机或崩溃。

尽管 Lean 的逻辑模型认为所有函数都是完全的，
但是 Lean 也是一种实用的编程语言，它提供了某些“逃生舱口”。
即便函数的停机性还未被证明，
  它们仍然可以在 Lean 的逻辑中使用，
  只要能够证明它们的陪域是非空的即可。
  这些函数在 Lean 的逻辑中被视作是未解释的函数，并且
  它们的计算行为会被忽略。
  但是在编译后的代码中，这些函数就像其他函数一样被处理。
还有一些函数可能会被标记为不安全的 Unsafe；
  这些函数在 Lean 的逻辑中是不可用的。
[与部分 Partial 函数和不安全函数定义相关的章节](https://lean-lang.org/doc/reference/latest/Definitions/Recursive-Definitions/#partial-unsafe)
包含了更多关于递归函数编程的细节。

类似地，存在于编译后代码中的那些会在运行时发生失败的操作（如数组的越界访问），
只有在已知结果类型是被占据的 Inhabited（即类型非空）的情况下才能被使用。
在 Lean 的逻辑里，这些操作的结果将会是该类型下任选的一个实例（具体来说是
由该类型的 [`Inhabited`](https://lean-lang.org/doc/reference/latest/Type-Classes/Basic-Classes/#Inhabited___mk) 类型类实例所指定的那个默认值）。

{{< labelindex 
  type="例子" 
  summary="恐慌"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：恐慌" 
  open=false
>}}
函数 `thirdChar` 
  提取数组的第 3 个元素，
  如果数组的长度小于等于 2 则会发生恐慌 Panic：

```lean {wrapper=false, lineNos=false}
def thirdChar (xs : Array Char) : Char := xs[2]!
```

`#['!']` 和 `#['-', 'x']` 不存在的第三个元素是相等的，
因为它们会得到同一个任意选择的字符：

```lean {wrapper=false, lineNos=false}
example : thirdChar #['!'] = thirdChar #['-', 'x'] := rfl
```

两个结果的确都等于 `'A'`，
这恰好是 `Char` 的默认回退 Fallback 值：

```lean {wrapper=false, lineNos=false}
example : thirdChar #['!'] = 'A' := rfl
example : thirdChar #['-', 'x'] = 'A' := rfl
```
{{< /admonition >}}

### 04.01.05. 函数 API 参考 API Reference {#S4-1-5}
{{< ctx level="3" >}}

#### 04.01.05.01. 一些有用的操作

`Function` 命名空间包含了以下
用于处理函数的通用辅助工具：

{{< labelindex 
  type="常量" 
  id_alias="Function.comp"
>}}
函数复合运算
{{< /labelindex >}}
{{< admonition 
  type=info
  title="常量：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
Function.comp.{u, v, w} {α : Sort u} {β : Sort v} {δ : Sort w}
  (f : β → δ) (g : α → β) : α → δ
```

函数复合运算，通常使用中缀运算符 `∘` 来表示。
一个新函数将由两个给定的函数创建，其中
一个函数的输出将作为另一个函数的输入。

例子：

- `Function.comp List.reverse (List.drop 2) [3, 2, 4, 1] = [1, 4]`

- `(List.reverse ∘ List.drop 2) [3, 2, 4, 1] = [1, 4]`

标识符命名约定：

- `∘` 的推荐写法是 `comp`。
{{< /admonition >}}

{{< labelindex 
  type="常量" 
  id_alias="Function.const"
>}}
常值函数构造
{{< /labelindex >}}
{{< admonition 
  type=info
  title="常量：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
Function.const.{u, v} {α : Sort u} (β : Sort v) (a : α) : β → α
```

构造忽略实参的常值函数。

如果 `a : α`, 那么 `Function.const β a : β → α` 便是“输出值为 `a` 的常值函数”。 
如此对于所有实参 `b : β` 都会有 `Function.const β a b = a`。 
上述函数通常也可以直接写成 `fun _ => a`。

例子：

- `Function.const Bool 10 true = 10`

- `Function.const Bool 10 false = 10`

- `Function.const String 10 "any string" = 10`
{{< /admonition >}}

{{< labelindex 
  type="常量" 
  id_alias="Function.curry"
>}}
函数柯里化
{{< /labelindex >}}
{{< admonition 
  type=info
  title="常量：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
Function.curry.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2}
  {φ : Sort u_3} : (α × β → φ) → α → β → φ
```

将函数从接收一个二元组的形式
转换成为接收两个实参的等价形式。

例子：

- ` Function.curry (fun (x, y) => x + y) 3 5 = 8`

- ` Function.curry Prod.swap 3 "five" = ("five", 3)`
{{< /admonition >}}

{{< labelindex 
  type="常量" 
  id_alias="Function.uncurry"
>}}
函数去柯里化
{{< /labelindex >}}
{{< admonition 
  type=info
  title="常量：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
Function.uncurry.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2}
  {φ : Sort u_3} : (α → β → φ) → α × β → φ
```

将函数从接收两个实参的形式
转换成为接收一个二元组的等价形式。

例子：

- `Function.uncurry List.drop (1, ["a", "b", "c"]) = ["b", "c"]`

- `[("orange", 2), ("android", 3) ].map (Function.uncurry String.take) = ["or", "and"]`
{{< /admonition >}}

#### 04.01.05.02. 一些有用的谓词

{{< labelindex 
  type="常量" 
  id_alias="Function.Injective"
>}}
函数为单射
{{< /labelindex >}}
{{< admonition 
  type=info
  title="常量：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
Function.Injective.{u_1, u_2} {α : Sort u_1} {β : Sort u_2}
  (f : α → β) : Prop
```

函数 `f` 是**单射的 Injective**
当且仅当 `f x = f y` 蕴含 `x = y`。
{{< /admonition >}}

{{< labelindex 
  type="常量" 
  id_alias="Function.Surjective"
>}}
函数为满射
{{< /labelindex >}}
{{< admonition 
  type=info
  title="常量：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
Function.Surjective.{u_1, u_2} {α : Sort u_1} {β : Sort u_2}
  (f : α → β) : Prop
```

函数 `f : α → β` 被称为**满射的 Surjective**
当且仅当对每个 `b : β` 都存在一个 `a : α` 使得 `f a = b`。
{{< /admonition >}}

{{< labelindex 
  type="常量" 
  id_alias="Function.LeftInverse"
>}}
函数是…的左逆
{{< /labelindex >}}
{{< admonition 
  type=info
  title="常量：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
Function.LeftInverse.{u_1, u_2} {α : Sort u_1} {β : Sort u_2}
  (g : β → α) (f : α → β) : Prop
```

`LeftInverse g f` 表示函数 `g` 是函数 `f` 的左逆，即 `g ∘ f = id`。
{{< /admonition >}}

{{< labelindex 
  type="常量" 
  id_alias="Function.HasLeftInverse"
>}}
函数有左逆
{{< /labelindex >}}
{{< admonition 
  type=info
  title="常量：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
Function.HasLeftInverse.{u_1, u_2} {α : Sort u_1} {β : Sort u_2}
  (f : α → β) : Prop
```

`HasLeftInverse f` 意味着
函数 `f` 存在一个左逆。
{{< /admonition >}}

{{< labelindex 
  type="常量" 
  id_alias="Function.RightInverse"
>}}
函数是…的右逆
{{< /labelindex >}}
{{< admonition 
  type=info
  title="常量：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
Function.RightInverse.{u_1, u_2} {α : Sort u_1} {β : Sort u_2}
  (g : β → α) (f : α → β) : Prop
```

`RightInverse g f` 表示函数 `g` 是函数 `f` 的右逆，即 `f ∘ g = id`。
{{< /admonition >}}

{{< labelindex 
  type="常量" 
  id_alias="Function.HasRightInverse"
>}}
函数有右逆
{{< /labelindex >}}
{{< admonition 
  type=info
  title="常量：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
Function.HasRightInverse.{u_1, u_2} {α : Sort u_1} {β : Sort u_2}
  (f : α → β) : Prop
```

`HasRightInverse f` 意味着
函数 `f` 存在一个右逆。
{{< /admonition >}}

## 04.02. 命题 Propositions {#S4-2}
{{< ctx level="2" >}}

命题是那些可以被证明的、
有意义的陈述。毫无意义的陈述不是命题，
但是值为 `false` 的陈述是命题。
所有命题都被归类为 `Prop`。

命题有以下特性：

- **定义上的证明无关性 Definitional Proof Irrelevance**

  同一命题的任意两个证明都是可互换的。
  
- **运行时无关性 Run-time irrelevance**

  命题的证明会在代码编译后被擦除。

- **非直谓性 Impredicativity**

  命题可以量化任意宇宙层级下的类型。

- **受限消去 Restricted Elimination**

  除了 [subsingletons](https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#--tech-term-subsingleton) 的情况以外，
  命题都不能被消解到非命题类型中。

- **命题外延性 Extensionality**

  任意两个逻辑上等价的命题
  都可以通过公理 [`propext`](https://lean-lang.org/doc/reference/latest/The-Type-System/Propositions/#propext) 被证明为彼此相等的。

{{< labelindex 
  type="公理" 
  id_alias="propext"
>}}
命题外延性
{{< /labelindex >}}
{{< admonition 
  type=info
  title="公理：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
propext {a b : Prop} : (a ↔ b) → a = b
```

[公理](https://lean-lang.org/doc/reference/4.31.0/find/?domain=Verso.Genre.Manual.section&name=axioms) `propext` 断言：
  如果两个命题 `a` 和 `b` 是逻辑上等价的
  （即 `a` 可以从 `b` 证明得出，反之亦然），
  那么它们便是相等的。
如此意味着 `a` 在语境中的所有出现都可被替换为 `b`。

标准的逻辑连词可以被证明遵守命题外延性。
然而公理有时是必需的，比如
  处理像 `P a` 这样的高阶表达式——其中 `P : Prop → Prop` 未知；或者是
  处理等式。
命题外延性在直觉主义视角下是有效的。
{{< /admonition >}}

## 04.03. 宇宙 Universes {#S4-3}
{{< ctx level="2" >}}

类型是通过宇宙进行分类的。

> 宇宙也被称作是 *Sort*。
> 
> Universes are also referred to as *sorts*. 

每个宇宙都有一个对应的层级，层级是一个自然数。
`Sort` 运算符会通过提供的层级构造一个宇宙。
如果一个宇宙的层级小于另一个宇宙的层级，
那么该宇宙本身就会被认为是较小的。
除了命题（将在本章后面描述）之外，
每个宇宙中的类型都只能量化比自己小的宇宙中的类型。
`Sort 0` 是命题的类型，每个
`Sort (u + 1)` 都是描述数据的类型。

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

```lean {wrapper=false, lineNos=false}
example : Sort 5 := Sort 4
example : Sort 2 := Sort 1
```

而 `Sort 3` 却不是 `Sort 5` 的一个元素：

```lean {wrapper=false, lineNos=false}
example : Sort 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`](https://lean-lang.org/doc/reference/latest/Basic-Types/The-Unit-Type/#Unit) 的类型为 `Sort 1`，
因此出于同样的原因，
其也不是 `Sort 2` 的一个元素：

```lean {wrapper=false, lineNos=false}
example : Sort 1 := Unit
example : Sort 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` 的缩写。

### 04.03.01. 直谓性 Predicativity {#S4-3-1}
{{< ctx level="3" >}}

每个宇宙都包含了依值函数类型，
这些类型还可以拿来表示全称量化和蕴含。
一个函数类型对应的宇宙是由其定义域和陪域的宇宙所决定的，
具体情况取决于函数的陪域是否是一个命题。

谓词是那些返回命题的函数（即函数的陪域是 `Prop`）：
它们的实参类型可以来自任意宇宙，
但函数类型本身仍然属于 `Prop`。
这意味着命题具有非直谓量化的特性，
因为命题本身可以是关于所有命题（以及其他所有类型）的陈述。

{{< labelindex 
  type="例子" 
  summary="命题的非直谓性"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：命题的非直谓性" 
  open=false
>}}
证明无关性就可以被写成一个量化所有命题的命题：

```lean {wrapper=false, lineNos=false}
example : Prop := ∀ (P : Prop) (p1 p2 : P), p1 = p2
```

命题也可以量化所有类型：

```lean {wrapper=false, lineNos=false}
example : Prop := ∀ (α : Type), ∀ (x : α), x = x
example : Prop := ∀ (α : Type 5), ∀ (x : α), x = x
```
{{< /admonition >}}

对于[层级](https://lean-lang.org/doc/reference/latest/The-Type-System/Universes/#--tech-term-level)为 1 以上的宇宙（即 `Type u` 层级）
量化都是**直谓性的**。
对这些宇宙而言，函数类型的宇宙层级即
定义域宇宙层级和陪域宇宙层级的最大者。

{{< labelindex 
  type="例子" 
  summary="函数类型的宇宙层级"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：函数类型的宇宙层级" 
  open=false
>}}
下面两个函数类型的宇宙层级都是 `Type 2`：

```lean {wrapper=false, lineNos=false}
example (α : Type 1) (β : Type 2) : Type 2 := α → β
example (α : Type 2) (β : Type 1) : Type 2 := α → β
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="宇宙（非命题）的直谓性"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：宇宙（非命题）的直谓性" 
  open=false
>}}
下述例子会报错，因为注解里的宇宙层级
比实际上函数类型的宇宙层级更小。

```lean {wrapper=false, lineNos=false}
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`
```
{{< /admonition >}}

Lean 的宇宙并不是累积的；
`Type u` 中的类型并不会自动地也属于 `Type (u + 1)`。
每个类型恰好属于一个宇宙。

{{< labelindex 
  type="例子" 
  summary="宇宙的非累积性"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：宇宙的非累积性" 
  open=false
>}}
下述例子会报错，因为注解里的宇宙层级
比实际上函数类型的宇宙层级更大。

```lean {wrapper=false, lineNos=false}
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`
```
{{< /admonition >}}

### 04.03.02. 宇宙多态性 Polymorphism {#S4-3-2}
{{< ctx level="3" >}}

Lean 还支持宇宙多态性，这意味着
在 Lean 环境中定义的常量可以带有宇宙形参。
在常量被使用时，这些形参就可以用宇宙层级实例化。
宇宙形参的声明写在常量名后一个点之后的花括号里面。

{{< labelindex 
  type="例子" 
  summary="宇宙多态恒等函数"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：宇宙多态恒等函数" 
  open=false
>}}
恒等函数会接收一个宇宙形参 `u` 。其类型签名如下：

```lean {wrapper=false, lineNos=false}
id.{u} {α : Sort u} (x : α) : α
```
{{< /admonition >}}

宇宙变量还可以出现在[宇宙层级表达式](https://lean-lang.org/doc/reference/latest/The-Type-System/Universes/#level-expressions)中，
这些表达式在定义中提供了具体的宇宙层级。
在多态定义被具体的层级实例化时，
这些宇宙层级表达式也会被求值以得到具体的层级。

{{< labelindex 
  type="例子" 
  summary="宇宙层级表达式"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：宇宙层级表达式" 
  open=false
>}}
在下述例子中，`Codec` 所处的宇宙
层级比其所包含的类型的宇宙层级大 1：

```lean {wrapper=false, lineNos=false}
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`：

```lean {wrapper=false, lineNos=false}
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
```
{{< /admonition >}}

宇宙多态的定义实际上创建了一个模板化的定义，
使其可以在不同层级的宇宙上进行实例化。但是
在不同层级的宇宙上实例化会创建彼此不兼容的值。

{{< labelindex 
  type="例子" 
  summary="宇宙多态性以及定义等价性"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：宇宙多态性以及定义等价性" 
  open=false
>}}
这一点可以通过下述例子中看出。在下面的例子中，
`T` 是一个非常平凡的宇宙多态函数，它总是返回 `true`。
由于被标记为 `opaque`，
因此 Lean 无法通过展开定义来检查等价性。
尽管 `T` 的两个实例都具有相同的类型，
但是由于是在不同宇宙上实例化的，因此它们并不兼容。

```lean {wrapper=false, lineNos=false}
opaque T.{u} (_ : Nat) : Bool :=
  (fun (α : Sort u) => true) PUnit.{u}

set_option pp.universes true

def test.{u, v} : 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)
```
{{< /admonition >}}

自动绑定的隐式形参会尽可能地支持宇宙多态性。
如下定义恒等函数：

```lean {wrapper=false, lineNos=false}
def id' (x : α) := x
```

将导致类型签名如下：

```lean {wrapper=false, lineNos=false}
id'.{u} {α : Sort u} (x : α) : α
```

{{< labelindex 
  type="例子" 
  summary="自动绑定的隐式形参的宇宙单态"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：自动绑定的隐式形参的宇宙单态" 
  open=false
>}}
另一方面，由于 `Nat` 位于宇宙 `Type 0` 中，
这个函数会自动为 `α` 生成一个具体的宇宙层级；
这是因为 `m` 被同时应用于 `Nat` 和 `α` 上，
因此两者必须具有相同的类型，也就必须在同一个宇宙中：

```lean {wrapper=false, lineNos=false}
partial def count [Monad m] (p : α → Bool) (act : m α) : m Nat := do
  if p (← act) then
    return 1 + (← count p act)
  else
    return 0
```
{{< /admonition >}}

#### 04.03.02.01. 宇宙层级表达式 Level Expressions {#S4-3-2-1}
{{< ctx level="4" >}}

定义里面宇宙层级的描述不仅仅局限于
  变量以及
  常量的加法。
宇宙之间更复杂的关系
可以通过层级表达式来定义。

```lean {wrapper=false, lineNos=false}
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` 的定义如下：

$\qquad\texttt{imax}~u~v=\begin{cases}
0        & \text{when } v = 0 \\
\max~u~v  & \text{otherwise}
\end{cases}$

`imax` 被用于实现 `Prop` 的[非直谓](https://lean-lang.org/doc/reference/latest/The-Type-System/Universes/#--tech-term-impredicative)量化。特别地，
如果 `A : Sort u` 且 `B : Sort v`，
那么 `(x : A) → B : Sort (imax u v)`。
如果 `B : Prop`，
那么函数类型本身就是一个 `Prop`；
否则函数类型的层级就是 `u` 和 `v` 的最大值。

#### 04.03.02.02. 宇宙变量绑定 Universe Variable Bindings {#S4-3-2-2}
{{< ctx level="4" >}}

宇宙多态的定义会绑定宇宙变量。
这些绑定可以是显式的，也可以是隐式的。
显式的宇宙变量绑定和实例化
会作为待声明名称的后缀出现：
声明宇宙形参需要
在常量名称后面加上一个点（`.`），然后在
花括号内放置以逗号分隔的宇宙变量序列。

{{< labelindex 
  type="例子" 
  summary="宇宙多态的 `map`"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：宇宙多态的 `map`" 
  open=false
>}}
常量 `map` 的定义
  声明了两个宇宙形参（`u` 和 `v`）并
  依次用它们实例化了多态的 `List`：

```lean {wrapper=false, lineNos=false}
def map.{u, v} {α : Type u} {β : Type v}
    (f : α → β) :
    List.{u} α → List.{v} β
  | [] => []
  | x :: xs => f x :: map f xs
```
{{< /admonition >}}

正如 Lean 会自动实例化隐式参数一样，
它也会自动实例化宇宙参数。
如果 [`autoImplicit`](https://lean-lang.org/doc/reference/latest/Definitions/Headers-and-Signatures/#autoImplicit) 选项被设置为默认值 `true`，
那么[隐式形参自动插入](https://lean-lang.org/doc/reference/latest/Definitions/Headers-and-Signatures/#automatic-implicit-parameters)被启用，没必要显式地绑定宇宙变量，它们会被自动插入；
如果 `autoImplicit` 被设置为 `false`，
那么就必须显式地添加它们，或者是使用 `universe` 命令来声明它们。

{{< labelindex 
  type="例子" 
  summary="隐式形参自动插入和宇宙多态"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：隐式形参自动插入和宇宙多态" 
  open=false
>}}
当 `autoImplicit` 为 `true`（默认值）时，
下述定义也会被接受，即便其没有绑定其宇宙形参：

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

当 `autoImplicit` 为 `false` 时，
下述定义会报错，因为 `u` 和 `v` 不在作用域内：

```lean {wrapper=false, lineNos=false}
set_option autoImplicit false
def map {α : Type u} {β : Type v} (f : α → β) : List α → List β
  | [] => []
  | x :: xs => f x :: map f xs
-- unknown universe level `u`
-- unknown universe level `v`
```
{{< /admonition >}}

除了使用 `autoImplicit` 之外，
还可以使用 `universe` 命令在特定的[小节作用域](https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections/#--tech-term-section-scope)中声明宇宙变量。

{{< labelindex 
  type="语法" 
  id_alias="宇宙变量声明"
>}}
`universe …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
```lean {wrapper=false, lineNos=false}
command ::= ...
  | universe ident ident*
```

在当前作用域的范围内
声明一个或多个宇宙变量。

正如 `variable` 命令会使得
特定的标识符被视作具有特定类型的形参，
命令 `universe` 会使得
后续的标识符在声明中被隐式地量化为宇宙形参，
即便选项 `autoImplicit` 为 `false`。
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="隐式形参自动插入和宇宙变量声明"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：隐式形参自动插入和宇宙变量声明" 
  open=false
>}}
```lean {wrapper=false, lineNos=false}
set_option autoImplicit false
universe u
def id₃ (α : Type u) (a : α) := a
```
{{< /admonition >}}

由于自动隐式形参功能只会插入那些
在声明的[头部](https://lean-lang.org/doc/reference/latest/Definitions/Headers-and-Signatures/#--tech-term-header)中被使用到的参数，
所以那些仅出现在定义的右侧的宇宙变量不会被作为参数插入，
除非它们已经被声明为宇宙变量——即便 `autoImplicit` 被设置为 `true`。

{{< labelindex 
  type="例子" 
  summary="宇宙形参自动插入和宇宙命令"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：宇宙形参自动插入和宇宙命令" 
  open=false
>}}
下述带有宇宙形参显式声明的定义是可被接受的：

```lean {wrapper=false, lineNos=false}
def L.{u} := List (Type u)
```

即便是开启了隐式形参自动插入，
下述定义依然会被拒绝，
因为 `u` 没有在 `:=` 之前的头部中被提及：

```lean {wrapper=false, lineNos=false}
set_option autoImplicit true
def L := List (Type u)
-- unknown universe level `u`
```

添加宇宙变量声明后，`u` 就可以作为形参
在 `:=` 的右侧被调用了：

```lean {wrapper=false, lineNos=false}
universe u
def L := List (Type u)
```

如此 `L` 的声明就是宇宙多态的，
其中 `u` 被作为宇宙形参插入。

在 `universe` 命令作用域范围内的声明都不会是多态的——
前提是宇宙变量
  不在这些声明中出现，或者是
  不在其他自动插入的实参中出现。

```lean {wrapper=false, lineNos=false}
universe u
def L := List (Type 0)
#check L
```
{{< /admonition >}}

#### 04.03.02.03. 宇宙提升 Universe Lifting {#S4-3-2-3}
{{< ctx level="4" >}}

当一个类型的宇宙层级比在某些语境中预期的宇宙层级要小的时候，
**宇宙提升 Universe Lifting** 操作符就可以弥合这个差距。
它们包裹着给定类型的项。相比于被包裹的类型，它们位于高层的宇宙中。
有两个提升操作符：

- [`PLift`](https://lean-lang.org/doc/reference/latest/The-Type-System/Universes/#PLift___up) 可以将任何类型（包括命题）提升一个层级。
  它可被用来在数据结构（例如列表）中包裹证明。

- [`ULift`](https://lean-lang.org/doc/reference/latest/The-Type-System/Universes/#ULift___up) 可以将任何非命题类型提升任意层级。

{{< labelindex 
  type="结构" 
  id_alias="PLift"
>}}
{{< /labelindex >}}
{{< admonition 
  type=info
  title="常量：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
PLift.{u} (α : Sort u) : Type u
```

将命题或者类型抬升到更高层次的宇宙。

`PLift α` 包裹了类型 `α` 的证明或者值。
由此产生的类型将位于比 `α` 所在的宇宙高一层的宇宙中。
特别地，命题借此转为了数据。

与之相关的类型 `ULift` 可以将非命题类型提升任意层级。

例子：

```lean {wrapper=false, lineNos=false}
#check False
-- False : Prop
#check PLift False
-- PLift False : Type
#check Nat
-- Nat : Type
#check (PLift Nat : Type 1)
-- PLift Nat : Type 1
#check ([.up (by trivial), .up (by simp), .up (by decide)] : List (PLift True))
-- [{ down := True.intro }, { down := True.intro }, { down := ⋯ }] : List (PLift True)
```

- **构造器**

  `PLift.up.{u}`

  包裹一个证明或值，将其类型的宇宙层级提升一层。

- **字段**

  `down : α`

  从一个被抬升的命题或类型中提取出被包裹的证明或值。
{{< /admonition >}}

{{< labelindex 
  type="结构" 
  id_alias="ULift"
>}}
{{< /labelindex >}}
{{< admonition 
  type=info
  title="常量：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
ULift.{r, s} (α : Type s) : Type (max s r)
```

将一个类型抬升到更高的宇宙层级。

`ULift α` 包裹了一个类型为 `α` 的值。
它不再占据与 `α` 相同的宇宙（那是其最小可能的层级），
而是接收一个额外的层级参数，并占据它们的最大值（`max s r`）。
由此产生的类型可以占据任何至少与 `α` 的宇宙一样大的宇宙。

该抬升算子最终生成的宇宙层级由第一个参数（即 `r`）决定，
你可以显式地写出该参数，同时让 `α` 的层级由系统自动推导。

与之相关的类型 `PLift` 可用于将命题或类型抬升一个层级。

例子：

```lean {wrapper=false, lineNos=false}
#check Nat
-- Nat : Type
#check (ULift Nat : Type 0)
-- ULift Nat : Type
#check (ULift Nat : Type 1)
-- ULift Nat : Type 1
#check (ULift Nat : Type 5)
-- ULift Nat : Type 5
#check (ULift.{7} (PUnit : Type 3) : Type 7)
-- ULift PUnit : Type 7
```

- **构造器**

  `ULift.up.{r, s}`

  包裹一个值以提升值的类型的宇宙层次。

- **字段**

  `down : α`

  从被抬升的类型中提取出被包裹的值。
{{< /admonition >}}

## 04.04. 归纳类型 Inductive Types {#S4-4}
{{< ctx level="2" >}}

归纳类型是 Lean 中引入新类型的主要手段。
除了宇宙、函数和商类型是用户无法添加的内置语法，
Lean 中的其他所有类型要么是
  归纳类型，不然就是
  基于宇宙、函数、归纳类型所定义的。
归纳类型由其**类型构造器**和**构造器**所指定。
归纳类型的其余属性皆由此二者推导而来。
每个归纳类型都有一个单一的类型构造器，
  类型构造器可以接受宇宙参数和普通参数。
归纳类型可以拥有任意数量的构造器，
  这些构造器引入了新的值，
  这些值的类型都以对应归纳类型的类型构造器为首。

基于归纳类型的构造器和类型构造器，
Lean 会推导出一个**递归器 Recursor**。
从逻辑的角度观察，递归器代表归纳原理或消解规则；
从计算的角度观察，它们对应于原始递归计算。
递归函数的停机性是通过将它们翻译为递归器的使用来证明的，因此
要做到这一点 Lean 的内核只需对递归器的应用进行类型检查即可，无需再进行额外的停机性分析。
此外 Lean 还会基于递归器生成一些辅助构造，这些构造会在系统的其他地方使用。

> 即便对于非递归类型，
> 我们也会使用“递归器”这个术语。

结构是归纳类型的一个特殊情况，它们只有一个构造器。
在结构被声明之后，Lean 会生成一些辅助构造，
这些构造使得新结构可以使用额外的语言特性。

本小节将会介绍：
  归纳类型和结构类型声明的语法细节、
  归纳类型声明后引入到环境中的新常量和新定义，以及
  归纳类型下的值在编译后代码中的运行时表示。

### 04.04.01. 归纳类型声明 Inductive Type Declarations {#S4-4-1}
{{< ctx level="3" >}}

{{< labelindex 
  type="语法" 
  id_alias="归纳类型声明"
>}}
`inductive … where (| … )* (deriving …)?`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
```lean {wrapper=false, lineNos=false}
command ::= ...
  | declModifiers
    inductive declId optDeclSig where
      (| declModifiers ident optDeclSig)*
    (deriving ident,*)?
```

归纳类型的声明。`declModifiers` 的语法在
[“声明修饰器”](https://lean-lang.org/doc/reference/latest/Definitions/Modifiers/#declaration-modifiers)
一节中有详细介绍。
{{< /admonition >}}

在声明一个归纳类型之后，其
  类型构造器、
  构造器以及
  递归器
就会被引入到当前环境中。
新的归纳类型扩展了 Lean 的核心逻辑，
这些归纳类型的编码或表示并不是通过某些已有的数据实现的。
归纳类型的声明必须满足一系列[结构良好性的要求 Well-Formedness Requirements](https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#well-formed-inductives)，
以确保逻辑保持一致。

声明的第一行 —— 也就是从 `inductive` 开始到 `where` 结束的部分，
指定了新的[类型构造器](https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#--tech-term-type-constructors)的名称和类型。
如果有为类型构造器提供类型签名，
那么类型构造器的返回类型必须是一个宇宙，但是形参不必是类型。
如果没有提供类型签名，
那么 Lean 会尝试推导出一个足够大的宇宙来包含类型构造器的返回类型。
不过这个过程在某些情况下可能会因为
  无法找到最小的宇宙，或者是
  根本找不到宇宙
而失败。因此注解有时是必不可少的。

构造器的具体描述在 `where` 之后。
构造器并不是必须的，
归纳类型 [`False`](https://lean-lang.org/doc/reference/latest/Basic-Propositions/Truth/#False) 和 [`Empty`](https://lean-lang.org/doc/reference/latest/Basic-Types/The-Empty-Type/#Empty) 就没有构造器。
每个构造器的指定
  都以一个竖线（`|`，Unicode `VERTICAL BAR (U+007c)`）开头，
  然后跟着声明修饰符以及构造器的名称。
构造器名称是一个[原始标识符 Raw Identifier](https://lean-lang.org/doc/reference/latest/Source-Files-and-Modules/#--tech-term-raw-identifier)。
构造器名称后可以补充构造器的类型签名，
类型签名可以
  指定任何形参（前提是满足归纳类型声明的结构良好性的要求
  modulo the well-formedness requirements for inductive type declarations）==TODO==，
但是其中返回的类型
  必须是当前正在指定的归纳类型的类型构造器的饱和应用
  a saturated application of the type constructor 
  of the inductive type being specified ==TODO==。
如果没有提供类型签名，
那么 Lean 会自动推导构造器的类型：
插入足够的隐式形参来构造一个结构良好的返回类型。

新的归纳类型名称会在[当前命名空间](https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections/#--tech-term-current-namespace)中
被定义。
每个构造器的名称都位于归纳类型对应的命名空间。

#### 04.04.01.01. 归纳类型形参索引声明 Parameters and Indicies {#S4-4-1-1}
{{< ctx level="4" >}}

类型构造器可以接收以下两种类型的参数：形参和索引。
在归纳类型声明中，
  形参的调用必须保持一致，
    各个构造器里所有的类型构造器应用都必须接收完全相同的实参。
  索引作为实参
    在类型构造器的各次应用里可以各不相同。
在类型构造器签名中，所有形参都必须出现在所有索引前面。

在类型构造器的签名里，
  出现在冒号（`:`）前面的形参会被视作是整个归纳类型声明的形参。
    它们在类型声明中必须始终保持一致；而
  出现在冒号后的形参则都是索引，
    它们作为实参在归纳类型的声明中可以有所不同。但是，
如果选项 `inductive.autoPromoteIndices` 被设置为 `true`，
那么那些可能成为形参的索引就会被提升为形参。
一个索引可以构成形参，只要其
  依赖的所有类型本身也是形参，并且其
  在所有类型构造器应用里作为未实例化的变量被一致地使用。

{{< labelindex 
  type="选项" 
  id_alias="inductive.autoPromoteIndices"
  summary="默认为 `true`"
>}}
提升索引为归纳类型的形参
{{< /labelindex >}}
{{< admonition 
  type=info
  title="选项：`{{< indexprint >}}`" 
>}}
将索引提升为归纳类型的形参，不论是否可行。
{{< /admonition >}}

索引可以被视为定义了一个**类型族 Family of Types**。
每个对索引的选择都会从这一族中选中一个类型，
被选中的这个类型有自己的一组可用构造器。
带有索引的类型构造器相当于指定了一个**类型索引族 Indexed Families of Types**。

#### 04.04.01.02. 归纳类型示范 Example Inductive Types {#S4-4-1-2}
{{< ctx level="4" >}}

{{< labelindex 
  type="例子" 
  summary="无构造器的归纳类型"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：无构造器的归纳类型" 
  open=false
>}}
`Vacant` 是一个空的归纳类型，
等价于 Lean 的 `Empty` 类型：

```lean {wrapper=false, lineNos=false}
inductive Vacant : Type where
```

空的归纳类型并不是没有用的；
它们可用于表示不可达的代码。
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="无构造器的归纳命题"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：无构造器的归纳命题" 
  open=false
>}}
`No` 是一个空的归纳类型，
等价于 Lean 的 `False`。

```lean {wrapper=false, lineNos=false}
inductive No : Prop where
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="单构造器的归纳类型"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：单构造器的归纳类型" 
  open=false
>}}
`Solo` 等同于 Lean 的 `Unit` 类型：

```lean {wrapper=false, lineNos=false}
inductive Solo where
  | solo
```

刚才的归纳类型声明
省略了构造器和类型构造器的类型签名。
Lean 会将 `Solo` 赋值为 `Type`：

```lean {wrapper=false, lineNos=false}
#check Solo
-- Solo : Type
```

构造器被命名为 `Solo.solo`，
因为构造器名称位于类型构造器的命名空间中。
由于 `Solo` 不需要任何参数，
因此 `Solo.solo` 的类型签名应被推导为：

```lean {wrapper=false, lineNos=false}
#check Solo.solo
-- Solo.solo : Solo
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="单构造器的归纳命题"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：单构造器的归纳命题" 
  open=false
>}}
`Yes` 等价于 Lean 的 `True` 命题：

```lean {wrapper=false, lineNos=false}
inductive Yes : Prop where
  | intro
```

与 `One` 有所不同的是，
新的归纳类型 `Yes` 位于宇宙 `Prop` 中。

```lean {wrapper=false, lineNos=false}
#check Yes
-- Yes : Prop
```

`Yes.intro` 的类型签名将被推导为：

```lean {wrapper=false, lineNos=false}
#check Yes.intro
-- Yes.intro : Yes
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="带形参和索引的类型"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：带形参和索引的类型" 
  open=false
>}}
一个 `EvenOddList` 是一个列表，其中
  `α` 是列表中存储元素的数据类型，而
  `b` 为 `true` 当且仅当列表中有偶数个元素：

```lean {wrapper=false, lineNos=false}
set_option autoImplicit true
inductive EvenOddList (α : Type u) : Bool → Type u where
  | nil : EvenOddList α true
  | cons {isEven} : α → EvenOddList α isEven → EvenOddList α (not isEven)
```

这个例子是类型良好的，因为列表中有两个元素：

```lean {wrapper=false, lineNos=false}
example : EvenOddList String true :=
  .cons "a" (.cons "b" .nil)
```

这个例子不是类型良好的，因为列表中有三个元素：

```lean {wrapper=false, lineNos=false}
example : EvenOddList String true :=
  .cons "a" (.cons "b" (.cons "c" .nil))
-- Type mismatch
--   EvenOddList.cons "a" (EvenOddList.cons "b" (EvenOddList.cons "c" EvenOddList.nil))
-- has type
--   EvenOddList String !!!true
-- but is expected to have type
--   EvenOddList String true
```

在这个声明中，
  `α : Type u` 是一个形参，因为它在 `EvenOddList` 的所有出现中都被一致地调用；而
  `b : Bool` 是一个索引，因为不同的 `Bool` 值在不同的出现中被使用。
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="冒号前后的形参"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：冒号前后的形参" 
  open=false
>}}
在 `Either` 的类型签名中，所有形参都在冒号前面被声明。

```lean {wrapper=false, lineNos=false}
set_option autoImplicit true
inductive Either (α : Type u) (β : Type v) : Type (max u v) where
  | left : α → Either α β
  | right : β → Either α β
```

下面的版本中出现了两个名为 `α` 但可能不相同的类型：

```lean {wrapper=false, lineNos=false}
set_option autoImplicit true
inductive Either' (α : Type u) (β : Type v) : Type (max u v) where
  | left : {α : Type u} → {β : Type v} → α → Either' α β
  | right : β → Either' α β
-- Mismatched inductive type parameter in
--   Either' α β
-- The provided argument
--   α
-- is not definitionally equal to the expected parameter
--   α✝
-- 
-- Note: The value of parameter `α✝` must be fixed 
-- throughout the inductive declaration. Consider 
-- making this parameter an index if it must vary.
```
{{< /admonition >}}

#### 04.04.01.03. 匿名构造器 Anonymous Constructor Syntax {#S4-4-1-3}
{{< ctx level="4" >}}

如果一个归纳类型只有一个构造器，
那么这个构造器就可以使用**匿名构造器语法 Anonymous Constructor Syntax**。
与其写出构造器名称并将其应用于实参，
不如将显式实参用逗号分隔，并用尖括号（`⟨` 和 `⟩`，Unicode 
`MATHEMATICAL LEFT ANGLE BRACKET (U+0x27e8)` 和 
`MATHEMATICAL RIGHT ANGLEBRACKET (U+0x27e9)`）
包裹起来。
这对于模式匹配和表达式语境都是可行的。
如果是
  打算按名称提供实参，或者是
  打算用 `@` 将所有隐式形参转为显式形参，
那么就必须使用普通的构造器语法。

{{< labelindex 
  type="语法" 
  id_alias="匿名构造器"
>}}
`⟨ … ⟩`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
构造器可以被匿名调用，只需将
它们的显式参数用逗号分隔并
包裹在一对尖括号内即可，

```lean {wrapper=false, lineNos=false}
term ::= ...
  | ⟨ term ,* ⟩
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="归纳常量声明（匿名构造器）"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：归纳常量声明（匿名构造器）" 
  open=false
>}}
类型 `AtLeastOne α` 类似 `List α`，但总是非空：

```lean {wrapper=false, lineNos=false}
inductive AtLeastOne (α : Type u) : Type u where
  | mk : α → Option (AtLeastOne α) → AtLeastOne α
```

匿名构造器语法可以用来构造它们：

```lean {wrapper=false, lineNos=false}
def oneTwoThree : AtLeastOne Nat :=
  ⟨1, some ⟨2, some ⟨3, none⟩⟩⟩
```

并且可以用来对它们进行模式匹配：

```lean {wrapper=false, lineNos=false}
def AtLeastOne.head : AtLeastOne α → α
  | ⟨x, _⟩ => x
```

Lean 在背后会将匿名构造器翻译为对等的传统的构造器写法：

```lean {wrapper=false, lineNos=false}
def oneTwoThree' : AtLeastOne Nat :=
  .mk 1 (some (.mk 2 (some (.mk 3 none))))

def AtLeastOne.head' : AtLeastOne α → α
  | .mk x _ => x
```
{{< /admonition >}}

#### 04.04.01.04. 实例推导 Deriving Instances {#S4-4-1-4}
{{< ctx level="4" >}}

归纳类型声明中可选的 `deriving` 子句
可以用于推导类型类的实例。
更多信息请见[实例推导](https://lean-lang.org/doc/reference/latest/Type-Classes/Deriving-Instances/#deriving-instances)一节。

### 04.04.02. 结构声明 Structure Declarations {#S4-4-2}
{{< ctx level="3" >}}

{{< labelindex 
  type="语法" 
  id_alias="结构声明"
>}}
`structure … (: …)? (extends (… : )?…)? where (… ::)? … (deriving …)?`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
```lean {wrapper=false, lineNos=false}
command ::= ...
  | declModifiers
    structure declId bracketedBinder* (: term)?
      (extends (ident : )?term,*)?
      where
      (declModifiers ident ::)?
      structFields
    (deriving derivingClass,*)?
```

会声明一个新的结构类型。
{{< /admonition >}}

结构是那些只有单个构造器且没有索引的归纳类型。
作为对这些限制的交换，Lean 会为结构生成代码，
这些提供了不少便利：
  为各个字段生成对应的投影函数；
  提供了基于字段名称而非位置参数的额外构造器语法，并且
  类似的语法也可被用来替换某些命名字段的值；然后
  结构也可以用于扩展其他结构。
正如其他归纳类型一样，结构也可以是递归的；
它们也受到**严格正性 Strict Positivity** 有关的相同限制。
结构并没有为 Lean 增加任何表达能力；
它们的所有特性都是通过代码生成实现的。

#### 04.04.02.01. 结构形参声明 Structure Parameters {#S4-4-2-1}

与普通的归纳类型声明类似，
结构声明的头部包含
  可以指定形参的类型签名，以及
  生成的值所属的宇宙。
结构不能用于定义类型索引族。

#### 04.04.02.02. 结构字段声明 Fields {#S4-4-2-2}
{{< ctx level="4" >}}

结构声明的每个字段都
对应于一个构造器形参。

{{< labelindex 
  type="例子" 
  summary="宇宙形参自动推导"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：宇宙形参自动推导" 
  open=false
>}}
结构 `MyProd` 类似于 `Prod`：

```lean {wrapper=false, lineNos=false}
set_option autoImplicit true
structure MyProd (α β : Type _) where
  fst : α
  snd : β
```

两个形参以及两个字段都是构造器形参：

```lean {wrapper=false, lineNos=false}
MyProd.mk.{u, v}
  {α : Type u}
  {β : Type v}
  (fst : α)
  (snd : β)
  : MyProd.{u, v} α β
```

此外构造器还是[宇宙多态的](https://lean-lang.org/doc/reference/latest/The-Type-System/Universes/#--tech-term-universe-polymorphism)。
类型构造器 `MyProd` 接收两个宇宙参数：

```lean {wrapper=false, lineNos=false}
MyProd.{u, v} (α : Type u) (β : Type v) : Type (max u v)
```

每个字段类型所属宇宙的层级
必须小于等于结构所处的宇宙层级。
Lean 会推导出足以容纳 `Type u` 和 `Type v` 的最小宇宙 `Type (max u v)`。
{{< /admonition >}}

隐式形参自动插入功能会为每个字段单独插入隐式形参，即便它们的名称可能存在冲突。
这些字段会成为构造器形参，这些形参会对类型进行量化。

{{< labelindex 
  type="例子" 
  summary="隐式形参自动插入结构字段"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：隐式形参自动插入结构字段" 
  open=false
>}}
对于结构 `MyStructure` 下的所有字段，
它们的类型都被自动插入隐式形参：

```lean {wrapper=false, lineNos=false}
structure MyStructure where
  field1 : Fin n
  field2 : Fin n
```

构造器 `MyStructure.mk` 里的每个字段
都拥有自己的隐式形参 `n : Nat`：

```lean {wrapper=false, lineNos=false}
MyStructure.mk
  (field1 : {n : Nat} → Fin n)
  (field2 : {n : Nat} → Fin n)
  : MyStructure
```

类型构造器 `MyStructure` 不接收任何形参，
返回的类型为 `Type`，而这正是 `Nat` 和 `Fin n` 所在的宇宙：

```lean {wrapper=false, lineNos=false}
MyStructure : Type
```
{{< /admonition >}}

对每个字段，Lean 会生成一个投影函数，
该函数从底层类型的构造器中提取字段的值。
这个函数位于结构名称对应的命名空间中。
结构字段投影会被阐述器特殊处理（如[结构继承](https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#structure-inheritance)一节所述），
阐述器会执行额外的步骤，而不仅仅是查找命名空间。
当字段类型依赖于先前的字段时，依值投影函数的类型
  会用先前的投影来书写，而不是直接
  使用显式的模式匹配。

{{< labelindex 
  type="例子" 
  summary="依值投影类型"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：依值投影类型" 
  open=false
>}}
结构 `ArraySized` 包含一个特殊字段，
其类型同时依赖于结构形参以及先前字段：

```lean {wrapper=false, lineNos=false}
set_option autoImplicit true
structure ArraySized (α : Type u) (length : Nat)  where
  array : Array α
  size_eq_length : array.size = length
```

投影函数 `size_eq_length` 的类型签名
  接收结构类型的形参作为隐式形参，并且
  使用对应的投影函数来调用先前的字段：

```lean {wrapper=false, lineNos=false}
ArraySized.size_eq_length.{u}
  {α : Type u} {length : Nat}
  (self : ArraySized α length)
  : self.array.size = length
```
{{< /admonition >}}

结构字段可以拥有默认值，
这是通过 `:=` 指定的。
这些值会在没有提供显式值时使用。

{{< labelindex 
  type="例子" 
  summary="结构字段默认值"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：结构字段默认值" 
  open=false
>}}
一个有向图的邻接表表示可以被表示为一个 `Nat` 列表的数组。
数组的大小表示顶点的数量，并且
每个顶点的出边都存储在数组中该顶点的索引处。
由于字段 `adjacency` 提供了默认值 `#[]`，
因此可以在不提供任何字段值的情况下构造空图 `Graph.empty`。

```lean {wrapper=false, lineNos=false}
structure Graph where
  adjacency : Array (List Nat) := #[]

def Graph.empty : Graph := {}
```
{{< /admonition >}}

结构字段也可以通过索引访问，使用点记法。
字段编号从 1 开始算起。

#### 04.04.02.03. 结构构造器 Structure Constructors {#S4-4-2-3}
{{< ctx level="4" >}}

结构的构造器可以被重命名，只需
提供新名称以及 `::` 即可。
如果没有显式地提供名称，
那么在结构对应的命名空间中构造器就会被命名为 `mk`。
你还可以为构造器新名称补充额外的
[声明修饰符](https://lean-lang.org/doc/reference/latest/Definitions/Modifiers/#declaration-modifiers)。

{{< labelindex 
  type="例子" 
  summary="结构构造器重命名"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：结构构造器重命名" 
  open=false
>}}
结构 `Palindrome` 包含一个字符串以及一个证明，
后者作为字符串是回文的证据：

```lean {wrapper=false, lineNos=false}
structure Palindrome where
  ofString ::
  text : String
  is_palindrome : text.data.reverse = text.data
```

在这里结构构造器被命名为
  `Palindrome.ofString` 而不是
  `Palindrome.mk`。
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="结构构造器声明修饰符"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：结构构造器声明修饰符" 
  open=false
>}}
结构 `NatStringBimap` 维护了
自然数和字符串之间的一个有限双射：其由一对哈希映射组成，满足
每个映射的键在另一个映射中都能作为值恰好出现一次。
由于构造器是私有的，定义所处的模块外部的代码
  无法构造新的实例，
  必须使用提供的 API 来维护类型的不变量。
此外，显式地提供构造器默认名称
其实是借机给构造器附加一段文档注释。

```lean {wrapper=false, lineNos=false}
structure NatStringBimap where
  /--
  Build a finite bijection between some
  natural numbers and strings
  -/
  private mk ::
  natToString : Std.HashMap Nat String
  stringToNat : Std.HashMap String Nat

def NatStringBimap.empty : NatStringBimap := ⟨{}, {}⟩

def NatStringBimap.insert
    (nat : Nat) (string : String)
    (map : NatStringBimap) :
    Option NatStringBimap :=
  if map.natToString.contains nat ||
      map.stringToNat.contains string then
    none
  else
    some <|
      NatStringBimap.mk
        (map.natToString.insert nat string)
        (map.stringToNat.insert string nat)
```
{{< /admonition >}}

由于结构是通过单构造器归纳类型所表示的，
它们的构造器也可以通过匿名构造器语法来调用或匹配。
结构也可以通过结构实例表示法来构造或匹配，
该表示法需要写出字段的名称以及对应的值。

{{< labelindex 
  type="语法" 
  id_alias="结构构造"
>}}
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
```lean {wrapper=false, lineNos=false}
term ::= ...
  | { structInstField,*
      (: term)? }
```

基于用户提供的各个字段的值来构造结构类型的新值。
字段指定器可以有两种形式：

```lean {wrapper=false, lineNos=false}
structInstField ::= ...
  | structInstLVal := private? term

structInstField ::= ...
  | ident
```

`structInstLVal` 可以是
  一个字段名称（标识符），
  一个字段索引（自然数），或者是
  一个方括号中的项，
然后跟随着零个或多个子字段。
子字段要么是
  一个带点号（`.`）前缀的字段名称或索引，或者是
  一个方括号中的项。

这个语法会被阐述为结构构造器的应用。
为字段提供的值是按名称给出的，
这些值可以按任意顺序提供。
为子字段提供的值则被
用于初始化那些本身就嵌套在其他字段内部的结构构造器的字段。
结构的构造不允许使用方括号中的项；这些项只用于结构的更新。

不包含 `:=` 的字段指定器是字段缩写。在这种语境下，
标识符 `f` 是 `f := f` 的缩写；也就是说，
当前作用域中 `f` 的值被用来初始化字段 `f`。

每个没有默认值的字段都必须被提供值。
如果一个策略被指定为默认参数，
那么它会在阐述时被运行以构造出参数的值。

在模式匹配的语境下，
字段名称会被映射到与其对应投影匹配的模式，而
字段缩写会绑定一个模式变量，该变量即字段名称。
默认的实参仍然会出现在模式中；
如果一个模式没有为具有默认值的字段指定值，
那么这个模式只会匹配默认值。

如果字段声明包含修饰符 `private`，
那么该值会被置于当前模块的私有作用域中，即便结构的值本身位于公共作用域中。
该值会被包裹在一个公共但不被暴露的辅助定义中。
这在处理类型类的实例时尤其有用，
因为类型类公共实例里方法的实现默认是被暴露的。
这个修饰符可将它们设置为私有的。

可选的类型注解允许在 Lean
无法确定结构类型的语境中指定结构类型。
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="结构字段默认值、模式匹配"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：结构字段默认值、模式匹配" 
  open=false
>}}
结构 `AugmentedIntList` 包含
  一个列表以及
  一些额外信息。
如果后者省略则为空：

```lean {wrapper=false, lineNos=false}
structure AugmentedIntList where
  list : List Int
  augmentation : String := ""
```
在测试列表是否为空时，函数 `isEmpty`
必须显式地匹配字段 `augmentation`，
即便该字段有默认值：

```lean {wrapper=false, lineNos=false}
def AugmentedIntList.isEmpty : AugmentedIntList → Bool
  | {list := [], augmentation := ""} => true
  | _ => false
#eval {list := [], augmentation := "extra" : AugmentedIntList}.isEmpty
-- false
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="结构字段私有"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：结构字段私有" 
  open=false
>}}
即便结构声明是公有的，
单个字段也可以通过字段级别的 `private` 修饰符来隐藏。
在下述模块中，暴露的公有常量声明 `x` 允许使用私有定义 `secret`，
因为字段 `imaginary` 的值并没有被暴露：

```lean {lineNos=false, name="Main.lean"}
module

public structure Complex where
  real : Float
  imaginary : Float

private def secret := 2.3

@[expose]
public def x : Complex := {
  real := 5.0
  imaginary := private 2 * secret
}
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="私有结构函数常量声明"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：私有结构函数常量声明" 
  open=false
>}}
在下述模块中，`State` 是公有的，
但是其构造器和字段却都是私有的。
函数 `State.toString` 也是私有的，
并且打算通过 `ToString` 实例来访问；但是，
由于方法的实现会被暴露给公有实例，
因此会有报错：

```lean {lineNos=false, name="Main.lean"}
module

public structure State where
  private mk ::
  private count : Nat

private def State.toString (s : State) : String :=
  s!"⟨{s.count}⟩"

public instance : ToString State where
  toString s := s.toString
-- Invalid field `toString`: The environment 
-- does not contain `State.toString`, so 
-- it is not possible to project the field `toString` 
-- from an expression
--   s
-- of type `State`
-- 
-- Note: A private declaration `State.toString` 
-- (from the current module) exists but 
-- would need to be public to access here.
```

将 `toString` 的实现标记为私有
会将其从模块的公共作用域中移除，
从而使其可以访问私有函数：

```lean {lineNos=false, name="Main.lean"}
module

public structure State where
  private mk ::
  private count : Nat

private def State.toString (s : State) : String :=
  s!"⟨{s.count}⟩"

public instance : ToString State where
  toString s := private s.toString
```
{{< /admonition >}}

{{< labelindex 
  type="语法" 
  id_alias="结构更新"
>}}
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
```lean {wrapper=false, lineNos=false}
term ::= ...
  | {term with
      structInstField,*
      (: term)?}
```

用于更新结构类型下的值。
以 `with` 子句开头的项
  会被期待为一个结构类型的值；
  其为待更新的值。
结构的新实例会被创建，当中
  每个未被指定的字段都会从待更新的值中复制过来，而
  被指定的字段则会被替换为它们的新值。
在更新结构时，我们也可以通过
在方括号中包含要更新的索引来替换数组值。
这种更新并没有强制要求
  索引表达式在数组中是有效的，并且
  索引越界的更新会被舍弃。
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="结构常量更新"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：结构常量更新" 
  open=false
>}}
结构更新可以通过指定待更新的字段名称来更新字段。
索引越界的更新将会被忽略。

```lean {wrapper=false, lineNos=false}
structure AugmentedIntArray where
  array : Array Int
  augmentation : String := ""
deriving Repr

def one : AugmentedIntArray := {array := #[1]}
def two : AugmentedIntArray := {one with array := #[1, 2]}
def two' : AugmentedIntArray := {two with array[0] := 2}
def two'' : AugmentedIntArray := {two with array[99] := 3}
#eval (one, two, two', two'')
-- ({ array := #[1], augmentation := "" },
--  { array := #[1, 2], augmentation := "" },
--  { array := #[2, 2], augmentation := "" },
--  { array := #[1, 2], augmentation := "" })
```
{{< /admonition >}}

结构类型下的值也可以通过 `where` 来声明，
后面跟着每个字段的值。这种方式
只能用于常量声明之中，
不能用于表达式语境中。

{{< labelindex 
  type="例子" 
  summary="结构常量声明（`where`）"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：结构常量声明（`where`）" 
  open=false
>}}
Lean 中的积类型是一个名为 `Prod` 的结构。
积类型可以通过向 `Prod` 各个字段提供值来构造：

```lean {wrapper=false, lineNos=false}
def location : Float × Float where
  fst := 22.807
  snd := -13.923
```
{{< /admonition >}}

#### 04.04.02.04. 结构继承 Structure Inheritance {#S4-4-2-4}
{{< ctx level="4" >}}

结构或许会被声明为继承自其他结构。
这是通过可选的 `extends` 子句来实现的。如此声明后所产生结构类型
会拥有所有父结构类型下的所有字段。
如果父结构类型中有重叠的字段名称，
那么所有重叠的字段名称必须具有相同的类型。

产生的结构类型会拥有一个**字段解析顺序 Field Resolution Order**，
其将影响字段的值。如果可能的话，这个解析顺序将会是结构父类型的
[**C3 线性化**](https://en.wikipedia.org/wiki/C3_linearization)。
特别地，字段解析顺序应该是整个父类型集合的一个全序，
使得每个 `extends` 列表都是有序的。
当没有 C3 线性化时，Lean 会利用启发式方法来找到一个顺序。
每个结构类型在其自身的字段解析顺序中都是排名第一的。

字段解析顺序被用于计算可选字段的默认值。
当字段的值未被指定时，首个在解析顺序中定义的默认值将会被使用。
默认值中的字段引用也会使用字段解析顺序；这意味着
覆盖父构造器默认字段的子结构也可能会改变父字段的计算默认值。
由于子结构在其自身解析顺序中排名第一，
因此子结构中的默认值优先于父结构中的默认值。

当一个新结构类型继承了现有结构类型时，
新结构类型的构造器会将现有结构类型的信息作为额外的实参接收。
通常情况下。这表现为为每个父结构体类型提供一个构造器参数。
这个父值包含了所有父结构的字段。然而，
如果父结构的字段存在重叠，
那么新结构类型的构造器中将会包含来自一个或多个父结构中非重叠字段的子集，
而不是整个父结构的值，如此以避免字段信息重复。

这里不存在父结构类型与子结构类型之间的子类型关系。即便结构 B 继承了结构 A，
一个期望输入为 A 的函数也不会接受 B。但是，转换函数将会被生成，
将一个结构转换为它的每个父结构。
这些转换函数被称为**父投影 parent projections**。
父投影位于子结构的命名空间中，
它们的名称是父结构名称前加 `to`。

{{< labelindex 
  type="例子" 
  summary="结构类型继承与字段重叠"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：结构类型继承与字段重叠" 
  open=false
>}}
在这个例子中，`Textbook` 是一个 `Book`，同时也是一个 `AcademicWork`：

```lean {wrapper=false, lineNos=false}
structure Book where
  title : String
  author : String

structure AcademicWork where
  author : String
  discipline : String

structure Textbook extends Book, AcademicWork

#check Textbook.toBook
-- Textbook.toBook (self : Textbook) : Book
```

由于 `Book` 和 `AcademicWork` 中都含有字段 `author`，
构造器 `Textbook.mk` 不会将两个父结构作为参数。它的类型签名为：

```lean {wrapper=false, lineNos=false}
Textbook.mk (toBook : Book) (discipline : String) : Textbook
```

转换函数为

```lean {wrapper=false, lineNos=false}
Textbook.toBook (self : Textbook) : Book
Textbook.toAcademicWork (self : Textbook) : AcademicWork
```

第二个转换函数会将 `Book` 下面的 `author` 字段
以及未打包的 `Discipline` 字段结合起来，也就等价于：

```lean {wrapper=false, lineNos=false}
def toAcademicWork (self : Textbook) : AcademicWork :=
  let .mk book discipline := self
  let .mk _title author := book
  .mk author discipline
```
{{< /admonition >}}

生成结构的所有投影函数可以直接被拿来使用，
就好像结构的所有字段是父结构字段的并集一样。
Lean 的阐释器会在使用字段时自动生成适当的投影函数。
同样地，
  基于字段的结构初始化以及
  结构更新语法
会隐藏继承编码的细节。
然而在
  使用构造器名称、
  使用匿名构造器语法、
  通过索引而非名称引用字段
时这些编码是可见的。

{{< labelindex 
  type="例子" 
  summary="结构类型继承和字段索引"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：结构类型继承和字段索引" 
  open=false
>}}
```lean {wrapper=false, lineNos=false}
structure Pair (α : Type u) where
  fst : α
  snd : α
deriving Repr

structure Triple (α : Type u) extends Pair α where
  thd : α
deriving Repr

def coords : Triple Nat := {fst := 17, snd := 2, thd := 95}
```

对 `coords` 的第一个字段索引进行求值会得到
底层的 `Pair` 而非字段 `fst` 的内容：

```lean {wrapper=false, lineNos=false}
#eval coords.1
-- { fst := 17, snd := 2 }
```

阐释器会将 `coords.fst` 翻译为 `coords.toPair.fst`。
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="无子类型关系的结构类型"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：无子类型关系的结构类型" 
  open=false
>}}
给定下述关于偶数、偶素数以及一个具体的偶素数的定义：

```lean {wrapper=false, lineNos=false}
structure EvenNumber where
  val : Nat
  isEven : 2 ∣ val := by decide

structure EvenPrime extends EvenNumber where
  notOne : val ≠ 1 := by decide
  isPrime : ∀ n, n ≤ val → n ∣ val  → n = 1 ∨ n = val

def two : EvenPrime where
  val := 2
  isPrime := by
    intros
    repeat' (cases ‹Nat.le _ _›)
    all_goals omega

def printEven (num : EvenNumber) : IO Unit :=
  IO.print num.val
```

将 `two` 直接传递给 `printEven` 会产生类型错误：

```lean {wrapper=false, lineNos=false}
#check printEven two
-- Application type mismatch: The argument
--   two
-- has type
--   EvenPrime
-- but is expected to have type
--   EvenNumber
-- in the application
--   printEven two
```

这是因为 `EvenPrime` 类型下的值
并不是 `EvenNumber` 类型下的值。
{{< /admonition >}}

`#print` 命令可以显示结构类型的最重要信息，包括
  父投影，
  所有字段及其默认值，
  构造器，以及
  字段解析顺序。
在处理包含菱形继承的深层次继承结构时，
这些信息会非常有用。

{{< labelindex 
  type="例子" 
  summary="继承图中的菱形结构"
/>}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：继承图中的菱形结构" 
  open=false
>}}
下述代码展示了各种自行车的模型，包括
  电动自行车、
  非电动自行车以及
  普通尺寸和大型家庭自行车。
最后一个结构类型 `ElectricFamilyBike`
在其继承关系图中包含一个菱形结构，
因为 `FamilyBike` 和 `ElectricBike` 都继承自 `Bicycle`。

```lean {wrapper=false, lineNos=false}
structure Vehicle where
  wheels : Nat

structure Bicycle extends Vehicle where
  wheels := 2

structure ElectricVehicle extends Vehicle where
  batteries : Nat := 1

structure FamilyBike extends Bicycle where
  wheels := 3

structure ElectricBike extends Bicycle, ElectricVehicle

structure ElectricFamilyBike
    extends FamilyBike, ElectricBike where
  batteries := 2
```

`#print` 命令可以显示每个结构类型的重要信息：

```lean {wrapper=false, lineNos=false}
#print ElectricBike
-- structure ElectricBike : Type
-- number of parameters: 0
-- parents:
--   ElectricBike.toBicycle : Bicycle
--   ElectricBike.toElectricVehicle : ElectricVehicle
-- fields:
--   Vehicle.wheels : Nat :=
--     2
--   ElectricVehicle.batteries : Nat :=
--     1
-- constructor:
--   ElectricBike.mk (toBicycle : Bicycle) (batteries : Nat) : ElectricBike
-- field notation resolution order:
--   ElectricBike, Bicycle, ElectricVehicle, Vehicle
```

一个 `ElectricFamilyBike` 有三个轮子，
因为 `FamilyBike` 在其解析顺序中
排在 `Bicycle` 之前。

```lean {wrapper=false, lineNos=false}
#print ElectricFamilyBike
-- structure ElectricFamilyBike : Type
-- number of parameters: 0
-- parents:
--   ElectricFamilyBike.toFamilyBike : FamilyBike
--   ElectricFamilyBike.toElectricBike : ElectricBike
-- fields:
--   Vehicle.wheels : Nat :=
--     3
--   ElectricVehicle.batteries : Nat :=
--     2
-- constructor:
--   ElectricFamilyBike.mk (toFamilyBike : FamilyBike) (batteries : Nat) : ElectricFamilyBike
-- field notation resolution order:
--   ElectricFamilyBike, FamilyBike, ElectricBike, Bicycle, ElectricVehicle, Vehicle
```
{{< /admonition >}}

### 04.04.03. 逻辑模型 Logical Model {#S4-4-3}
{{< ctx level="3" >}}

### 04.04.04. 运行时表示 Run-time Representation {#S4-4-4}
{{< ctx level="3" >}}

### 04.04.05. 互为递归的类型 Mutual Inductive Types {#S4-4-5}
{{< ctx level="3" >}}

## 索引 Index {#index}

### 语法

{{< indexlist type="语法" >}}

### 常量

{{< indexlist type="常量" code_wrap=true >}}

### 定理

{{< indexlist type="定理" code_wrap=true >}}

### 公理

{{< indexlist type="公理" code_wrap=true >}}

### 结构

{{< indexlist type="结构" code_wrap=true >}}

### 选项

{{< indexlist type="选项" code_wrap=true >}}

### 属性

{{< indexlist type="属性" code_wrap=true >}}

### 例子

{{< indexlist type="例子" print_section=false >}}


---

> 作者: [沉积岩](ych817.github.io)  
> URL: https://ych817.github.io/posts/9cc1dea/