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

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

项是一种带依值类型的 λ-演算：它们包括 函数项的构造、 函数项的应用、 let 绑定、 标识符。 项语言中的标识符除了可以指代 受缚变量之外，还可以指代 归纳项的构造子、 归纳类型构造子、 归纳项的递归子、 不透明常量以及 已声明常量 Declared Constant、 其中前四者不可以被展开，而 已声明常量可以被展开为对应的定义内容。

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

除了拥有类型之外，项还可以通过 定义等价性 Definitional Equality 彼此关联： 这是一种可以通过机器检验的关系， 可以在语法层面上将项等同起来——前提是它们拥有类似的计算行为。 定义等价性包括以下几种形式的归约 Reduction：

• β（beta）

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

• δ（delta）

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

• ι（iota）

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

• ζ（zeta）

  将被 let 绑定的名称替换为其对应的定义。

• Quotient

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

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

定义等价还涵盖了 函数以及 只有单个项构造子的归纳类型的 η 等价 η-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 以及 归纳类型构造子。 已声明常量、 归纳项的递归子的应用、 函数项应用、 公理、 不透明常量 也可以额外地产生类型， 正如它们能够产生其他类型下的项一样。

4.1. 函数 Functions

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

函数类型有以下两种：

• 依值的 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
  -- 这里 (lt : i < xs.size) 意味着依值函数类型表达式绑定了名称 lt

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

4.1.1. 抽象 Function Abstraction

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

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

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

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

4.1.2. 柯里化 Currying

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

4.1.3. 外延性 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

4.1.4. 完全性、可以终止性 Totality and Termination

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

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

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

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

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

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

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

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

4.1.5. API 参考 API Reference

4.1.5.1. 相关操作 Operations

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} : (α → β → φ) → α × β → φ

4.1.5.2. 相关谓词 Properties

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

4.2. 命题 Propositions

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

命题有以下特性：

• 定义上的命题类型的证明无关性 Definitional Proof Irrelevance

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

• 运行时无关性 Run-Time Irrelevance

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

• 非直谓性 Impredicativity

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

• 受限消去 Restricted Elimination

  除了子单例的情况以外， 任何命题都不能被消解到非命题类型中。

• 外延性 Extensionality

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

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

4.3. 宇宙 Universes

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

宇宙也被称作是 Sort。

每个宇宙都有一个对应的层级 Level，层级是一个自然数。 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 的缩写。

4.3.1. 直谓性 Predicativity

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

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

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 层级） 量化都是直谓的 Predicative。 对这些宇宙而言，函数类型的宇宙层级即 定义域宇宙层级和陪域宇宙层级的最大者。

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`

4.3.2. 多态性 Polymorphism

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

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

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

structure Codec.{u} : Type (u + 1) where -- u + 1 即宇宙层级表达式
  type : Type u
  encode : Array UInt32 → type → Array UInt32
  decode : Array UInt32 → Nat → Option (type × Nat)

def Codec.char : Codec where -- 没必要写成 Codec.{0} 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

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

set_option autoImplicit false
def T.{u} (_ : Nat) : Bool :=
  (fun (α : Sort u) => true) PUnit.{u}

set_option pp.universes true

theorem test.{u, v} : T.{u} 0 = T.{v} 0 := rfl

set_option autoImplicit 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)

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

set_option autoImplicit true
def id' (x : α) := x

将导致如下类型签名：

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

set_option autoImplicit true
partial def count [Monad m] (p : α → Bool) (act : m α) : m Nat := do
-- 这里会自动在 count 与 [Monad m] 之间插入 {m α}
  if p (← act) then
    return 1 + (← count p act)
  else
    return 0

#check count
-- count.{u_1} {m : Type → Type u_1} {α : Type} [Monad m] (p : α → Bool) (act : m α) : m Nat

4.3.2.1. 层级表达式 Level Expressions

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

Level ::= 
  | 0 | 1 | 2 | ...  -- 宇宙层级常量
  | u, v             -- 宇宙层级变量
  | Level + n        -- 宇宙层级表达式的运算
  | max Level Level  -- 宇宙层级的最小上界
  | imax Level Level -- 宇宙层级的非直谓最小上界

4.3.2.2. 层级形参声明 Universe Variable Bindings

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

-- 这里的 List.{u} 和 List.{v} 是宇宙层级形参的显式调用
def map.{u, v} {α : Type u} {β : Type v} (f : α → β) : List.{u} α → List.{v} β
  | [] => []
  | x :: xs => f x :: map f xs

正如 Lean 会自动实例化隐式形参， 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`

set_option autoImplicit true
def L : Type (u + 1) := List (Type u)

universe u
def L := List (Type u)

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

4.3.2.3. 提升 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) -- 这个很重要，不然 (by …) 会报错
)
-- [
--   { 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

4.4. 归纳类型 Inductive Types

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

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

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

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

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

4.4.1. 归纳类型声明 Inductive Type Declarations

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

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

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

归纳项构造子的具体描述在 where 之后。 归纳项构造子并不是必须的，比如归纳类型 False 和 Empty 就没有归纳项构造子。 每个归纳项构造子的指定 都以一个竖线（|，Unicode VERTICAL BAR (U+007c)）开启， 然后跟着声明修饰器以及归纳项构造子的名称。 归纳项构造子名称是一个原始标识符。 归纳项构造子名称后可以补充归纳项构造子的类型签名， 类型签名可以 指定任何形参（前提是满足归纳类型声明形式良好性的要求）， 但是其中返回的类型 必须是当前正在声明的归纳类型的类型构造子的饱和应用。 如果没有提供类型签名， 那么 Lean 便会自动推导归纳项构造子的类型 —— 通过 自动声明足够的隐式形参来构造一个形式良好的返回类型。

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

4.4.1.1. 形参和索引声明 Parameters and Indicies

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

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

索引相当于是声明了一个类型族 Family of Types。 每个对索引的选择都会从这一族类型中选中一个类型， 被选中的这个类型有自己的一组可用的归纳项构造子。 带有索引的归纳类型构造子相当于指定了一个类型索引族 Indexed Families of Types。

4.4.1.2. 示范 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        -- 没有这个会报错：unknown universe u
set_option relaxedAutoImplicit true -- 没有这个会报错：unknown identifier `isEven`
inductive EvenOddList (α : Type u) : Bool → Type u where
  | nil : EvenOddList α true
  | cons : α → EvenOddList α isEven → EvenOddList α (not isEven)
-- cons 这里会自动添加 {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.

4.4.1.3. 项的匿名构造 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

4.4.1.4. 实例推导 Deriving Instances

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

4.4.2. 结构类型声明 Structure Declarations

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

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

4.4.2.1. 形参声明 Structure Parameters

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

4.4.2.2. 字段声明 Fields

结构声明中的每个字段 Field 都对应于一个结构项构造子的形参。

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 开始算起。

4.4.2.3. 项构造子 Structure Constructors

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

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

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)

由于结构其实就是只有单个项构造子的归纳， 结构项构造子也可以通过归纳项构造子调用的匿名表示语法来调用或模式匹配。 结构项的构造或匹配也可以使用实例表示 Instance Notation 方式， 该表示法需要写出结构字段的名称以及对应的值。

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

4.4.2.4. 结构继承 Structure Inheritance

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

新结构将会拥有一个字段解析顺序 Field Resolution Order， 其会影响字段的值。如果可能的话，这个解析顺序将会是父结构的 C3 线性化 C3 Linearization。 特别地，字段解析顺序应该是所有父结构构成的集合上的一个全序关系， 满足每个 extends 的链都是有序的。 如果 C3 线性化无解，那么 Lean 就会利用启发式方法来找到一个顺序。 每个结构在其自身的字段解析顺序中都是排名第一的。

字段解析顺序会被用于计算可选字段的默认值。 当字段的值未被指定时，默认值将会按照解析顺序中的首个类进行设置。 字段默认值表达式中的字段引用同样也遵循字段解析顺序；这意味着： 如果子结构声明覆盖了父结构字段的默认值， 那么其也可能会改变父结构字段的默认值。 由于子结构在其自身解析顺序中排名第一， 因此子结构中字段的默认值优先于父结构的默认值。

当一个新结构继承了现有的结构时， 新结构对应的项构造子会将现有结构的信息作为额外的实参接收。通常情况下这体现为 所有父结构都会有一个对应的项作为实参被传入新结构对应的项构造子， 每个父结构对应的项都携带了父结构所有字段的值。然而， 如果多个父结构的字段存在重叠，那么新结构对应的项构造子就 只会包含来自一个或多个父结构不重叠字段的子集， 而非父结构下完整的项，以此来避免信息重复。

这里不存在父结构与子结构之间的子类型关系。 即便结构类型 B 继承了结构类型 A， 一个期望实参类型为 A 的函数也不会接受 B 类型下的项。但是， 转换函数将会被生成，用于将结构项转换为它的每个父结构对应的项。 这些转换函数称作是项的父投影函数 Parent Projection。 项的父投影函数位于与子结构类型同名的命名空间中， 它们的名称为父结构类型名称前加上前缀 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

#check Textbook.mk
-- Textbook.mk (toBook : Book) (discipline : String) : Textbook
-- 在字段解析顺序中，Textbook > Book > AcademicWork

#check Textbook.toBook
-- Textbook.toBook (self : Textbook) : Book
#print Textbook.toBook
-- @[reducible] def Textbook.toBook
-- : Textbook → Book
-- :=fun self ↦ self.1

#check Textbook.toAcademicWork
-- Textbook.toAcademicWork (self : Textbook) : AcademicWork
#print Textbook.toAcademicWork
-- @[reducible] def Textbook.toAcademicWork
-- : Textbook → AcademicWork
-- :=fun self ↦ {
--   author := self.author,
--   discipline := self.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