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

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

项是一种依值类型 λ-演算：它们包括 函数抽象、 函数应用、 变量和 let 绑定。 除了变量绑定之外，项语言中的变量也可以指代 构造器， 类型构造器， 递归器， 已声明常量或 不透明常量。 其中 构造器、 类型构造器、 递归器和 不透明常量 不参与替换，而 已声明常量 可以被替换为对应的定义。

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

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

• β（beta）

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

• δ（delta）

  将已声明常量的出现替换为其对应定义。

• ι（iota）

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

• ζ（zeta）

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

• Quotient reduction

  在商类型的函数提升算子被应用于商元素时， 对其进行归约。

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

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

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

def LengthList (α : Type u) : Nat → Type u
  | 0 => PUnit
  | n + 1 => α × LengthList α n

example : LengthList Int 0 := ()

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

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", ())

Lean 里面基本的类型有 宇宙、 函数、 商类型构造器 Quot 以及 归纳类型的类型构造器。 已声明常量、 递归器应用、 函数应用、 公理、 不透明常量 也可以额外地产生类型， 正如它们能够产生其他类型下的项一样。

04.01. 函数类型 Functions

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

函数类型有以下两种：

• 依值的 Dependent

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

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

• 非依值的 Non-Dependent

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

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

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

example : ((x : Nat) → String) = (Nat → String) :=
  rfl

example : ((n : Nat) → n + 1 = 1 + n) = ((k : Nat) → k + 1 = 1 + k) :=
  rfl

def AllNonZero (xs : Array Nat) : Prop :=
  (i : Nat) → (lt : i < xs.size) → xs[i] ≠ 0

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

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

example :
    ({α : Type} → (x : α) → α)
    =
    ((α : Type) → (x : α) → α)
  := rfl

04.01.01. 函数构造 Function Abstraction

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

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

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

在 Lean 的项语言中， 函数抽象表达式可以 声明多个形参，或者是 使用模式匹配。 这些特性会被翻译为核心语言， 当中所有函数抽象都只接收一个实参。 并非所有函数都源于函数抽象： 类型构造器、 构造器以及 递归器 都可能具有函数类型， 但它们不能单独依靠函数抽象来创建。

04.01.02. 函数柯里化 Currying

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

04.01.03. 函数外延性 Extensionality

函数的定义等价性在 Lean 里面是内涵的 Intensional。这意味着 定义等价性是在语法层面上定义的 —— 前提是忽略受缚变量的重命名与归约。 粗略地说，只要两个函数实现了相同的算法， 那么它们就是定义等价的； 这有别于数学中通常描述的相等（即 只要两个函数能够将 定义域中同一个元素映射到 陪域中的同一个元素， 那么它们就是相等的）。

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

除了归约和受缚变量的重命名， 定义等价性还支持一种有限形式的外延性， 即 η-等价； 在这种等价中，函数等价于 在函数体中将自身应用到形参的抽象。举个例子： 给定 f，其具有类型为 (x : α) → β x， 那么 f 与 fun x => f x 就是定义等价的。

在对函数进行推理的时候， 定理 funext 或者 相应的策略 funext 或 ext 可被用于证明两个函数相等—— 只要这两个函数能够将相等的输入映射到相等的输出。

不同于其他内涵性的类型论， funext 在 Lean 里是一个定理。 它的证明可以通过商类型来完成。

funext.{u, v} {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}
  (h : ∀ (x : α), f x = g x) : f = g

04.01.04. 函数完全性与停机性 Totality and Termination

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

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

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

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

类似地，存在于编译后代码中的那些会在运行时发生失败的操作（如数组的越界访问）， 只有在已知结果类型是被占据的 Inhabited（即类型非空）的情况下才能被使用。 在 Lean 的逻辑里，这些操作的结果将会是该类型下任选的一个实例（具体来说是 由该类型的 Inhabited 类型类实例所指定的那个默认值）。

def thirdChar (xs : Array Char) : Char := xs[2]!

example : thirdChar #['!'] = thirdChar #['-', 'x'] := rfl

example : thirdChar #['!'] = 'A' := rfl
example : thirdChar #['-', 'x'] = 'A' := rfl

04.01.05. 函数 API 参考 API Reference

04.01.05.01. 一些有用的操作

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

Function.comp.{u, v, w} {α : Sort u} {β : Sort v} {δ : Sort w}
  (f : β → δ) (g : α → β) : α → δ

Function.const.{u, v} {α : Sort u} (β : Sort v) (a : α) : β → α

Function.curry.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2}
  {φ : Sort u_3} : (α × β → φ) → α → β → φ

Function.uncurry.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2}
  {φ : Sort u_3} : (α → β → φ) → α × β → φ

04.01.05.02. 一些有用的谓词

Function.Injective.{u_1, u_2} {α : Sort u_1} {β : Sort u_2}
  (f : α → β) : Prop

Function.Surjective.{u_1, u_2} {α : Sort u_1} {β : Sort u_2}
  (f : α → β) : Prop

Function.LeftInverse.{u_1, u_2} {α : Sort u_1} {β : Sort u_2}
  (g : β → α) (f : α → β) : Prop

Function.HasLeftInverse.{u_1, u_2} {α : Sort u_1} {β : Sort u_2}
  (f : α → β) : Prop

Function.RightInverse.{u_1, u_2} {α : Sort u_1} {β : Sort u_2}
  (g : β → α) (f : α → β) : Prop

Function.HasRightInverse.{u_1, u_2} {α : Sort u_1} {β : Sort u_2}
  (f : α → β) : Prop

04.02. 命题 Propositions

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

命题有以下特性：

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

  同一命题的任意两个证明都是可互换的。

• 运行时无关性 Run-time irrelevance

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

• 非直谓性 Impredicativity

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

• 受限消去 Restricted Elimination

  除了 subsingletons 的情况以外， 命题都不能被消解到非命题类型中。

• 命题外延性 Extensionality

  任意两个逻辑上等价的命题 都可以通过公理 propext 被证明为彼此相等的。

propext {a b : Prop} : (a ↔ b) → a = b

04.03. 宇宙 Universes

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

宇宙也被称作是 Sort。

Universes are also referred to as sorts.

每个宇宙都有一个对应的层级，层级是一个自然数。 Sort 运算符会通过提供的层级构造一个宇宙。 如果一个宇宙的层级小于另一个宇宙的层级， 那么该宇宙本身就会被认为是较小的。 除了命题（将在本章后面描述）之外， 每个宇宙中的类型都只能量化比自己小的宇宙中的类型。 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 := 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 := 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

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

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

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

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

对于层级为 1 以上的宇宙（即 Type u 层级） 量化都是直谓性的。 对这些宇宙而言，函数类型的宇宙层级即 定义域宇宙层级和陪域宇宙层级的最大者。

example (α : Type 1) (β : Type 2) : Type 2 := α → β
example (α : Type 2) (β : Type 1) : Type 2 := α → β

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`

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

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`

04.03.02. 宇宙多态性 Polymorphism

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

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

宇宙变量还可以出现在宇宙层级表达式中， 这些表达式在定义中提供了具体的宇宙层级。 在多态定义被具体的层级实例化时， 这些宇宙层级表达式也会被求值以得到具体的层级。

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

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

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

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)

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

def id' (x : α) := x

将导致类型签名如下：

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

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

04.03.02.01. 宇宙层级表达式 Level Expressions

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

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 的非直谓量化。特别地， 如果 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

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

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

正如 Lean 会自动实例化隐式参数一样， 它也会自动实例化宇宙参数。 如果 autoImplicit 选项被设置为默认值 true， 那么隐式形参自动插入被启用，没必要显式地绑定宇宙变量，它们会被自动插入； 如果 autoImplicit 被设置为 false， 那么就必须显式地添加它们，或者是使用 universe 命令来声明它们。

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

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`

除了使用 autoImplicit 之外， 还可以使用 universe 命令在特定的小节作用域中声明宇宙变量。

command ::= ...
  | universe ident ident*

set_option autoImplicit false
universe u
def id₃ (α : Type u) (a : α) := a

由于自动隐式形参功能只会插入那些 在声明的头部中被使用到的参数， 所以那些仅出现在定义的右侧的宇宙变量不会被作为参数插入， 除非它们已经被声明为宇宙变量——即便 autoImplicit 被设置为 true。

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

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

universe u
def L := List (Type u)

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

04.03.02.03. 宇宙提升 Universe Lifting

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

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

• ULift 可以将任何非命题类型提升任意层级。

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

#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)

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

#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

04.04. 归纳类型 Inductive Types

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

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

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

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

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

04.04.01. 归纳类型声明 Inductive Type Declarations

command ::= ...
  | declModifiers
    inductive declId optDeclSig where
      (| declModifiers ident optDeclSig)*
    (deriving ident,*)?

在声明一个归纳类型之后，其 类型构造器、 构造器以及 递归器 就会被引入到当前环境中。 新的归纳类型扩展了 Lean 的核心逻辑， 这些归纳类型的编码或表示并不是通过某些已有的数据实现的。 归纳类型的声明必须满足一系列结构良好性的要求 Well-Formedness Requirements， 以确保逻辑保持一致。

声明的第一行 —— 也就是从 inductive 开始到 where 结束的部分， 指定了新的类型构造器的名称和类型。 如果有为类型构造器提供类型签名， 那么类型构造器的返回类型必须是一个宇宙，但是形参不必是类型。 如果没有提供类型签名， 那么 Lean 会尝试推导出一个足够大的宇宙来包含类型构造器的返回类型。 不过这个过程在某些情况下可能会因为 无法找到最小的宇宙，或者是 根本找不到宇宙 而失败。因此注解有时是必不可少的。

构造器的具体描述在 where 之后。 构造器并不是必须的， 归纳类型 False 和 Empty 就没有构造器。 每个构造器的指定 都以一个竖线（|，Unicode VERTICAL BAR (U+007c)）开头， 然后跟着声明修饰符以及构造器的名称。 构造器名称是一个原始标识符 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 会自动推导构造器的类型： 插入足够的隐式形参来构造一个结构良好的返回类型。

新的归纳类型名称会在当前命名空间中 被定义。 每个构造器的名称都位于归纳类型对应的命名空间。

04.04.01.01. 归纳类型形参索引声明 Parameters and Indicies

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

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

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

04.04.01.02. 归纳类型示范 Example Inductive Types

inductive Vacant : Type where

inductive No : Prop where

inductive Solo where
  | solo

#check Solo
-- Solo : Type

#check Solo.solo
-- Solo.solo : Solo

inductive Yes : Prop where
  | intro

#check Yes
-- Yes : Prop

#check Yes.intro
-- Yes.intro : Yes

set_option autoImplicit true
inductive EvenOddList (α : Type u) : Bool → Type u where
  | nil : EvenOddList α true
  | cons {isEven} : α → EvenOddList α isEven → EvenOddList α (not isEven)

example : EvenOddList String true :=
  .cons "a" (.cons "b" .nil)

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

set_option autoImplicit true
inductive Either (α : Type u) (β : Type v) : Type (max u v) where
  | left : α → Either α β
  | right : β → Either α β

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.

04.04.01.03. 匿名构造器 Anonymous Constructor Syntax

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

term ::= ...
  | ⟨ term ,* ⟩

inductive AtLeastOne (α : Type u) : Type u where
  | mk : α → Option (AtLeastOne α) → AtLeastOne α

def oneTwoThree : AtLeastOne Nat :=
  ⟨1, some ⟨2, some ⟨3, none⟩⟩⟩

def AtLeastOne.head : AtLeastOne α → α
  | ⟨x, _⟩ => x

def oneTwoThree' : AtLeastOne Nat :=
  .mk 1 (some (.mk 2 (some (.mk 3 none))))

def AtLeastOne.head' : AtLeastOne α → α
  | .mk x _ => x

04.04.01.04. 实例推导 Deriving Instances

归纳类型声明中可选的 deriving 子句 可以用于推导类型类的实例。 更多信息请见实例推导一节。

04.04.02. 结构声明 Structure Declarations

command ::= ...
  | declModifiers
    structure declId bracketedBinder* (: term)?
      (extends (ident : )?term,*)?
      where
      (declModifiers ident ::)?
      structFields
    (deriving derivingClass,*)?

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

04.04.02.01. 结构形参声明 Structure Parameters

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

04.04.02.02. 结构字段声明 Fields

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

set_option autoImplicit true
structure MyProd (α β : Type _) where
  fst : α
  snd : β

MyProd.mk.{u, v}
  {α : Type u}
  {β : Type v}
  (fst : α)
  (snd : β)
  : MyProd.{u, v} α β

MyProd.{u, v} (α : Type u) (β : Type v) : Type (max u v)

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

structure MyStructure where
  field1 : Fin n
  field2 : Fin n

MyStructure.mk
  (field1 : {n : Nat} → Fin n)
  (field2 : {n : Nat} → Fin n)
  : MyStructure

MyStructure : Type

对每个字段，Lean 会生成一个投影函数， 该函数从底层类型的构造器中提取字段的值。 这个函数位于结构名称对应的命名空间中。 结构字段投影会被阐述器特殊处理（如结构继承一节所述）， 阐述器会执行额外的步骤，而不仅仅是查找命名空间。 当字段类型依赖于先前的字段时，依值投影函数的类型 会用先前的投影来书写，而不是直接 使用显式的模式匹配。

set_option autoImplicit true
structure ArraySized (α : Type u) (length : Nat)  where
  array : Array α
  size_eq_length : array.size = length

ArraySized.size_eq_length.{u}
  {α : Type u} {length : Nat}
  (self : ArraySized α length)
  : self.array.size = length

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

structure Graph where
  adjacency : Array (List Nat) := #[]

def Graph.empty : Graph := {}

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

04.04.02.03. 结构构造器 Structure Constructors

结构的构造器可以被重命名，只需 提供新名称以及 :: 即可。 如果没有显式地提供名称， 那么在结构对应的命名空间中构造器就会被命名为 mk。 你还可以为构造器新名称补充额外的 声明修饰符。

structure Palindrome where
  ofString ::
  text : String
  is_palindrome : text.data.reverse = text.data

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)

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

term ::= ...
  | { structInstField,*
      (: term)? }

structInstField ::= ...
  | structInstLVal := private? term

structInstField ::= ...
  | ident

structure AugmentedIntList where
  list : List Int
  augmentation : String := ""

def AugmentedIntList.isEmpty : AugmentedIntList → Bool
  | {list := [], augmentation := ""} => true
  | _ => false
#eval {list := [], augmentation := "extra" : AugmentedIntList}.isEmpty
-- false

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
}

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.

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

term ::= ...
  | {term with
      structInstField,*
      (: term)?}

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 := "" })

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

def location : Float × Float where
  fst := 22.807
  snd := -13.923

04.04.02.04. 结构继承 Structure Inheritance

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

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

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

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

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

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

Textbook.mk (toBook : Book) (discipline : String) : Textbook

Textbook.toBook (self : Textbook) : Book
Textbook.toAcademicWork (self : Textbook) : AcademicWork

def toAcademicWork (self : Textbook) : AcademicWork :=
  let .mk book discipline := self
  let .mk _title author := book
  .mk author discipline

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

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}

#eval coords.1
-- { fst := 17, snd := 2 }

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

#check printEven two
-- Application type mismatch: The argument
--   two
-- has type
--   EvenPrime
-- but is expected to have type
--   EvenNumber
-- in the application
--   printEven two

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

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