Lean 函数式编程(二) | 重载与类型类

发表于 2025-10-10 更新于 2025-10-11 阅读次数：字数： 27k 时间 ≈ 1:39

重载与类型类

在许多语言中，内置数据类型有特殊的优待。例如，在 C 和 Java 中，+ 可以被用于 float 和 int，但不能用于其他第三方库的数字。类似地，数字字符可以被直接用于内置类型，但是不能用于用户定义的数字类型。其他语言为运算符提供 重载（overloading） 机制，使得同一个运算符可以在新的类型有意义。在这些语言中，比如 C++ 和 C#，多种内置运算符都可以被重载，编译器使用类型检查来选择一个特定的实现。

除了数字和运算符，许多语言还可以重载函数或方法。在 C++，Java，C# 和 Kotlin 中，对于不同的数字和类型参数，一个方法可以有多种实现。编译器使用参数的数字和它们的类型来决定使用哪个重载。

函数和运算符的重载有一个关键的受限之处：多态函数无法限定它们的类型参数为重载存在的那些类型。例如，一个重载方法可能在字符串，字节数组和文件指针上有定义，但是没有任何方法能写第二个方法能在任意这些类型上适用。如果想这样做的话，这第二个方法必须本身也为每一个类型都有一个原始方法的重载，最终产生许多繁琐的定义而不是一个简单的多态定义。这种限制的另一个后果是一些运算符（例如 Java 中的等号）对 每一个 参数组合都要有定义，即使这样做是完全没必要的。如果程序员没有很谨慎的话，这可能会导致程序在运行时崩溃，或者静静地计算出错误的结果。

Lean 用 类型类（type classes） 机制（源于 Haskell）来实现重载。这使得运算符，函数和字面量重载与多态有一个很好的配合。一个类型类描述了一族可重载的运算符。要将这些运算符重载到新的类型上，你需要创建一个包含对新类型的每一个运算的实现方式的 实例（instance） 。例如，Add 类型类描述了可加的类型，一个对 Nat 类型的 Add 实例提供了 Nat 上加法的实现。

类和实例这两个词可能会使面向对象程序员感到混淆，因为 Lean 中的它们与面向对象语言中的类和实例关系不大。然而，它们有相同的基本性质：在日常语言中，“类”这个词指的是具有某些共同属性的组。虽然面向对象编程中的类确实描述了具有共同属性的对象组，但该术语还指代描述此类对象组的特定编程语言机制。类型类也是描述共享共同属性的类型（即某些操作的实现）的一种方式，但它们与面向对象编程中的类并没有其他共同点。

Lean 的类型类更像是 Java 或 C# 中的 接口（interface） 。类型类和接口都描述了在概念上有联系的运算的集合，这些运算为一个类型或一个类型集合实现。类似地，类型类的实例也很像 Java 或 C# 中描述实现了的接口的类，而不是 Java 或 C# 中类的实例。不像 Java 或 C# 的接口，对于一个类型，该类型的作者并不能访问的类型类也可以给这个类型实例。从这种意义上讲，这和 Rust 的 traits 很像。

正整数

自定义类型

在某些应用场景中，只有正数才有意义。例如，编译器和解释器通常使用从1开始的行号和列号来表示源代码位置，而表示非空列表的数据类型永远不会报告长度为零的情况。与其依赖自然数并在代码中散布断言来确保数字不为零，不如设计一个只表示正数的数据类型。

表示正数的一种方法与 Nat 非常相似，只是用 one 作为基础情况而不是 zero：

1
2
3

inductive Pos : Type where
  | one : Pos
  | succ : Pos → Pos

这个数据类型准确地表示了我们想要的值集合，但使用起来并不方便。例如，数字字面量会被拒绝：

1	def seven : Pos := 7

1 2	failed to synthesize instance OfNat Pos 7

相反，必须直接使用构造子：

1 2	def seven : Pos := Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ Pos.one)))))

同样，加法和乘法也不容易使用：

def fourteen : Pos := seven + seven

failed to synthesize instance
  HAdd Pos Pos ?m.291

def fortyNine : Pos := seven * seven

failed to synthesize instance
  HMul Pos Pos ?m.291

这些错误消息都以 failed to synthesize instance 开头。这表明错误是由于尚未实现的重载操作引起的，并描述了必须实现的类型类。

类与实例

类型类由名称、一些参数和一组 方法（method） 组成。参数描述了要为其定义可重载操作的类型，方法是可重载操作的名称和类型签名。这里再次出现了与面向对象语言的术语冲突。在面向对象编程中，方法本质上是连接到内存中特定对象的函数，具有访问对象私有状态的特殊权限。对象通过其方法进行交互。在 Lean 中，"方法"一词指的是已声明为可重载的操作，与对象、值或私有字段没有特殊关联。

重载加法的一种方法是定义一个名为 Plus 的类型类，其中包含一个名为 plus 的加法方法。一旦为 Nat 定义了 Plus 的实例，就可以使用 Plus.plus 来相加两个 Nat：

1
2
3

#eval Plus.plus 5 3

8

添加更多实例可以让 Plus.plus 接受更多类型的参数。

在下面的类型类声明中，Plus 是类的名称，α : Type 是唯一的参数，plus : α → α → α 是唯一的方法：

1 2	class Plus (α : Type) where plus : α → α → α

这个声明表示存在一个类型类 Plus，它针对类型 α 重载操作。具体来说，有一个名为 plus 的重载操作，它接受两个 α 并返回一个 α。

类型类是一等公民，就像类型是一等公民一样。特别地，类型类是另一种类型。Plus 的类型是 Type → Type，因为它接受一个类型作为参数（α），并产生一个新类型，该类型描述了 Plus 操作对 α 的重载。

要为特定类型重载 plus，需要编写一个实例：

1 2	instance : Plus Nat where plus := Nat.add

instance 后的冒号表明 Plus Nat 确实是一个类型。类 Plus 的每个方法都应该使用 := 赋值。在这种情况下，只有一个方法：plus。

默认情况下，类型类方法在与类型类同名的命名空间中定义。打开命名空间会很方便，这样用户就不需要先输入类的名称。open 命令中的括号表示只有指定的名称才能从命名空间中访问：

open Plus (plus)

#eval plus 5 3

8

为 Pos 定义加法函数和 Plus Pos 的实例，可以使用 plus 来相加 Pos 或 Nat 值：

def Pos.plus : Pos → Pos → Pos
  | Pos.one, k => Pos.succ k
  | Pos.succ n, k => Pos.succ (n.plus k)

instance : Plus Pos where
  plus := Pos.plus

def fourteen : Pos := plus seven seven

因为还没有 Plus Float 的实例，尝试使用 plus 相加两个浮点数会失败，并显示熟悉的错误消息：

#eval plus 5.2 917.25861

failed to synthesize instance
  Plus Float

这些错误意味着 Lean 无法为给定的类型类找到实例。

重载加法

Lean 的内置加法运算符是名为 HAdd 的类型类的语法糖，它灵活地允许加法的参数具有不同的类型。HAdd 是 异构加法（heterogeneous addition） 的缩写。例如，可以编写一个 HAdd 实例来允许将 Nat 与 Float 相加，结果是一个新的 Float。当程序员写 x + y 时，它被解释为 HAdd.hAdd x y。

虽然对 HAdd 完全通用性的理解依赖于本章另一节中讨论的特性，但有一个更简单的类型类叫做 Add，它不允许混合参数类型。当两个参数具有相同类型时，Lean 库的设置会使得在找到 HAdd 实例时，会找到 Add 的实例。

定义 Add Pos 的实例将允许 Pos 值使用普通的加法语法：

instance : Add Pos where
  add := Pos.plus

-- instance : HAdd Pos Pos Pos where
--   hAdd : Pos → Pos → Pos := Pos.plus

def fourteen : Pos := seven + seven

转换为字符串

另一个有用的内置类叫做 ToString。ToString 的实例提供了将给定类型的值转换为字符串的标准方法。例如，当值出现在插值字符串中时会使用 ToString 实例，它决定了在 IO 描述开始处 使用的 IO.println 函数如何显示值。

例如，将 Pos 转换为 String 的一种方法是显示其内部结构。函数 posToString 接受一个 Bool 参数，该参数决定是否为 Pos.succ 的使用加括号，在函数的初始调用中应该为 true，在所有递归调用中应该为 false。

def posToString (atTop : Bool) (p : Pos) : String :=
  let paren s := if atTop then s else "(" ++ s ++ ")"
  match p with
  | Pos.one => "Pos.one"
  | Pos.succ n => paren s!"Pos.succ {posToString false n}"

将此函数用于 ToString 实例：

1 2	instance : ToString Pos where toString := posToString true

会产生信息丰富但令人眼花缭乱的输出：

1
2
3

#eval s!"There are {seven}"

"There are Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ Pos.one)))))"

另一方面，每个正数都有对应的 Nat。将其转换为 Nat，然后使用 ToString Nat 实例（即 Nat 的 toString 重载）是生成更简短输出的快速方法：

def Pos.toNat : Pos → Nat
  | Pos.one => 1
  | Pos.succ n => n.toNat + 1

instance : ToString Pos where
  toString x := toString (x.toNat)

#eval s!"There are {seven}"

"There are 7"

当定义了多个实例时，最新的实例优先。此外，如果类型有 ToString 实例，那么即使该类型没有使用 deriving Repr 定义，也可以用它来显示 #eval 的结果，所以 #eval seven 输出 7。

重载乘法

对于乘法，有一个名为 HMul 的类型类允许混合参数类型，就像 HAdd 一样。正如 x + y 被解释为 HAdd.hAdd x y，x * y 被解释为 HMul.hMul x y。对于两个相同类型参数相乘的常见情况，Mul 实例就足够了。

An instance of Mul allows ordinary multiplication syntax to be used with Pos:

Mul 的实例允许在 Pos 中使用普通的乘法语法：

def Pos.mul : Pos → Pos → Pos
  | Pos.one, k => k
  | Pos.succ n, k => n.mul k + k

instance : Mul Pos where
  mul := Pos.mul

有了这个实例，乘法按预期工作：

#eval [seven * Pos.one,
       seven * seven,
       Pos.succ Pos.one * seven]

[7, 49, 14]

数字字面量

为正数写出一系列构造子是相当不方便的。解决这个问题的一种方法是提供一个将 Nat 转换为 Pos 的函数。然而，这种方法有缺点。首先，因为 Pos 不能表示 0，结果函数要么将 Nat 转换为更大的数字，要么返回 Option Pos。这两种方式对用户都不是特别方便。其次，需要显式调用函数会使使用正数的程序比使用 Nat 的程序编写起来不那么方便。在精确类型和方便的 API 之间进行权衡意味着精确类型变得不那么有用。

在 Lean 中，自然数字面量使用名为 OfNat 的类型类来解释：

1 2	class OfNat (α : Type) (_ : Nat) where ofNat : α

这个类型类接受两个参数：α 是要为其重载自然数的类型，未命名的 Nat 参数是程序中遇到的实际字面量数字。然后使用方法 ofNat 作为数字字面量的值。因为类包含 Nat 参数，所以可以只为那些数字有意义的值定义实例。

OfNat 展示了类型类的参数不需要是类型。因为在 Lean 中，类型是语言中的一等公民，可以作为参数传递给函数，并且可以使用 def 和 abbrev 给出定义。Lean 并不阻止非类型参数出现在类型类的参数位置上，但一些不够灵活的语言则不允许这种操作。这种灵活性能为特定的值以及特定的类型提供运算符重载。

例如，表示小于四的自然数的和类型可以定义如下：

inductive LT4 where
  | zero
  | one
  | two
  | three
deriving Repr

虽然允许任何字面量数字用于此类型没有意义，但小于四的数字显然是有意义的：

instance : OfNat LT4 0 where
  ofNat := LT4.zero

instance : OfNat LT4 1 where
  ofNat := LT4.one

instance : OfNat LT4 2 where
  ofNat := LT4.two

instance : OfNat LT4 3 where
  ofNat := LT4.three

有了这些实例，以下示例可以工作：

#eval (3 : LT4)
LT4.three

#eval (0 : LT4)
LT4.zero

另一方面，越界的字面量仍然不被允许：

#eval (4 : LT4)

failed to synthesize instance
OfNat LT4 4

对于 Pos，OfNat 实例应该适用于除 Nat.zero 之外的任何 Nat。另一种表达方式是说，对于所有自然数 n，实例应该适用于 n + 1。正如像 α 这样的名称自动成为 Lean 自己填充的函数的隐式参数一样，实例可以接受自动隐式参数。在这个实例中，参数 n 代表任何 Nat，实例为大一的 Nat 定义：

instance : OfNat Pos (n + 1) where
  ofNat :=
    -- 定义局部辅助函数 natPlusOne
    let rec natPlusOne : Nat → Pos
      | 0 => Pos.one
      | k + 1 => Pos.succ (natPlusOne k)
    natPlusOne n

因为 n 代表比用户写的数字小一的 Nat，辅助函数 natPlusOne 返回比其参数大一的 Pos。这使得可以为正数使用自然数字面量，但不能为零：

1
2
3

def eight : Pos := 8

def zero : Pos := 0

1 2	failed to synthesize instance OfNat Pos 0

练习

表示正数的另一种方法是作为某个 Nat 的后继。用一个构造子名为 succ 且包含 Nat 的结构体替换 Pos 的定义：

1
2
3

structure Pos where
  succ ::
  pred : Nat

定义 Add、Mul、ToString 和 OfNat 的实例，使这个版本的 Pos 能够方便地使用。

解答：

instance : Add Pos where
  add x y := Pos.succ (x.pred + y.pred + 1)

instance : Mul Pos where
  mul x y := Pos.succ (x.pred * y.pred + x.pred + y.pred)

instance : ToString Pos where
  toString x := toString (x.pred + 1)

instance : OfNat Pos (n + 1) where
  ofNat := Pos.succ n

定义一个只表示偶数的数据类型。定义 Add、Mul 和 ToString 的实例，使其能够方便地使用。OfNat 需要下一节中介绍的特性。

-- 定义偶数数据类型
inductive Even : Type where
  | zero : Even                    -- 0 是偶数
  | addTwo : Even → Even          -- 如果 n 是偶数，那么 n+2 也是偶数

-- 将偶数转换为自然数的辅助函数
def Even.toNat : Even → Nat
  | Even.zero => 0
  | Even.addTwo e => e.toNat + 2

def Even.add : Even → Even → Even
  | x, Even.zero => x
  | x, Even.addTwo y => Even.addTwo (Even.add x y)

-- Add 实例：两个偶数相加仍是偶数
instance : Add Even where
  add := Even.add

def Even.mul : Even → Even → Even
  | Even.zero, _ => Even.zero
  -- (2 + x) * y
  | Even.addTwo x, y => (y + y + Even.mul x y)

-- Mul 实例：两个偶数相乘仍是偶数
instance : Mul Even where
  mul := Even.mul

-- ToString 实例：显示为自然数形式
instance : ToString Even where
  toString e := toString e.toNat

HTTP 请求以 HTTP 方法的标识开始，如 GET 或 POST，以及 URI 和 HTTP 版本。定义一个归纳类型来表示 HTTP 方法的有趣子集，以及一个表示 HTTP 响应的结构体。响应应该有一个 ToString 实例，使其可以进行调试。使用类型类将不同的 IO 操作与每个 HTTP 方法关联，并编写一个测试工具作为 IO 操作，调用每个方法并打印结果。

类型类与多态

编写适用于给定函数的任意重载可能会很有用。例如，IO.println 适用于任何具有 ToString 实例的类型。通过在所需实例周围使用方括号来表示：IO.println 的类型是 {α : Type} → [ToString α] → α → IO Unit。这个类型表示 IO.println 接受一个类型为 α 的参数，并且 Lean 应该自动确定这个类型，而且必须有一个可用于 α 的 ToString 实例，最后返回一个 IO 操作。

注：这一节我们讨论如何编写作用于所有注册类型的函数。

对多态函数的类型检查

对接受隐式参数，或使用了类型类的函数进行类型检查时，我们需要用到一些额外的语法。简单地写

1	#check (IO.println)

会产生一个包含元变量的类型。

1	IO.println : ?m.3620 → IO Unit

这里显示出了元变量是因为即使 Lean 尽全力去寻找隐式参数，但还是没有找到足够的类型信息来做到这一点。要理解函数的签名，可以在函数名之前加上一个 at 符号（@）来抑制此特性。

1
2
3

#check @IO.println

@IO.println : {α : Type u_1} → [inst : ToString α] → α → IO Unit

在这个输出信息中，实例本身被给予了 inst 这个名字。此外，Type 后面有一个 u_1 ，这里使用了目前尚未介绍的 Lean 的特性。我们可以暂时忽略这些 Type 的参数。

定义含隐式实例的多态函数

前边介绍了常规的重载方式，比如为 Nat 定义 Add 实例，为 Pos 定义 ToString 实例。

-- 为具体类型直接定义实例
instance : Add Nat where
  add := Nat.add

instance : ToString Pos where
  toString x := toString (x.toNat)

特点是直接为具体类型提供实现。我们这小节考虑更复杂的情形。先看一个例子，一个对列表中所有条目求和的函数需要两个实例：Add 允许对条目进行加法运算，而 OfNat 实例为 0 提供了一个合理的值，以便对空列表进行返回。

1
2
3

def List.sum [Add α] [OfNat α 0] : List α → α
  | [] => 0
  | x :: xs => x + xs.sum

这个函数可以被用于 Nat 列表：

def fourNats : List Nat := [1, 2, 3, 4]

#eval fourNats.sum

10

由于 Pos 在 0 处没有定义，不能被用于 Pos 列表：

def fourPos : List Pos := [1, 2, 3, 4]

#eval fourPos.sum

failed to synthesize instance
  OfNat Pos 0

上边例子中，在方括号中的所需实例规范被称为 隐式实例（instance implicits） 。在幕后，每个类型类都定义了一个结构，该结构具有每个重载操作的字段。实例是该结构类型的值，每个字段包含一个实现。在调用时，Lean 负责为每个隐式实例参数找到一个实例值传递。

普通的隐式参数和隐式实例最重要的不同就是 Lean 寻找参数值的策略。对于普通的隐式参数，Lean 使用一种被称为 归一化（unification） 的技术来找到一个唯一的能使程序通过类型检查的参数值。这个过程只依赖于函数定义中的具体类型和调用时的类型。

就像对 Pos 的 OfNat 实例用一个自然数 n 作为自动隐式参数，实例本身也可能接受隐式实例参数。在 多态那一节 中展示了一个多态点类型：

structure PPoint (α : Type) where
  x : α
  y : α
deriving Repr

点之间的加法需要将从属的 x 和 y 字段相加。因此，PPoint 的 Add 实例需要这些字段所具有的类型的 Add 实例。换句话说，PPoint 的 Add 实例需要进一步的 α 的 Add 实例。我们用条件实例来表达：

1 2	instance [Add α] : Add (PPoint α) where add p1 p2 := { x := p1.x + p2.x, y := p1.y + p2.y }

当 Lean 遇到两点之间的加法，它会寻找并找到这个实例。然后会更进一步寻找 Add α 实例。

用这种方式构造的实例值是类型类的结构体值。一个成功的递归实例搜索会产生一个结构体值，该结构体值引用了另一个结构体值。比如一个 Add (PPoint Nat) 实例包含对找到的 Add Nat 实例的引用。

这种递归搜索意味着类型类显著地比普通重载函数更加强大。一个多态实例库是一个由代码砖块组成的集合，编译器会根据所需的类型自行搭建。接受实例参数的多态函数是对类型类机制的潜在请求，以在幕后组装辅助函数。API的客户端无需手工组合所有必要的部分，从而使用户从这类烦人的工作中解放出来。

方法与隐式参数

@OfNat.ofNat 的类型可能会令人惊讶。它是 {α : Type} → (n : Nat) → [OfNat α n] → α，其中 Nat 参数 n 作为显式函数参数出现。然而，在方法的声明中，ofNat 只是类型 α。这种看似的不一致是因为声明一个类型类实际上会产生以下结果：

声明一个包含了每个重载操作的实现的结构体类型
声明一个与类同名的命名空间
对于每个方法，会在类的命名空间中声明一个函数，该函数从实例中获取其实现。

这类似于声明新结构也声明访问器函数的方式。主要区别在于结构的访问器函数将结构值作为显式参数，而类型类方法将实例值作为隐式实例，由 Lean 自动查找。

为了让 Lean 找到一个实例，它的参数必须是可用的。这意味着类型类的每个参数必须是出现在实例之前的方法的参数。当这些参数是隐式的时候最方便，因为 Lean 会发现它们的值。例如，@Add.add 的类型是 {α : Type} → [Add α] → α → α → α。在这种情况下，类型参数 α 可以是隐式的，因为对 Add.add 的参数提供了关于用户意图的类型信息。然后，可以使用这种类型来搜索 Add 实例。

而在 ofNat 的例子中，要被解码的特定 Nat 字面量并没有作为其他参数的一部分出现。这意味着 Lean 在尝试确定隐式参数 n 时将没有足够的信息可以用。如果Lean选择使用隐式参数，那么结果将是一个非常不方便的 API。因此，在这些情况下，Lean 选择为类方法提供一个显式参数。

注：在用多参函数表达类型时，参数部分允许 (n : Nat)，但不能出现在函数值

def f : Nat -> (n : Nat) -> Nat := fun a _ => a
#eval f 2 0
2

def g : Nat -> (n : Nat) := sorry
type expected, got
  (n : Nat)Lean 4

练习

偶数数字字面量为 上一节的练习题 中的偶数数据类型写一个使用递归实例搜索的 OfNat 实例。对于基本实例，有必要编写 OfNat Even Nat.zero 而不是 OfNat Even 0。

-- 基本的 OfNat 实例：0 是偶数
instance : OfNat Even 0 where
  ofNat := Even.zero

-- 递归实例：如果 n 是偶数，那么 n+2 也是偶数
-- 这里利用了递归实例搜索：Lean 会自动寻找 OfNat Even n 实例
instance [OfNat Even n] : OfNat Even (n + 2) where
  ofNat := Even.addTwo (OfNat.ofNat n : Even)

#eval (2 : Even)

递归实例搜索深度：Lean 编译器尝试进行递归实例搜素的次数是有限的。这限制了前面的练习中定义的偶数字面量的尺寸。实验性地确定这个上限是多少。

实测为 256：

1	#check (256 : Even)

控制实例搜索

要方便地相加两个 Pos 类型，并产生另一个 Pos，一个 Add 类的的实例就足够了。但是，在许多情况下，参数可能有不同的类型，重载一个灵活的 异质(heterogeneous) 运算符是更为有用的。例如，让 Nat 和 Pos，或 Pos 和 Nat 相加总会是一个 Pos：

def addNatPos : Nat → Pos → Pos
  | 0, p => p
  | n + 1, p => Pos.succ (addNatPos n p)

def addPosNat : Pos → Nat → Pos
  | p, 0 => p
  | p, n + 1 => Pos.succ (addPosNat p n)

这些函数允许自然数与正数相加，但他们不能在 Add 类型类中，因为它希望 add 的两个参数都有同样的类型。

异质重载

就像在重载加法一节提到的，Lean 提供了名为 HAdd 的类型类来重载异质加法。 HAdd 类接受三个类型参数：两个参数的类型和一个返回类型。HAdd Nat Pos Pos 和 HAdd Pos Nat Pos 的实例可以让常规加法符号可以接受不同类型。

instance : HAdd Nat Pos Pos where
  hAdd := addNatPos

instance : HAdd Pos Nat Pos where
  hAdd := addPosNat

有了上面两个实例，就有了下面的例子：

#eval (3 : Pos) + (5 : Nat)
8

#eval (3 : Nat) + (5 : Pos)
8

HAdd 的定义和下面 HPlus 的定义很像。下面是 HPlus 和它对应的实例：

class HPlus (α : Type) (β : Type) (γ : Type) where
  hPlus : α → β → γ

instance : HPlus Nat Pos Pos where
  hPlus := addNatPos

instance : HPlus Pos Nat Pos where
  hPlus := addPosNat

然而，HPlus 的实例明显没有 HAdd 的实例有用。当尝试用 #eval 使用这些实例时，一个错误就出现了：

#eval HPlus.hPlus (3 : Pos) (5 : Nat)

typeclass instance problem is stuck, it is often due to metavariables
  HPlus Pos Nat ?m.7527

发生错误是因为类型中有元变量，Lean 没办法解决它。

就像我们在 多态一开始的描述 里说的那样，元变量代表了程序无法被推断的未知部分。当一个表达式被写在 #eval 后时，Lean 会尝试去自动确定它的类型。在这种情况下，它无法做到自动确定类型。因为 HPlus 的第三个类型参数依然是未知的，Lean 没办法进行类型类实例搜索，但是实例搜索是 Lean 唯一可能确定表达式的类型的方式。也就是说，HPlus Pos Nat Pos 实例只能在表达式的类型为 Pos 时应用，但除了实例本身之外，程序中没有其他东西表明它应该具有这种类型。

一种解决方法是保证全部三个类型都是已知的，通过给整个表达式添加一个类型标记来实现这一点：

1 2	#eval (HPlus.hPlus (3 : Pos) (5 : Nat) : Pos) 8

然而，这种解决方式对使用我们的正数库的用户来说并不是很方便。

输出参数

刚才的问题也可以通过声明 γ 是一个 输出参数（output parameter） 来解决。多数类型类参数是作为搜索算法的输入：它们被用于选取一个实例。例如，在 OfNat 实例中，类型和自然数都被用于选取一个数字字面量的特定解释。然而，在一些情况下，在尽管有些类型参数仍然处于未知状态时就开始进行搜索是更方便的。这样就能使用在搜索中发现的实例来决定元变量的值。在开始搜索实例时不需要用到的参数就是这个过程的结果，该参数使用 outParam 修饰符来声明。

1 2	class HPlus (α : Type) (β : Type) (γ : outParam Type) where hPlus : α → β → γ

有了这个输出参数，类型类实例搜索就能够在不需要知道 γ 的情况下选取一个实例了。例如：

1 2	#eval HPlus.hPlus (3 : Pos) (5 : Nat) 8

在思考时，将输出参数视为定义某种函数可能会有帮助。任意给定的类型类的实例都有一个或更多输出参数提供给 Lean。这能指导 Lean 通过输入（的类型参数）来确定输出（的类型）。一个可能是递归的实例搜索过程，最终会比简单的重载更为强大。输出参数能够决定程序中的其他类型，实例搜索能够将一族附属实例组合成具有这种类型的程序。

默认实例

确定一个参数是否是输入或输出参数控制了 Lean 会在何时启动类型类搜索。具体而言，直到所有输入都变为已知，类型类搜索才会开始。然而，在一些情况下，输出参数是不足的。此时，即使一些输入参数仍然处于未知状态，实例搜索也应该开始。这有点像是 Python 或 Kotlin 中可选函数参数的默认值，但在这里是默认类型。

默认实例 是 当并不是全部输入均为已知时 可用的实例。当一个默认实例能被使用时，他就将会被使用。这能帮助程序成功通过类型检查，而不是因为关于未知类型和元变量的错误而失败。但另一方面，默认类型会让实例选取变得不那么可预测。具体来说，如果一个不合适的实例被选取了，那么表达式将可能具有和预期不同的类型。这会导致令人困惑的类型错误发生在程序中。更聪明做法是根据情况选择要使用默认实例的地方！

默认实例可以发挥作用的一个例子是可以从 Add 实例派生出的 HPlus 实例。换句话说，常规的加法是异质加法在三个参数类型都相同时的特殊情况。这可以用下面的实例来实现：

1 2	instance [Add α] : HPlus α α α where hPlus := Add.add

有了这个实例，hPlus 就可以被用于任何可加的类型，就像 Nat：

1
2
3

#eval HPlus.hPlus (3 : Nat) (5 : Nat)

8

然而，这个实例只会用在两个参数类型都已知的情况下。例如：

1	#check HPlus.hPlus (5 : Nat) (3 : Nat)

产生类型

1	HPlus.hPlus 5 3 : Nat

就像我们预想的那样，但是

1	#check HPlus.hPlus (5 : Nat)

产生了一个包含剩余参数和返回值类型的两个元变量的类型：

1	HPlus.hPlus 5 : ?m.7706 → ?m.7708

在绝大多数情况下，当提供一个加法参数时，另一个参数也会是同一个类型。来让这个实例成为默认实例，应用 default_instance 属性：

1
2
3

@[default_instance]
instance [Add α] : HPlus α α α where
  hPlus := Add.add

有了默认实例，这个例子就有了更有用的类型：

1	#check HPlus.hPlus (5 : Nat)

结果为：

1	HPlus.hPlus 5 : Nat → Nat

每个同时重载了异质和同质运算的运算符，都能在默认实例需要异质运算的语境中使用同质运算。中缀运算符会被替换为异质运算，并且在需要时尽可能选择同质的默认实例。

简单来说，简单地写 5 会给出一个 Nat 而不是一个需要更多信息来选取 OfNat 实例的一个包含元变量的类型。这是因为 OfNat 以 Nat 作为默认实例。

默认实例也可以被赋予 优先级 ，这会影响在可能的应用多于一种的情况下的选择。更多关于默认实例优先级的信息，请查阅 Lean 手册。

练习

定义一个 HMul (PPoint α) α (PPoint α) 的实例，该实例将两个投影都乘以标量。它应适用于任何存在 Mul α 实例的类型 α。例如：

1	#eval {x := 2.5, y := 3.7 : PPoint Float} * 2.0

结果应为

1	{ x := 5.000000, y := 7.400000 }

数组与索引

我们在插曲中描述了如何使用索引符号来通过位置查找列表中的条目。此语法也由类型类管理，并且可以用于各种不同的类型。

数组

比如说，Lean 中的数组在多数情况下就比链表更为高效。在 Lean 中，Array α 类型是一个动态大小的数组，可以用来装类型为 α 的值。这很像是 Java 中的 ArrayList，C++ 中的 std::vector，或者 Rust 中的 Vec。不像是 List 在每一次用到 cons 构造子的地方都会有一个指针指向每个节点，数组会占用内存中一段连续的空间。这会带来更好的处理器缓存效果。并且，在数组中查找值的时间复杂度为常数，但在链表中查找值所需要的时间则与遍历的节点数量成正比。

在像 Lean 这样的纯函数式语言中，在数据结构中改变某位置上的数据的值是不可能的。相反，Lean 会制作一个副本，该副本具有所需的修改。当使用一个数组时，Lean 编译器和运行时包含了一个优化：当该数组只被引用了一次时，会在幕后将制作副本优化为原地操作。

数组写起来很像列表，只是在开头多了一个 #：

1 2	def northernTrees : Array String := #["sloe", "birch", "elm", "oak"]

数组中值的数量可以通过 Array.size 找到。例如：northernTrees.size 结果是 4。对于小于数组大小的索引值，索引符号可以被用来找到对应的值，就像列表一样。就是说，northernTrees[2] 会被计算为 "elm"。类似地，编译器需要一个索引值未越界的证明。尝试去查找越界的值会导致编译时错误，就和列表一样。例如：northernTrees[8] 的结果为：

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 perfomed, 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
⊢ 8 < Array.size northernTrees

非空列表

一个表示非空列表的数据类型可以被定义为一个结构，这个结构有一个列表头字段，和一个尾字段。尾字段是一个常规的，可能为空的列表。

1
2
3

structure NonEmptyList (α : Type) : Type where
  head : α
  tail : List α

例如：非空列表 idahoSpiders（包含了一些美国爱达荷州的本土蜘蛛品种）由 "Banded Garden Spider" 和四种其它蜘蛛构成，一共有五种蜘蛛：

def idahoSpiders : NonEmptyList String := {
  head := "Banded Garden Spider",
  tail := [
    "Long-legged Sac Spider",
    "Wolf Spider",
    "Hobo Spider",
    "Cat-faced Spider"
  ]
}

通过递归函数在列表中查找特定索引的值需要考虑到三种情况：

索引是 0，此时应返回列表头。
索引是 n + 1 并且列表尾是空的，这意味着索引越界了。
索引是 n + 1 并且列表尾非空，此时应该在列表尾上递归调用函数并传入 n。

例如，一个返回 Option 的查找函数可以写成如下形式：

def NonEmptyList.get? : NonEmptyList α → Nat → Option α
  | xs, 0 => some xs.head
  | {head := _, tail := []}, _ + 1 => none
  | {head := _, tail := h :: t}, n + 1 => get? {head := h, tail := t} n

每种模式匹配的情况都对应于上面的一种可能性。 get? 的递归调用不需要 NonEmptyList 命名空间标识符，因为定义内部隐式地在定义的命名空间中。另一种方式来编写这个函数是：当索引大于零时就将 get? 应用在列表上。

1
2
3

def NonEmptyList.get? : NonEmptyList α → Nat → Option α
  | xs, 0 => some xs.head
  | xs, n + 1 => xs.tail.get? n

If the list contains one entry, then only 0 is a valid index. If it contains two entries, then both 0 and 1 are valid indices. If it contains three entries, then 0, 1, and 2 are valid indices. In other words, the valid indices into a non-empty list are natural numbers that are strictly less than the length of the list, which are less than or equal to the length of the tail.

如果列表包含一个条目，那么只有 0 是合法的索引。如果它包含两个条目，那么 0 和 1 是合法的索引。如果它包含三个条目，那么 0, 1, 和 2 都是合法的索引。换句话说，非空列表的合法索引是严格小于列表长度的自然数。同时它也是小于等于列表尾的长度的。

The definition of what it means for an index to be in bounds should be written as an abbrev because the tactics used to find evidence that indices are acceptable are able to solve inequalities of numbers, but they don’t know anything about the name NonEmptyList.inBounds:

“索引值没有出界”意味着什么的这个定义，应该被写成一个 abbrev。因为这个可以用来证明索引值未越界的策略（tactics）要在不知道 NonEmptyList.inBounds 这个方法的情况下解决数字之间的不等关系。 (此处原文表意不明，按原文字面意思译出。原文大致意思应为 abbrev 比 def 对tactic的适应性更好)

1 2	abbrev NonEmptyList.inBounds (xs : NonEmptyList α) (i : Nat) : Prop := i ≤ xs.tail.length

This function returns a proposition that might be true or false. For instance, 2 is in bounds for idahoSpiders, while 5 is not: This function returns a proposition that might be true or false. For instance, 2 is in bounds for idahoSpiders, while 5 is not:

这个函数返回一个可能为真也可能为假的命题。例如，2 对于 idahoSpiders未越界，而 5 就越界了。

1
2
3

theorem atLeastThreeSpiders : idahoSpiders.inBounds 2 := by simp

theorem notSixSpiders : ¬idahoSpiders.inBounds 5 := by simp

The logical negation operator has a very low precedence, which means that ¬idahoSpiders.inBounds 5 is equivalent to ¬(idahoSpiders.inBounds 5).

逻辑非运算符有很低的结合度，这意味着 ¬idahoSpiders.inBounds 5 等价于 ¬(idahoSpiders.inBounds 5)。

This fact can be used to write a lookup function that requires evidence that the index is valid, and thus need not return Option, by delegating to the version for lists that checks the evidence at compile time:

这个事实可被用于编写能证明索引值合法的查找函数，并且无需返回一个 Option。该证据会在编译时检查。下面给出代码：

def NonEmptyList.get (xs : NonEmptyList α) (i : Nat) (ok : xs.inBounds i) : α :=
  match i with
  | 0 => xs.head
  | n + 1 => xs.tail[n]

It is, of course, possible to write this function to use the evidence directly, rather than delegating to a standard library function that happens to be able to use the same evidence. This requires techniques for working with proofs and propositions that are described later in this book.

当然，将这个函数写成直接用证据的形式也是可能的。但这需要会玩证明和命题的一些技术，这些内容会在本书后续内容中提到。

Overloading Indexing

重载索引

Indexing notation for a collection type can be overloaded by defining an instance of the GetElem type class. For the sake of flexiblity, GetElem has four parameters: * The type of the collection * The type of the index * The type of elements that are extracted from the collection * A function that determines what counts as evidence that the index is in bounds

对于集合类型的索引符号，可通过定义 GetElem 类型类的实例来重载。出于灵活性考虑，GetElem 有四个参数：

集合的类型
索引的类型
集合中元素的类型
一个函数，用于确定什么是索引在边界内的证据

The element type and the evidence function are both output parameters. GetElem has a single method, getElem, which takes a collection value, an index value, and evidence that the index is in bounds as arguments, and returns an element:

元素类型和证明函数都是输出参数。 GetElem 有一个方法 —— getElem —— 接受一个集合值，一个索引值，和一个索引未越界的证明，并且返回一个元素：

1 2	class GetElem (coll : Type) (idx : Type) (item : outParam Type) (inBounds : outParam (coll → idx → Prop)) where getElem : (c : coll) → (i : idx) → inBounds c i → item

In the case of NonEmptyList α, these parameters are: * The collection is NonEmptyList α * Indices have type Nat * The type of elements is α * An index is in bounds if it is less than or equal to the length of the tail

在 NonEmptyList α 中，这些参数是：

集合是 NonEmptyList α
索引的类型是 Nat
元素的类型是 α
索引如果小于等于列表尾那么就没有越界

In fact, the GetElem instance can delegate directly to NonEmptyList.get:

事实上，GetElem 实例可以直接使用 NonEmptyList.get：

1 2	instance : GetElem (NonEmptyList α) Nat α NonEmptyList.inBounds where getElem := NonEmptyList.get

With this instance, NonEmptyList becomes just as convenient to use as List. Evaluating idahoSpiders[0] yields "Banded Garden Spider", while idahoSpiders[9] leads to the compile-time error:

有了这个实例，NonEmptyList 就和 List 一样方便了。计算 idahoSpiders[0] 结果为 "Banded Garden Spider"，而 idahoSpiders[9] 会导致编译时错误：

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 perfomed, 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
⊢ NonEmptyList.inBounds idahoSpiders 9

Because both the collection type and the index type are input parameters to the GetElem type class, new types can be used to index into existing collections. The positive number type Pos is a perfectly reasonable index into a List, with the caveat that it cannot point at the first entry. The follow instance of GetElem allows Pos to be used just as conveniently as Nat to find a list entry:

因为集合的类型和索引的类型都是 GetElem 类型类的参数，所以可以使用新类型来索引现有的集合。之前的 Pos 是一个完全合理的可以用来索引 List 的类型，但注意它不能指向第一个条目。下面 GetElem 的实例使 Pos 在查找列表条目方面和 Nat 一样方便。

1 2	instance : GetElem (List α) Pos α (fun list n => list.length > n.toNat) where getElem (xs : List α) (i : Pos) ok := xs[i.toNat]

Indexing can also make sense for non-numeric indices. For example, Bool can be used to select between the fields in a point, with false corresponding to x and true corresponding to y:

使用非数字索引值来进行索引也可以是合理的。例如：Bool 也可以被用于选择点中的字段，比如我们可以让 false 对应于 x，true 对应于 y：

1
2
3

instance : GetElem (PPoint α) Bool α (fun _ _ => True) where
  getElem (p : PPoint α) (i : Bool) _ :=
    if not i then p.x else p.y

In this case, both Booleans are valid indices. Because every possible Bool is in bounds, the evidence is simply the true proposition True.

在这个例子中，布尔值都是合法的索引。因为每个可能的 Bool 值都是未越界的，证据我们只需简单地给出 True 命题。

Standard Classes

标准类

This section presents a variety of operators and functions that can be overloaded using type classes in Lean. Each operator or function corresponds to a method of a type class. Unlike C++, infix operators in Lean are defined as abbreviations for named functions; this means that overloading them for new types is not done using the operator itself, but rather using the underlying name (such as HAdd.hAdd).

本节中展示了各种可重载的运算符和函数。在 Lean 中，它们都通过类型类来重载。每个运算符或函数都对应于一个类型类中的方法。不像 C++，Lean 中的中缀操作符定义为命名函数的缩写；这意味着为新类型重载它们不是使用操作符本身，而是使用其底层名称（例如 HAdd.hAdd）。

Arithmetic

算术符号

Most arithmetic operators are available in a heterogeneous form, where the arguments may have different type and an output parameter decides the type of the resulting expression. For each heterogeneous operator, there is a corresponding homogeneous version that can found by removing the letter h, so that HAdd.hAdd becomes Add.add. The following arithmetic operators are overloaded:

多数算术运算符都是可以进行异质运算的。这意味着参数可能有不同的类型，并且输出参数决定了结果表达式的类型。对于每个异质运算符，都有一个同质运算符与其对应。只要把字母 h 去掉就能找到那个同质运算符了，HAdd.hAdd 对应 Add.add。下面的算术运算符都可以被重载：

Expression	Desugaring	Class Name
`x + y`	`HAdd.hAdd x y`	`HAdd`
`x - y`	`HSub.hSub x y`	`HSub`
`x * y`	`HMul.hMul x y`	`HMul`
`x / y`	`HDiv.hDiv x y`	`HDiv`
`x % y`	`HMod.hMod x y`	`HMod`
`x ^ y`	`HPow.hPow x y`	`HPow`
`(- x)`	`Neg.neg x`	`Neg`

Bitwise Operators

位运算符

Lean contains a number of standard bitwise operators that are overloaded using type classes. There are instances for fixed-width types such as UInt8, UInt16, UInt32, UInt64, and USize. The latter is the size of words on the current platform, typically 32 or 64 bits. The following bitwise operators are overloaded:

Lean 包含了许多标准位运算符，他们也可以用类型类来重载。 Lean 中有对于定长类型的实例，例如 UInt8，UInt16，UInt32，UInt64，和 USize。

Expression	Desugaring	Class Name
`x &&& y`	`HAnd.hAnd x y`	`HAnd`
`x
`x ^^^ y`	`HXor.hXor x y`	`HXor`
`~~~ x`	`Complement.complement x`	`Complement`
`x >>> y`	`HShiftRight.hShiftRight x y`	`HShiftRight`
`x <<< y`	`HShiftLeft.hShiftLeft x y`	`HShiftLeft`
Because the names `And` and `Or` are already taken as the names of logical connectives, the homogeneous versions of `HAnd` and `HOr` are called `AndOp` and `OrOp` rather than `And` and `Or`.

由于 And 和 Or 已经是逻辑连接词了，所以 HAnd 和 HOr 的同质对应叫做 AndOp 和 OrOp 而不是 And 和 Or。

Equality and Ordering

相等性与有序性

Testing equality of two values typically uses the BEq class, which is short for “Boolean equality”. Due to Lean’s use as a theorem prover, there are really two kinds of equality operators in Lean: * Boolean equality is the same kind of equality that is found in other programming languages. It is a function that takes two values and returns a Bool. Boolean equality is written with two equals signs, just as in Python and C#. Because Lean is a pure functional language, there’s no separate notions of reference vs value equality—pointers cannot be observed directly. * Propositional equality is the mathematical statement that two things are equal. Propositional equality is not a function; rather, it is a mathematical statement that admits proof. It is written with a single equals sign. A statement of propositional equality is like a type that classifies evidence of this equality.

测试两个值之间的相等性通常会用 BEq 类，该类名是 Boolean equality（布尔等价）的缩写。由于 Lean 是一个定理证明器，所以在 Lean 中其实有两种类型的相等运算符：

布尔等价（Boolean equality） 和你能在其他编程语言中看到的等价是一样的。这是一个接受两个值并且返回一个 Bool 的函数。布尔等价使用两个等号表示，就像在 Python 和 C# 中那样。因为 Lean 是一个纯函数式语言，指针并不能被直接看到，所以引用和值等价并没有符号上的区别。
命题等价（Propositional equality） 是一个 数学陈述（mathematical statement） ，指两个东西是等价的。命题等价并不是一个函数，而是一个可以证明的数学陈述。可以用一个单等号表示。一个命题等价的陈述就像一个能检查等价性证据的类型。

Both notions of equality are important, and used for different purposes. Boolean equality is useful in programs, when a decision needs to be made about whether two values are equal. For example, "Octopus" == "Cuttlefish" evaluates to false, and "Octopodes" == "Octo".append "podes" evaluates to true. Some values, such as functions, cannot be checked for equality. For example, (fun (x : Nat) => 1 + x) == (Nat.succ ·) yields the error:

这两种等价都很重要，它们有不同的用处。布尔等价在程序中很有用，有时我们需要考察两个值是否是相等的。例如："Octopus" == "Cuttlefish" 结果为 false，以及 "Octopodes" == "Octo".append "podes" 结果为 true。有一些值，比如函数，无法检查等价性。例如，(fun (x : Nat) => 1 + x) == (Nat.succ ·) 会报错：

1 2	failed to synthesize instance BEq (Nat → Nat)

As this message indicates, == is overloaded using a type class. The expression x == y is actually shorthand for BEq.beq x y.

就像这条信息说的，== 是使用了类型类重载的。表达式 x == y 事实上是 BEq.beq x y 的缩写。

Propositional equality is a mathematical statement rather than an invocation of a program. Because propositions are like types that describe evidence for some statement, propositional equality has more in common with types like String and Nat → List Int than it does with Boolean equality. This means that it can’t automatically be checked. However, the equality of any two expressions can be stated in Lean, so long as they have the same type. The statement (fun (x : Nat) => 1 + x) = (Nat.succ ·) is a perfectly reasonable statement. From the perspective of mathematics, two functions are equal if they map equal inputs to equal outputs, so this statement is even true, though it requires a two-line proof to convince Lean of this fact.

命题等价是一个数学陈述，而不是程序调用。因为命题就像描述一些数学陈述的证据的类型，命题等价和像是 String 和 Nat → List Int 这样的类型有更多的相同之处，而不是布尔等价。这意味着它并不能被自动检查。然而，在 Lean 中，只要两个表达式具有相同的类型，就可以陈述它们的相等性。 (fun (x : Nat) => 1 + x) = (Nat.succ ·) 是一个十分合理的陈述。从数学角度来讲，如果两个函数把相等的输入映射到相等的输出，那么这两个函数就是相等的。所以那个陈述是真的，尽管它需要一个两行的证明来让 Lean 相信这个事实。

Generally speaking, when using Lean as a programming language, it’s easiest to stick to Boolean functions rather than propositions. However, as the names true and false for Bool’s constructors suggest, this difference is sometimes blurred. Some propositions are decidable, which means that they can be checked just like a Boolean function. The function that checks whether the proposition is true or false is called a decision procedure, and it returns evidence of the truth or falsity of the proposition. Some examples of decidable propositions include equality and inequality of natural numbers, equality of strings, and “ands” and “ors” of propositions that are themselves decidable.

通常来说，当把 Lean 作为一个编程语言来用时，用布尔值函数会比用命题要更简单。

In Lean, if works with decidable propositions. For example, 2 < 4 is a proposition:

在 Lean 中，if 语句适用于可判定命题。例如：2 < 4 是一个命题。

#check 2 < 4



2 < 4 : Prop

Nonetheless, it is perfectly acceptable to write it as the condition in an if. For example, if 2 < 4 then 1 else 2 has type Nat and evaluates to 1.

尽管如此，将其写作 if 语句中的条件是完全可以接受的。例如，if 2 < 4 then 1 else 2 的类型是 Nat，并且计算结果为 1。

Not all propositions are decidable. If they were, then computers would be able to prove any true proposition just by running the decision procedure, and mathematicians would be out of a job. More specifically, decidable propositions have an instance of the Decidable type class which has a method that is the decision procedure. Trying to use a proposition that isn’t decidable as if it were a Bool results in a failure to find the Decidable instance. For example, if (fun (x : Nat) => 1 + x) = (Nat.succ ·) then "yes" else "no" results in:

并不是所有的命题都是可判定的。如果所有的命题都是可判定的，那么计算机通过运行判定程序就可以证明任何的真命题，数学家们就此失业了。更具体来说，可判定的命题都会有一个 Decidable 类型的实例，实例中的方法是判定程序。因为认为会返回一个 Bool 而尝试去用一个不可判定的命题，最终会报错，因为 Lean 无法找到 Decidable 实例。例如，if (fun (x : Nat) => 1 + x) = (Nat.succ ·) then "yes" else "no" 会导致：

1 2	failed to synthesize instance Decidable ((fun x => 1 + x) = fun x => Nat.succ x)

The following propositions, that are usually decidable, are overloaded with type classes:

下面的命题，通常都是重载了可判定类型类的：

Expression	Desugaring	Class Name
`x < y`	`LT.lt x y`	`LT`
`x ≤ y`	`LE.le x y`	`LE`
`x > y`	`LT.lt y x`	`LT`
`x ≥ y`	`LE.le y x`	`LE`
Because defining new propositions hasn’t yet been demonstrated, it may be difficult to define new instances of `LT` and `LE`.

因为还没有演示如何定义新命题，所以定义新的 LT 和 LE 实例可能会比较困难。

Additionally, comparing values using <, ==, and > can be inefficient. Checking first whether one value is less than another, and then whether they are equal, can require two traversals over large data structures. To solve this problem, Java and C# have standard compareTo and CompareTo methods (respectively) that can be overridden by a class in order to implement all three operations at the same time. These methods return a negative integer if the receiver is less than the argument, zero if they are equal, and a positive integer if the receiver is greater than the argument. Rather than overload the meaning of integers, Lean has a built-in inductive type that describes these three possibilities:

另外，使用 <, ==, 和 > 来比较值可能效率不高。首先检查一个值是否小于另一个值，然后再检查它们是否相等，这可能需要对大型数据结构进行两次遍历。为了解决这个问题，Java 和 C# 分别有标准的 compareTo 和 CompareTo 方法，可以通过类来重写以同时实现这三种操作。这些方法在接收者小于参数时返回负整数，等于时返回零，大于时返回正整数。 Lean 与其重载整数，不如有一个内置的归纳类型来描述这三种可能性：

inductive Ordering where
| lt
| eq
| gt

The Ord type class can be overloaded to produce these comparisons. For Pos, an implementation can be:

Ord 类型类可以被重载，这样就可以用于比较。对于 Pos 一个实现可以是：

def Pos.comp : Pos → Pos → Ordering
  | Pos.one, Pos.one => Ordering.eq
  | Pos.one, Pos.succ _ => Ordering.lt
  | Pos.succ _, Pos.one => Ordering.gt
  | Pos.succ n, Pos.succ k => comp n k

instance : Ord Pos where
  compare := Pos.comp

In situations where compareTo would be the right approach in Java, use Ord.compare in Lean.

对于 Java 中应该使用 compareTo 的情形，在 Lean 中用 Ord.compare 就对了。

Hashing

哈希

Java and C# have hashCode and GetHashCode methods, respectively, that compute a hash of a value for use in data structures such as hash tables. The Lean equivalent is a type class called Hashable:

Java 和 C# 有 hashCode 和 GetHashCode 方法，用于计算值的哈希值，以便在哈希表等数据结构中使用。 Lean 中的等效类型类称为 Hashable：

1 2	class Hashable (α : Type) where hash : α → UInt64

If two values are considered equal according to a BEq instance for their type, then they should have the same hashes. In other words, if x == y then hash x == hash y. If x ≠ y, then hash x won’t necessarily differ from hash y (after all, there are infinitely more Nat values than there are UInt64 values), but data structures built on hashing will have better performance if unequal values are likely to have unequal hashes. This is the same expectation as in Java and C#.

对于两个值而言，如果它们根据各自类型的 BEq 实例是相等的，那么它们也应该有相同的哈希值。换句话说，如果 x == y，那么有 hash x == hash y。如果 x ≠ y，那么 hash x 不一定就和 hash y 不一样（毕竟 Nat 有无穷多个，而 UInt64 最多只能有有限种组合方式。），但是如果不一样的值有不一样的哈希值的话，那么建立在其上的数据结构会有更好的表现。这与 Java 和 C# 中对哈希的要求是一致的。

The standard library contains a function mixHash with type UInt64 → UInt64 → UInt64 that can be used to combine hashes for different fields for a constructor. A reasonable hash function for an inductive datatype can be written by assigning a unique number to each constructor, and then mixing that number with the hashes of each field. For example, a Hashable instance for Pos can be written:

在标准库中包含了一个函数 mixHash，它的类型是 UInt64 → UInt64 → UInt64。它可以用来组合构造子不同字段的哈希值。一个合理的归纳数据类型的哈希函数可以通过给每个构造函数分配一个唯一的数字，然后将该数字与每个字段的哈希值混合来编写。例如，可以这样编写 Pos 的 Hashable 实例：

def hashPos : Pos → UInt64
  | Pos.one => 0
  | Pos.succ n => mixHash 1 (hashPos n)

instance : Hashable Pos where
  hash := hashPos

Hashable instances for polymorphic types can use recursive instance search. Hashing a NonEmptyList α is only possible when α can be hashed:

Hashable 实例对于多态可以使用递归类型搜索。哈希化一个 NonEmptyList α 需要 α 是可以被哈希化的。

1 2	instance [Hashable α] : Hashable (NonEmptyList α) where hash xs := mixHash (hash xs.head) (hash xs.tail)

Binary trees use both recursion and recursive instance search in the implementations of BEq and Hashable:

在二叉树的 BEq 和 Hashable 的实现中，递归和递归实例搜索这二者都被用到了。

inductive BinTree (α : Type) where
  | leaf : BinTree α
  | branch : BinTree α → α → BinTree α → BinTree α

def eqBinTree [BEq α] : BinTree α → BinTree α → Bool
  | BinTree.leaf, BinTree.leaf =>
    true
  | BinTree.branch l x r, BinTree.branch l2 x2 r2 =>
    x == x2 && eqBinTree l l2 && eqBinTree r r2
  | _, _ =>
    false

instance [BEq α] : BEq (BinTree α) where
  beq := eqBinTree

def hashBinTree [Hashable α] : BinTree α → UInt64
  | BinTree.leaf =>
    0
  | BinTree.branch left x right =>
    mixHash 1 (mixHash (hashBinTree left) (mixHash (hash x) (hashBinTree right)))

instance [Hashable α] : Hashable (BinTree α) where
  hash := hashBinTree

Deriving Standard Classes

派生标准类

Instance of classes like BEq and Hashable are often quite tedious to implement by hand. Lean includes a feature called instance deriving that allows the compiler to automatically construct well-behaved instances of many type classes. In fact, the deriving Repr phrase in the definition of Point in the section on structures is an example of instance deriving.

像 BEq 和 Hashable 这样的类的实例，手动实现起来通常相当繁琐。Lean 包含一个称为 实例派生（instance deriving） 的特性，它使得编译器可以自动构造许多类型类的良好实例。事实上，结构那一节中 Point 定义中的 deriving Repr 短语就是实例派生的一个例子。

Instances can be derived in two ways. The first can be used when defining a structure or inductive type. In this case, add deriving to the end of the type declaration followed by the names of the classes for which instances should be derived. For a type that is already defined, a standalone deriving command can be used. Write deriving instance C1, C2, ... for T to derive instances of C1, C2, ... for the type T after the fact.

派生实例的方法有两种。第一种在定义一个结构体或归纳类型时使用。在这种情况下，添加 deriving 到类型声明的末尾，后面再跟实例应该派生自的类。对于已经定义好的类型，单独的 deriving 也是可用的。写 deriving instance C1, C2, ... for T 来为类型 T 派生 C1, C2, ... 实例。

BEq and Hashable instances can be derived for Pos and NonEmptyList using a very small amount of code:

Pos 和 NonEmptyList 上的 BEq 和 Hashable 实例可以用很少量的代码派生出来：

1 2	deriving instance BEq, Hashable for Pos deriving instance BEq, Hashable, Repr for NonEmptyList

Instances can be derived for at least the following classes: * Inhabited * BEq * Repr * Hashable * Ord

至少以下几种类型类的实例都是可以派生的：

Inhabited
BEq
Repr
Hashable
Ord

In some cases, however, the derived Ord instance may not produce precisely the ordering desired in an application. When this is the case, it’s fine to write an Ord instance by hand. The collection of classes for which instances can be derived can be extended by advanced users of Lean.

然而，有些时候 Ord 的派生实例可能不是你想要的。当发生这种事情的时候，就手写一个 Ord 实例把。你如果对自己的 Lean 水平足够有自信的话，你也可以自己添加可以派生实例的类型类。

Aside from the clear advantages in programmer productivity and code readability, deriving instances also makes code easier to maintain, because the instances are updated as the definitions of types evolve. Changesets involving updates to datatypes are easier to read without line after line of formulaic modifications to equality tests and hash computation.

实例派生除了在开发效率和代码可读性上有很大的优势外，它也使得代码更易于维护，因为实例会随着类型定义的变化而更新。对数据类型的一系列更新更易于阅读，因为不需要一行又一行地对相等性测试和哈希计算进行公式化的修改。

Appending

Many datatypes have some sort of append operator. In Lean, appending two values is overloaded with the type class HAppend, which is a heterogeneous operation like that used for arithmetic operations:

许多数据类型都有某种形式的连接操作符。在 Lean 中，连接两个值的操作被重载为类型类 HAppend，这是一个异质操作，与用于算术运算的操作类似：

1 2	class HAppend (α : Type) (β : Type) (γ : outParam Type) where hAppend : α → β → γ

The syntax xs ++ ys desugars to HAppend.hAppend xs ys. For homogeneous cases, it’s enough to implement an instance of Append, which follows the usual pattern:

语法 xs ++ ys 会被脱糖为 HAppend.hAppend xs ys. 对于同质的情形，按照常规模式实现一个 Append 即可：

1
2
3

instance : Append (NonEmptyList α) where
  append xs ys :=
    { head := xs.head, tail := xs.tail ++ ys.head :: ys.tail }

After defining the above instance,

在定义了上面的实例后，

1	#eval idahoSpiders ++ idahoSpiders

has the following output:

就有了下面的结果：

{ head := "Banded Garden Spider",
tail := ["Long-legged Sac Spider",
         "Wolf Spider",
         "Hobo Spider",
         "Cat-faced Spider",
         "Banded Garden Spider",
         "Long-legged Sac Spider",
         "Wolf Spider",
         "Hobo Spider",
         "Cat-faced Spider"] }

Similarly, a definition of HAppend allows non-empty lists to be appended to ordinary lists:

类似地：定义一个 HAppend 来使常规列表可以和一个非空列表连接。

1
2
3

instance : HAppend (NonEmptyList α) (List α) (NonEmptyList α) where
  hAppend xs ys :=
    { head := xs.head, tail := xs.tail ++ ys }

With this instance available,

有了这个实例后，

1	#eval idahoSpiders ++ ["Trapdoor Spider"]

results in

结果为

1 2	{ head := "Banded Garden Spider", tail := ["Long-legged Sac Spider", "Wolf Spider", "Hobo Spider", "Cat-faced Spider", "Trapdoor Spider"] }

Functors

函子

A polymorphic type is a functor if it has an overload for a function named map that transforms every element contained in it by a function. While most languages use this terminology, C#'s equivalent to map is called System.Linq.Enumerable.Select. For example, mapping a function over a list constructs a new list in which each entry from the starting list has been replaced by the result of the function on that entry. Mapping a function f over an Option leaves none untouched, and replaces some x with some (f x).

如果一个多态类型重载了一个函数 map，这个函数将位于上下文中的每个元素都用一个函数来映射，那么这个类型就是一个 函子（functor） 。虽然大多数语言都使用这个术语，但C#中等价于 map 的是 System.Linq.Enumerable.Select。例如，用一个函数对一个列表进行映射会产生一个新的列表，列表中的每个元素都是函数应用在原列表中元素的结果。用函数 f 对一个 Option 进行映射，如果 Option 的值为 none，那么结果仍为 none；如果为 some x，那么结果为 some (f x)。

Here are some examples of functors and how their Functor instances overload map: * Functor.map (· + 5) [1, 2, 3] evaluates to [6, 7, 8] * Functor.map toString (some (List.cons 5 List.nil)) evaluates to some "[5]" * Functor.map List.reverse [[1, 2, 3], [4, 5, 6]] evaluates to [[3, 2, 1], [6, 5, 4]]

下面是一些函子，这些函子是如何重载 map 的例子：

Functor.map (· + 5) [1, 2, 3] 结果为 [6, 7, 8]
Functor.map toString (some (List.cons 5 List.nil)) 结果为 some "[5]"
Functor.map List.reverse [[1, 2, 3], [4, 5, 6]] 结果为 [[3, 2, 1], [6, 5, 4]]

Because Functor.map is a bit of a long name for this common operation, Lean also provides an infix operator for mapping a function, namely <$>. The prior examples can be rewritten as follows: * (· + 5) <$> [1, 2, 3] evaluates to [6, 7, 8] * toString <$> (some (List.cons 5 List.nil)) evaluates to some "[5]" * List.reverse <$> [[1, 2, 3], [4, 5, 6]] evaluates to [[3, 2, 1], [6, 5, 4]]

因为 Functor.map 这个操作很常用，但它的名字又有些长了，所以 Lean 也提供了一个中缀运算符来映射函数，叫做 <$>。下面是一些简单的例子：

(· + 5) <$> [1, 2, 3] 结果为 [6, 7, 8]
toString <$> (some (List.cons 5 List.nil)) 结果为 some "[5]"
List.reverse <$> [[1, 2, 3], [4, 5, 6]] 结果为 [[3, 2, 1], [6, 5, 4]]

An instance of Functor for NonEmptyList requires specifying the map function.

Functor 对于 NonEmptyList 的实例需要我们提供 map 函数。

1 2	instance : Functor NonEmptyList where map f xs := { head := f xs.head, tail := f <$> xs.tail }

Here, map uses the Functor instance for List to map the function over the tail. This instance is defined for NonEmptyList rather than for NonEmptyList α because the argument type α plays no role in resolving the type class. A NonEmptyList can have a function mapped over it no matter what the type of entries is. If α were a parameter to the class, then it would be possible to make versions of Functor that only worked for NonEmptyList Nat, but part of being a functor is that map works for any entry type.

在这里，map 使用 List 上的 Functor 实例来将函数映射到列表尾。这个实例是在 NonEmptyList 下定义的，而不是 NonEmptyList α。因为类型参数 α 在当前类型类中用不上。 无论条目的类型是什么 ，我们都可以用一个函数来映射 NonEmptyList。如果 α 是类型类的一个参数，那么我们就可以做出只工作在某个 α 类型上的 Functor，比如 NonEmptyList Nat。但成为一个函子类型的必要条件就是 map 对任意条目类型都是有效的。

Here is an instance of Functor for PPoint:

这里有一个将 PPoint 实现为一个函子的实例：

1 2	instance : Functor PPoint where map f p := { x := f p.x, y := f p.y }

In this case, f has been applied to both x and y.

在这里，f 被应用到 x 和 y 上。

Even when the type contained in a functor is itself a functor, mapping a function only goes down one layer. That is, when using map on a NonEmptyList (PPoint Nat), the function being mapped should take PPoint Nat as its argument rather than Nat.

即使包含在一个函子类型中的类型本身也是一个函子，映射一个函数也只会向下一层。也就是说，当在 NonEmptyList (PPoint Nat) 上 map 时，被映射的函数会接受 PPoint Nat 作为参数，而不是 Nat。

The definition of the Functor class uses one more language feature that has not yet been discussed: default method definitions. Normally, a class will specify some minimal set of overloadable operations that make sense together, and then use polymorphic functions with instance implicit arguments that build on the overloaded operations to provide a larger library of features. For example, the function concat can concatenate any non-empty list whose entries are appendable:

Functor 类型类的定义中用到了一个还没介绍的语言特性：默认方法定义。正常来说，一个类型类会指定一些有意义的最小的可重载操作集合，然后使用具有隐式实例参数的多态函数，这些函数建立在重载操作的基础上，以提供更大的功能库。例如，函数 concat 可以连接任何非空列表的条目，只要条目是可连接的：

def concat [Append α] (xs : NonEmptyList α) : α :=
  let rec catList (start : α) : List α → α
    | [] => start
    | (z :: zs) => catList (start ++ z) zs
  catList xs.head xs.tail

However, for some classes, there are operations that can be more efficiently implemented with knowledge of the internals of a datatype.

然而，对于一些类型类，如果你对数据类型的内部又更深的理解的话，那么就会有一些更高效的运算实现。

In these cases, a default method definition can be provided. A default method definition provides a default implementation of a method in terms of the other methods. However, instance implementors may choose to override this default with something more efficient. Default method definitions contain := in a class definition.

在这些情况下，可以提供一个默认方法定义。默认方法定义提供了一个基于其他方法的默认实现。然而，实例实现者可以选择用更高效的方法来重写这个默认实现。默认方法定义在 class 定义中，包含 :=。

In the case of Functor, some types have a more efficient way of implementing map when the function being mapped ignores its argument. Functions that ignore their arguments are called constant functions because they always return the same value. Here is the definition of Functor, in which mapConst has a default implementation:

对于 Functor 而言，当被映射的函数并不需要参数时，许多类型有更高效的 map 实现方式。

class Functor (f : Type → Type) where
  map : {α β : Type} → (α → β) → f α → f β

  mapConst {α β : Type} (x : α) (coll : f β) : f α :=
    map (fun _ => x) coll

Just as a Hashable instance that doesn’t respect BEq is buggy, a Functor instance that moves around the data as it maps the function is also buggy. For example, a buggy Functor instance for List might throw away its argument and always return the empty list, or it might reverse the list. A bad instance for PPoint might place f x in both the x and the y fields. Specifically, Functor instances should follow two rules: 1. Mapping the identity function should result in the original argument. 2. Mapping two composed functions should have the same effect as composing their mapping.

就像不符合 BEq 的 Hashable 实例是有问题的一样，一个在映射函数时移动数据的 Functor 实例也是有问题的。例如，一个有问题的 List 的 Functor 实例可能会丢弃其参数并总是返回空列表，或者它可能会反转列表。一个有问题的 PPoint 实例可能会将 f x 放在 x 和 y 字段中。具体来说，Functor 实例应遵循两条规则：

映射恒等函数应返回原始参数。
映射两个复合函数应具有与它们的映射组合相同的效果。

More formally, the first rule says that id <$> x equals x. The second rule says that map (fun y => f (g y)) x equals map f (map g x). The composition fun y => f (g y) can also be written f ∘ g. These rules prevent implementations of map that move the data around or delete some of it.

更形式化的讲，第一个规则说 id <$> x 等于 x。第二个规则说 map (fun y => f (g y)) x 等于 map f (map g x)。 fun y => f (g y) 也可以写成 f ∘ g。这些规则能防止 map 的实现移动数据或删除一些数据。

Messages You May Meet

你也许会遇到的问题

Lean is not able to derive instances for all classes. For example, the code

Lean 不能为所有类派生实例。例如代码

1	deriving instance ToString for NonEmptyList

results in the following error:

会导致如下错误：

1	default handlers have not been implemented yet, class: 'ToString' types: [NonEmptyList]

Invoking deriving instance causes Lean to consult an internal table of code generators for type class instances. If the code generator is found, then it is invoked on the provided type to create the instance. This message, however, means that no code generator was found for ToString.

调用 deriving instance 会使 Lean 查找一个类型类实例的内部代码生成器的表。如果找到了代码生成器，那么就会调用它来创建实例。然而这个报错就意味着没有发现对 ToString 的代码生成器。

Exercises

练习

Write an instance of HAppend (List α) (NonEmptyList α) (NonEmptyList α) and test it. * Implement a Functor instance for the binary tree datatype.
- 写一个 HAppend (List α) (NonEmptyList α) (NonEmptyList α) 的实例并测试它
- 为二叉树实现一个 Functor 的实例。

Coercions

强制转换

In mathematics, it is common to use the same symbol to stand for different aspects of some object in different contexts. For example, if a ring is referred to in a context where a set is expected, then it is understood that the ring’s underlying set is what’s intended. In programming languages, it is common to have rules to automatically translate values of one type into values of another type. For instance, Java allows a byte to be automatically promoted to an int, and Kotlin allows a non-nullable type to be used in a context that expects a nullable version of the type.

在数学中，用同一个符号来在不同的语境中代表数学对象的不同方面是很常见的。例如，如果在一个需要集合的语境中给出了一个环，那么理解为该环对应的集合也是很有道理的。在编程语言中，有一些规则自动地将一种类型转换为另一种类型也是很常见的。例如，Java 允许 byte 自动转换为一个 int，Kotlin 也允许非空类型在可为空的语境中使用。

In Lean, both purposes are served by a mechanism called coercions. When Lean encounters an expression of one type in a context that expects a different type, it will attempt to coerce the expression before reporting a type error. Unlike Java, C, and Kotlin, the coercions are extensible by defining instances of type classes.

在 Lean 中，这两个目的都是用一个叫做 强制转换（coercions） 的机制实现的。当 Lean 遇到了在某语境中某表达式的类型与期望类型不一致时，Lean 在报错前会尝试进行强制转换。不像 Java，C，和 Kotlin，强制转换是通过定义类型类实例实现的，并且是可扩展的。

Positive Numbers

正数

For example, every positive number corresponds to a natural number. The function Pos.toNat that was defined earlier converts a Pos to the corresponding Nat:

例如，每个正数都对应一个自然数。之前定义的函数 Pos.toNat 可以将一个 Pos 转换成对应的 Nat：

1
2
3

def Pos.toNat : Pos → Nat
  | Pos.one => 1
  | Pos.succ n => n.toNat + 1

The function List.drop, with type {α : Type} → Nat → List α → List α, removes a prefix of a list. Applying List.drop to a Pos, however, leads to a type error:

函数 List.drop，的类型是 {α : Type} → Nat → List α → List α，它将列表的前缀移除。将 List.drop 应用到 Pos 会产生一个类型错误：

[1, 2, 3, 4].drop (2 : Pos)



application type mismatch
  List.drop 2
argument
  2
has type
  Pos : Type
but is expected to have type
  Nat : Type

Because the author of List.drop did not make it a method of a type class, it can’t be overridden by defining a new instance.

因为 List.drop 的作者没有让它成为一个类型类的方法，所以它没有办法通过定义新实例的方式来重写。

The type class Coe describes overloaded ways of coercing from one type to another:

Coe 类型类描述了类型间强制转换的重载方法。

1 2	class Coe (α : Type) (β : Type) where coe : α → β

An instance of Coe Pos Nat is enough to allow the prior code to work:

一个 Coe Pos Nat 的实例就足够让先前的代码正常工作了。

instance : Coe Pos Nat where
  coe x := x.toNat

#eval [1, 2, 3, 4].drop (2 : Pos)



[3, 4]

Using #check shows the result of the instance search that was used behind the scenes:

用 #check 来看隐藏在幕后的实例搜索。

#check [1, 2, 3, 4].drop (2 : Pos)



List.drop (Pos.toNat 2) [1, 2, 3, 4] : List Nat

Chaining Coercions

链式强制转换

When searching for coercions, Lean will attempt to assemble a coercion out of a chain of smaller coercions. For example, there is already a coercion from Nat to Int. Because of that instance, combined with the Coe Pos Nat instance, the following code is accepted:

在寻找强制转换时，Lean 会尝试通过一系列较小的强制转换来组成一个完整的强制转换。例如，已经存在一个从 Nat 到 Int 的强制转换实例。由于这个实例结合了 Coe Pos Nat 实例，我们就可以写出下面的代码：

1	def oneInt : Int := Pos.one

This definition uses two coercions: from Pos to Nat, and then from Nat to Int.

这个定义用到了两个强制转换：从 Pos 到 Nat，再从 Nat 到 Int。

The Lean compiler does not get stuck in the presence of circular coercions. For example, even if two types A and B can be coerced to one another, their mutual coercions can be used to find a path:

Lean 编译器在存在循环强制转换的情况下不会陷入无限循环。例如，即使两个类型 A 和 B 可以互相强制转换，在转换中 Lean 也可以找到一个路径。

inductive A where
  | a

inductive B where
  | b

instance : Coe A B where
  coe _ := B.b

instance : Coe B A where
  coe _ := A.a

instance : Coe Unit A where
  coe _ := A.a

def coercedToB : B := ()

Remember: the double parentheses () is short for the constructor Unit.unit. After deriving a Repr B instance,

提示：双括号 () 是构造子 Unit.unit 的简写。在派生 Repr B 实例后，

1	#eval coercedToB

results in:

结果为：

B.b

The Option type can be used similarly to nullable types in C# and Kotlin: the none constructor represents the absence of a value. The Lean standard library defines a coercion from any type α to Option α that wraps the value in some. This allows option types to be used in a manner even more similar to nullable types, because some can be omitted. For instance, the function List.getLast? that finds the last entry in a list can be written without a some around the return value x:

Option 类型类似于 C# 和 Kotlin 中可为空的类型：none 构造子就代表了一个不存在的值。 Lean 标准库定义了一个从任意类型 α 到 Option α 的强制转换，效果是会将值包裹在 some 中。这使得 option 类型用起来更像是其他语言中可为空的类型，因为 some 是可以忽略的。例如，可以找到列表中最后一个元素的函数 List.getLast?，就可以直接返回值 x 而无需加上 some：

def List.last? : List α → Option α
  | [] => none
  | [x] => x
  | _ :: x :: xs => last? (x :: xs)

Instance search finds the coercion, and inserts a call to coe, which wraps the argument in some. These coercions can be chained, so that nested uses of Option don’t require nested some constructors:

实例搜索找到强制转换，并插入对 coe 的调用，该调用会将参数包装在 some 中。这些强制转换可以是链式的，这样嵌套使用 Option 时就不需要嵌套的 some 构造子：

1 2	def perhapsPerhapsPerhaps : Option (Option (Option String)) := "Please don't tell me"

Coercions are only activated automatically when Lean encounters a mismatch between an inferred type and a type that is imposed from the rest of the program. In cases with other errors, coercions are not activated. For example, if the error is that an instance is missing, coercions will not be used:

仅当 Lean 遇到推断出的类型和剩下的程序需要的类型不匹配时，才会自动使用强制转换。在遇到其它错误时，强制转换不会被使用。例如，如果遇到的错误是实例缺失，强制类型转换不会被使用：

def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
  392

1 2	failed to synthesize instance OfNat (Option (Option (Option Nat))) 392

This can be worked around by manually indicating the desired type to be used for OfNat:

这可以通过手动指定 OfNat 所需的类型来解决：

1 2	def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) := (392 : Nat)

Additionally, coercions can be manually inserted using an up arrow:

此外，强制转换用一个上箭头手动调用。

1 2	def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) := ↑(392 : Nat)

In some cases, this can be used to ensure that Lean finds the right instances. It can also make the programmer’s intentions more clear.

在一些情况下，这可以保证 Lean 找到了正确的实例。这也会让程序员的意图更加清晰。

Non-Empty Lists and Dependent Coercions

非空列表与依值强制转换

An instance of Coe α β makes sense when the type β has a value that can represent each value from the type α. Coercing from Nat to Int makes sense, because the type Int contains all the natural numbers. Similarly, a coercion from non-empty lists to ordinary lists makes sense because the List type can represent every non-empty list:

当 β 类型中的值可以对应每一个 α 类型中的值时，Coe α β 实例才是合理的。将 Nat 强制转换为 Int 是合理的，因为 Int 类型中包含了全部的自然数。类似地，一个从非空列表到常规列表的强制转换也是合理的，因为 List 类型可以表示每一个非空列表：

1
2
3

instance : Coe (NonEmptyList α) (List α) where
  coe
    | { head := x, tail := xs } => x :: xs

This allows non-empty lists to be used with the entire List API.

这使得非空列表可以使用全部的 List API。

On the other hand, it is impossible to write an instance of Coe (List α) (NonEmptyList α), because there’s no non-empty list that can represent the empty list. This limitation can be worked around by using another version of coercions, which are called dependent coercions. Dependent coercions can be used when the ability to coerce from one type to another depends on which particular value is being coerced. Just as the OfNat type class takes the particular Nat being overloaded as a parameter, dependent coercion takes the value being coerced as a parameter:

另一方面，我们不可能写出一个 Coe (List α) (NonEmptyList α) 的实例，因为没有任何一个非空列表可以表示一个空列表。这个限制可以通过其他方式的强制转换来解决，该强制转换被称为 依值强制转换（dependent coercions） 。当是否能将一种类型强制转换到另一种类型依赖于具体的值时，依值强制转换就派上用场了。就像 OfNat 类型类需要具体的 Nat 来作为参数，依值强制转换也接受要被强制转换的值作为参数：

1 2	class CoeDep (α : Type) (x : α) (β : Type) where coe : β

This is a chance to select only certain values, either by imposing further type class constraints on the value or by writing certain constructors directly. For example, any List that is not actually empty can be coerced to a NonEmptyList:

这可以使得只选取特定的值，通过加上进一步的类型类约束或者直接写出特定的构造子。例如，任意非空的 List 都可以被强制转换为一个 NonEmptyList：

1 2	instance : CoeDep (List α) (x :: xs) (NonEmptyList α) where coe := { head := x, tail := xs }

Coercing to Types

强制转换为类型（本节中 sort 的翻译待讨论）

In mathematics, it is common to have a concept that consists of a set equipped with additional structure. For example, a monoid is some set S, an element s of S, and an associative binary operator on S, such that s is neutral on the left and right of the operator. S is referred to as the “carrier set” of the monoid. The natural numbers with zero and addition form a monoid, because addition is associative and adding zero to any number is the identity. Similarly, the natural numbers with one and multiplication also form a monoid. Monoids are also widely used in functional programming: lists, the empty list, and the append operator form a monoid, as do strings, the empty string, and string append:

在数学中，一个建立在集合上，但是比集合具有额外的结构的概念是很常见的。例如，一个幺半群就是一些集合 S ，一个 S 中的元素 s ，以及一个 S 上结合的二元运算，使得 s 在运算的左侧和右侧都是中性的。 S 是这个幺半群的“载体集”。自然数集上的零和加法构成一个幺半群，因为加法是满足结合律的，并且为任何一个数字加零都是恒等的。类似地，自然数上的一和乘法也构成一个幺半群。幺半群在函数式编程中的应用也很广泛：列表，空列表，和连接运算符构成一个幺半群。字符串，空字符串，和连接运算符也构成一个幺半群：

structure Monoid where
  Carrier : Type
  neutral : Carrier
  op : Carrier → Carrier → Carrier

def natMulMonoid : Monoid :=
  { Carrier := Nat, neutral := 1, op := (· * ·) }

def natAddMonoid : Monoid :=
  { Carrier := Nat, neutral := 0, op := (· + ·) }

def stringMonoid : Monoid :=
  { Carrier := String, neutral := "", op := String.append }

def listMonoid (α : Type) : Monoid :=
  { Carrier := List α, neutral := [], op := List.append }

Given a monoid, it is possible to write the foldMap function that, in a single pass, transforms the entries in a list into a monoid’s carrier set and then combines them using the monoid’s operator. Because monoids have a neutral element, there is a natural result to return when the list is empty, and because the operator is associative, clients of the function don’t have to care whether the recursive function combines elements from left to right or from right to left.

给定一个幺半群，我们就可以写出一个 foldMap 函数，该函数在一次遍历中将整个列表中的元素映射到载体集中，然后使用幺半群的运算符将它们组合起来。由于幺半群有单位元，所以当列表为空时我们就可以返回这个值。又因为运算符是满足结合律的，这个函数的用户不需要关心函数结合元素的顺序到底是从左到右的还是从右到左的。

def foldMap (M : Monoid) (f : α → M.Carrier) (xs : List α) : M.Carrier :=
  let rec go (soFar : M.Carrier) : List α → M.Carrier
    | [] => soFar
    | y :: ys => go (M.op soFar (f y)) ys
  go M.neutral xs

Even though a monoid consists of three separate pieces of information, it is common to just refer to the monoid’s name in order to refer to its set. Instead of saying “Let A be a monoid and let x and y be elements of its carrier set”, it is common to say “Let A be a monoid and let x and y be elements of A”. This practice can be encoded in Lean by defining a new kind of coercion, from the monoid to its carrier set.

尽管一个幺半群是由三部分信息组成的，但在提及它的载体集时使用幺半群的名字也是很常见的。说“令 A 为一个幺半群，并令 x 和 y 为 A 中的元素”是很常见的，而不是说“令 A 为一个幺半群，并令 x 和 y 为载体集中的元素”。这种方式可以通过定义一种新的强制转换来在 Lean 中实现，该转换从幺半群到它的载体集。

The CoeSort class is just like the Coe class, with the exception that the target of the coercion must be a sort, namely Type or Prop. The term sort in Lean refers to these types that classify other types—Type classifies types that themselves classify data, and Prop classifies propositions that themselves classify evidence of their truth. Just as Coe is checked when a type mismatch occurs, CoeSort is used when something other than a sort is provided in a context where a sort would be expected.

CoeSort 类型类和 Coe 大同小异，只是要求强制转换的目标一定要是一个 sort ，即 Type 或 Prop。词语 sort 指的是这些分类其他类型的类型——Type 分类那些本身分类数据的类型，而 Prop 分类那些本身分类其真实性证据的命题。正如在类型不匹配时会检查 Coe 一样，当在预期为 sort 的上下文中提供了其他东西时，会使用 CoeSort。

The coercion from a monoid into its carrier set extracts the carrier:

从一个幺半群到它的载体集的强制转换会返回该载体集：

1 2	instance : CoeSort Monoid Type where coe m := m.Carrier

With this coercion, the type signatures become less bureaucratic:

有了这个强制转换，类型签名变得不那么繁琐了：

def foldMap (M : Monoid) (f : α → M) (xs : List α) : M :=
  let rec go (soFar : M) : List α → M
    | [] => soFar
    | y :: ys => go (M.op soFar (f y)) ys
  go M.neutral xs

Another useful example of CoeSort is used to bridge the gap between Bool and Prop. As discussed in the section on ordering and equality, Lean’s if expression expects the condition to be a decidable proposition rather than a Bool. Programs typically need to be able to branch based on Boolean values, however. Rather than have two kinds of if expression, the Lean standard library defines a coercion from Bool to the proposition that the Bool in question is equal to true:

另一个有用的 CoeSort 使用场景是它可以让 Bool 和 Prop 建立联系。就像在有序性和等价性那一节我们提到的，Lean 的 if 表达式需要条件为一个可判定的命题而不是一个 Bool。然而，程序通常需要能够根据布尔值进行分支。 Lean 标准库并没有定义两种 if 表达式，而是定义了一种从 Bool 到命题的强制转换，即该 Bool 值等于 true：

1 2	instance : CoeSort Bool Prop where coe b := b = true

In this case, the sort in question is Prop rather than Type.

如此，这个 sort 将是一个 Prop 而不是 Bool。

Coercing to Functions

强制转换为函数（本节翻译需要润色）

Many datatypes that occur regularly in programming consist of a function along with some extra information about it. For example, a function might be accompanied by a name to show in logs or by some configuration data. Additionally, putting a type in a field of a structure, similarly to the Monoid example, can make sense in contexts where there is more than one way to implement an operation and more manual control is needed than type classes would allow. For example, the specific details of values emitted by a JSON serializer may be important because another application expects a particular format. Sometimes, the function itself may be derivable from just the configuration data.

许多在编程中常见的数据类型都会有一个函数和一些额外的信息组成。例如，一个函数可能附带一个名称以在日志中显示，或附带一些配置数据。此外，将一个类型放在结构体的字段中（类似于 Monoid 的例子）在某些上下文中是有意义的，这些上下文中存在多种实现操作的方法，并且需要比类型类允许的更手动的控制。例如，JSON 序列化器生成的值的具体细节可能很重要，因为另一个应用程序期望特定的格式。有时，仅从配置数据就可以推导出函数本身。

A type class called CoeFun can transform values from non-function types to function types. CoeFun has two parameters: the first is the type whose values should be transformed into functions, and the second is an output parameter that determines exactly which function type is being targeted.

CoeFun 类型类可以将非函数类型的值转换为函数类型的值。 CoeFun 有两个参数：第一个是需要被转变为函数的值的类型，第二个是一个输出参数，决定了到底应该转换为哪个函数类型。

1 2	class CoeFun (α : Type) (makeFunctionType : outParam (α → Type)) where coe : (x : α) → makeFunctionType x

The second parameter is itself a function that computes a type. In Lean, types are first-class and can be passed to functions or returned from them, just like anything else.

第二个参数本身是一个可以计算类型的函数。在 Lean 中，类型是一等公民，可以作为函数参数被传递，也可以作为返回值，就像其他东西一样。

For example, a function that adds a constant amount to its argument can be represented as a wrapper around the amount to add, rather than by defining an actual function:

例如，一个将常量加到其参数的函数可以表示为围绕要添加的量的包装，而不是通过定义一个实际的函数：

1 2	structure Adder where howMuch : Nat

A function that adds five to its argument has a 5 in the howMuch field:

一个为参数加上5的函数的 howMuch 字段为 5：

1	def add5 : Adder := ⟨5⟩

This Adder type is not a function, and applying it to an argument results in an error:

这个 Adder 类型并不是一个函数，将它应用到一个参数会报错：

#eval add5 3



function expected at
  add5
term has type
  Adder

Defining a CoeFun instance causes Lean to transform the adder into a function with type Nat → Nat:

定义一个 CoeFun 实例让 Lean 来将 adder 转换为一个 Nat → Nat 的函数：

instance : CoeFun Adder (fun _ => Nat → Nat) where
  coe a := (· + a.howMuch)

#eval add5 3



8

Because all Adders should be transformed into Nat → Nat functions, the argument to CoeFun’s second parameter was ignored.

因为所有的 Adder 都应该被转换为 Nat → Nat 的函数，CoeFun 的第二个参数就被省略了。

When the value itself is needed to determine the right function type, then CoeFun’s second parameter is no longer ignored. For example, given the following representation of JSON values:

当我们需要这个值来决定正确的函数类型时，CoeFun 的第二个参数就派上用场了。例如，给定下面的 JSON 值表示：

inductive JSON where
  | true : JSON
  | false : JSON
  | null : JSON
  | string : String → JSON
  | number : Float → JSON
  | object : List (String × JSON) → JSON
  | array : List JSON → JSON
deriving Repr

a JSON serializer is a structure that tracks the type it knows how to serialize along with the serialization code itself:

一个 JSON 序列化器是一个结构体，它不仅包含它知道如何序列化的类型，还包含序列化代码本身：

1
2
3

structure Serializer where
  Contents : Type
  serialize : Contents → JSON

A serializer for strings need only wrap the provided string in the JSON.string constructor:

对字符串的序列化器只需要将所给的字符串包装在 JSON.string 构造子中即可：

def Str : Serializer :=
  { Contents := String,
    serialize := JSON.string
  }

Viewing JSON serializers as functions that serialize their argument requires extracting the inner type of serializable data:

将 JSON 序列化器视为序列化其参数的函数需要提取可序列化数据的内部类型：

1 2	instance : CoeFun Serializer (fun s => s.Contents → JSON) where coe s := s.serialize

Given this instance, a serializer can be applied directly to an argument:

有了这个实例，一个序列化器就能直接应用在参数上。

def buildResponse (title : String) (R : Serializer) (record : R.Contents) : JSON :=
  JSON.object [
    ("title", JSON.string title),
    ("status", JSON.number 200),
    ("record", R record)
  ]

The serializer can be passed directly to buildResponse:

这个序列化器可以直接传入 buildResponse：

#eval buildResponse "Functional Programming in Lean" Str "Programming is fun!"



JSON.object
  [("title", JSON.string "Functional Programming in Lean"),
   ("status", JSON.number 200.000000),
   ("record", JSON.string "Programming is fun!")]

Aside: JSON as a String

附注：将 JSON 表示为字符串

It can be a bit difficult to understand JSON when encoded as Lean objects. To help make sure that the serialized response was what was expected, it can be convenient to write a simple converter from JSON to String. The first step is to simplify the display of numbers. JSON doesn’t distinguish between integers and floating point numbers, and the type Float is used to represent both. In Lean, Float.toString includes a number of trailing zeros:

当 JSON 被编码为 Lean 对象时可能有点难以理解。为了帮助保证序列化的响应是我们所期望的，写一个简单的从 JSON 到 String 的转换器可能会很方便。第一步是简化数字的显示。 JSON 不区分整数和浮点数，Float 类型即可用来代表二者。在 Lean 中，Float.toString 包括数字的后继零。

#eval (5 : Float).toString



"5.000000"

The solution is to write a little function that cleans up the presentation by dropping all trailing zeros, followed by a trailing decimal point:

解决方案是写一个小函数，这个函数可以清理掉所有的后继零，和后继的小数点：

def dropDecimals (numString : String) : String :=
  if numString.contains '.' then
    let noTrailingZeros := numString.dropRightWhile (· == '0')
    noTrailingZeros.dropRightWhile (· == '.')
  else numString

With this definition, #eval dropDecimals (5 : Float).toString yields "5", and #eval dropDecimals (5.2 : Float).toString yields "5.2".

有了这个定义，#eval dropDecimals (5 : Float).toString 结果为 "5"，#eval dropDecimals (5.2 : Float).toString 结果为 "5.2"。

The next step is to define a helper function to append a list of strings with a separator in between them:

下一步是定义一个辅助函数来连接字符串列表，并在中间添加分隔符：

def String.separate (sep : String) (strings : List String) : String :=
  match strings with
  | [] => ""
  | x :: xs => String.join (x :: xs.map (sep ++ ·))

This function is useful to account for comma-separated elements in JSON arrays and objects. #eval ", ".separate ["1", "2"] yields "1, 2", #eval ", ".separate ["1"] yields "1", and #eval ", ".separate [] yields "".

这个函数用于处理 JSON 数组和对象中的逗号分隔元素。 #eval ", ".separate ["1", "2"] 结果为 "1, 2"，#eval ", ".separate ["1"] 结果为 "1"，#eval ", ".separate [] 结果为 ""。

Finally, a string escaping procedure is needed for JSON strings, so that the Lean string containing "Hello!" can be output as "\"Hello!\"". Fortunately, the Lean compiler contains an internal function for escaping JSON strings already, called Lean.Json.escape. To access this function, add import Lean to the beginning of your file.

最后，需要一个字符串转义程序来处理 JSON 字符串，以便包含 “Hello!” 的 Lean 字符串可以输出为 "“Hello!””。幸运的是，Lean 编译器已经包含了一个用于转义 JSON 字符串的内部函数，叫做 Lean.Json.escape。要使用这个函数，可以在文件开头添加 import Lean。

The function that emits a string from a JSON value is declared partial because Lean cannot see that it terminates. This is because recursive calls to asString occur in functions that are being applied by List.map, and this pattern of recursion is complicated enough that Lean cannot see that the recursive calls are actually being performed on smaller values. In an application that just needs to produce JSON strings and doesn’t need to mathematically reason about the process, having the function be partial is not likely to cause problems.

将 JSON 值转换为字符串的函数被声明了 partial，因为 Lean 并不知道它是否停机。这是因为出现在函数中的 asString 的递归调用被应用到了 List.map，这种模式的递归已经复杂到 Lean 无法知道递归过程中值的规模是否是减小的。在一个只需要产生 JSON 字符串而不需要让过程在数学上是合理的的应用中，让函数是 partial 的不太可能造成麻烦。

partial def JSON.asString (val : JSON) : String :=
  match val with
  | true => "true"
  | false => "false"
  | null => "null"
  | string s => "\"" ++ Lean.Json.escape s ++ "\""
  | number n => dropDecimals n.toString
  | object members =>
    let memberToString mem :=
      "\"" ++ Lean.Json.escape mem.fst ++ "\": " ++ asString mem.snd
    "{" ++ ", ".separate (members.map memberToString) ++ "}"
  | array elements =>
    "[" ++ ", ".separate (elements.map asString) ++ "]"

With this definition, the output of serialization is easier to read:

有了这个定义，序列化的结果更加易读了：

#eval (buildResponse "Functional Programming in Lean" Str "Programming is fun!").asString



"{\\"title\\": \\"Functional Programming in Lean\\", \\"status\\": 200, \\"record\\": \\"Programming is fun!\\"}"

Messages You May Meet

可能会遇到的问题

Natural number literals are overloaded with the OfNat type class. Because coercions fire in cases where types don’t match, rather than in cases of missing instances, a missing OfNat instance for a type does not cause a coercion from Nat to be applied:

自然数字面量是通过 OfNat 类型类重载的。因为在类型不匹配时才会触发强制转换，而不是在找不到实例时，所以当对于某类型的 OfNat 实例缺失时，并不会触发强制转换：

def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
  392

1 2	failed to synthesize instance OfNat (Option (Option (Option Nat))) 392

Design Considerations

设计原则

Coercions are a powerful tool that should be used responsibly. On the one hand, they can allow an API to naturally follow the everyday rules of the domain being modeled. This can be the difference between a bureaucratic mess of manual conversion functions and a clear program. As Abelson and Sussman wrote in the preface to Structure and Interpretation of Computer Programs (MIT Press, 1996),

强制转换是一个强大的工具，请负责任地使用它。一方面，它可以使 API 设计得更贴近领域内使用习惯。这是繁琐的手动转换函数和一个清晰的程序间的差别。正如 Abelson 和 Sussman 在《计算机程序的构造和解释》（ Structure and Interpretation of Computer Programs ）（麻省理工学院出版社，1996年）前言中所写的那样：

Programs must be written for people to read, and only incidentally for machines to execute.

写程序须以让人读明白为主，让计算机执行为辅。

Coercions, used wisely, are a valuable means of achieving readable code that can serve as the basis for communication with domain experts. APIs that rely heavily on coercions have a number of important limitations, however. Think carefully about these limitations before using coercions in your own libraries.

明智地使用强制转换，可以使得代码更加易读——这是与领域内专家的交流的基础。然而，严重依赖强制转换的 API 会有许多限制。在你自己的代码中使用强制转换前，认真思考这些限制。

First off, coercions are only applied in contexts where enough type information is available for Lean to know all of the types involved, because there are no output parameters in the coercion type classes. This means that a return type annotation on a function can be the difference between a type error and a successfully applied coercion. For example, the coercion from non-empty lists to lists makes the following program work:

首先，强制转换只应该出现在类型信息充足，Lean 能够知道所有参与的类型的语境中。因为强制转换类型类中并没有输出参数这么一说。这意味着在函数上添加返回类型注释可以决定是类型错误还是成功应用强制转换。例如，从非空列表到列表的强制转换使以下程序得以运行：

1 2	def lastSpider : Option String := List.getLast? idahoSpiders

On the other hand, if the type annotation is omitted, then the result type is unknown, so Lean is unable to find the coercion:

另一方面，如果类型注释被省略了，那么结果的类型就是未知的，那么 Lean 就无法找到对应的强制转换。

def lastSpider :=
  List.getLast? idahoSpiders



application type mismatch
  List.getLast? idahoSpiders
argument
  idahoSpiders
has type
  NonEmptyList String : Type
but is expected to have type
  List ?m.34258 : Type

More generally, when a coercion is not applied for some reason, the user receives the original type error, which can make it difficult to debug chains of coercions.

通常来讲，如果一个强制转换因为一些原因失败了，用户会收到原始的类型错误，这会使在强制转换链上定位错误变得十分困难。

Finally, coercions are not applied in the context of field accessor notation. This means that there is still an important difference between expressions that need to be coerced and those that don’t, and this difference is visible to users of your API.

最后，强制转换不会在字段访问符号的上下文中应用。这意味着需要强制转换的表达式与不需要强制转换的表达式之间仍然存在重要区别，而这个区别对用户来说是肉眼可见的。

Additional Conveniences

其他便利功能

Constructor Syntax for Instances

实例的构造子语法

Behind the scenes, type classes are structure types and instances are values of these types. The only differences are that Lean stores additional information about type classes, such as which parameters are output parameters, and that instances are registered for searching. While values that have structure types are typically defined using either ⟨...⟩ syntax or with braces and fields, and instances are typically defined using where, both syntaxes work for both kinds of definition.

在幕后，类型类都是一些结构体类型，实例都是那些类型的值。唯一的区别是 Lean 存储关于类型类的额外信息，例如哪些参数是输出参数，和记录要被搜索的实例。虽然结构体类型的值通常要么是用 ⟨...⟩ 定义的，要么是用大括号和字段定义的，而实例通常使用where定义，但这两种语法都适用于这两种定义方式。

For example, a forestry application might represent trees as follows:

例如，一个林业应用程序可能会这样表示树木：

structure Tree : Type where
  latinName : String
  commonNames : List String

def oak : Tree :=
  ⟨"Quercus robur", ["common oak", "European oak"]⟩

def birch : Tree :=
  { latinName := "Betula pendula",
    commonNames := ["silver birch", "warty birch"]
  }

def sloe : Tree where
  latinName := "Prunus spinosa"
  commonNames := ["sloe", "blackthorn"]

All three syntaxes are equivalent.

这些语法都是等价的

Similarly, type class instances can be defined using all three syntaxes:

类似地，这三种语法也可以用于定义类型类的实例。

class Display (α : Type) where
  displayName : α → String

instance : Display Tree :=
  ⟨Tree.latinName⟩

instance : Display Tree :=
  { displayName := Tree.latinName }

instance : Display Tree where
  displayName t := t.latinName

Generally speaking, the where syntax should be used for instances, and the curly-brace syntax should be used for structures. The ⟨...⟩ syntax can be useful when emphasizing that a structure type is very much like a tuple in which the fields happen to be named, but the names are not important at the moment. However, there are situations where it can make sense to use other alternatives. In particular, a library might provide a function that constructs an instance value. Placing a call to this function after := in an instance declaration is the easiest way to use such a function.

一般来说，where 语法应该用于实例，单书名号应该用于结构体。当强调一个结构类型非常类似于一个字段被命名的元组，但名字此刻并不重要时，⟨...⟩ 语法会很有用。然而，有些情况用其他方式可能才是合理的。具体而言，一个库可能提供一个构建实例值的函数。在实例声明中的 := 之后调用这个函数是使用此类函数的最简单方法。

Examples

例子

When experimenting with Lean code, definitions can be more convenient to use than #eval or #check commands. First off, definitions don’t produce any output, which can help keep the reader’s focus on the most interesting output. Secondly, it’s easiest to write most Lean programs by starting with a type signature, allowing Lean to provide more assistance and better error messages while writing the program itself. On the other hand, #eval and #check are easiest to use in contexts where Lean is able to determine the type from the provided expression. Thirdly, #eval cannot be used with expressions whose types don’t have ToString or Repr instances, such as functions. Finally, multi-step do blocks, let-expressions, and other syntactic forms that take multiple lines are particularly difficult to write with a type annotation in #eval or #check, simply because the required parenthesization can be difficult to predict.

当用 Lean 代码做实验时，定义可能比 #eval 或 #check 指令更方便。首先，定义不会产生任何输出，这可以让读者的注意力集中在最有趣的输出上。第二，从一个类型签名开始一个 Lean 程序是最简单的方式，这也会使 Lean 能够提供更多的协助和更好的错误信息。另一方面，#eval 和 #check 在 Lean 可以通过表达式给出类型时用起来最简单。第三，#eval 并不能用于没有 ToString 或 Repr 实例的类型，例如函数。最后，多步的 do 语法块，let 表达式，和其他多行语法形式在 #eval 或 #check 中有时候是一个需要多层括号区分优先级的长表达式，在这里面插入类型标注会很难读。

To work around these issues, Lean supports the explicit indication of examples in a source file. An example is like a definition without a name. For instance, a non-empty list of birds commonly found in Copenhagen’s green spaces can be written:

为了绕开这些问题，Lean 支持源码中例子的显式类型推断。一个例子就是一个无名的定义。例如，一个在 Copenhagen’s green spaces 中常见鸟类的非空列表可以写成这样：

example : NonEmptyList String :=
  { head := "Sparrow",
    tail := ["Duck", "Swan", "Magpie", "Eurasian coot", "Crow"]
  }

Examples may define functions by accepting arguments:

接受参数的例子可以用来定义函数：

1 2	example (n : Nat) (k : Nat) : Bool := n + k == k + n

While this creates a function behind the scenes, this function has no name and cannot be called. Nonetheless, this is useful for demonstrating how a library can be used with arbitrary or unknown values of some given type. In source files, example declarations are best paired with comments that explain how the example illustrates the concepts of the library.

这会在幕后创建一个函数，这个函数没有名字，也不能被调用。此外，这可以用来检查某库中的函数是否可以在任意的或一些类型的未知值上正常工作。在源码中，example 声明很适合与解释概念的注释搭配使用。

Summary

总结

Type Classes and Overloading

类型类和重载

Type classes are Lean’s mechanism for overloading functions and operators. A polymorphic function can be used with multiple types, but it behaves in the same manner no matter which type it is used with. For example, a polymorphic function that appends two lists can be used no matter the type of the entries in the list, but it is unable to have different behavior depending on which particular type is found. An operation that is overloaded with type classes, on the other hand, can also be used with multiple types. However, each type requires its own implementation of the overloaded operation. This means that the behavior can vary based on which type is provided.

类型类是 Lean 重载函数和运算符的机制。一个多态函数可以用于多种类型，但是不管是什么类型，它的行为都是一致的。例如，一个连接两个列表的多态函数在使用时不关心列表中元素的类型，但它也不可能根据具体的元素类型有不一样的行为。另一方面，一个用类型类重载的运算符，也可以用在多种类型上。然而，每个类型都需要自己的重载运算实现。这意味着可以根据不同的类型有不同的行为。

A type class has a name, parameters, and a body that consists of a number of names with types. The name is a way to refer to the overloaded operations, the parameters determine which aspects of the definitions can be overloaded, and the body provides the names and type signatures of the overloadable operations. Each overloadable operation is called a method of the type class. Type classes may provide default implementations of some methods in terms of the others, freeing implementors from defining each overload by hand when it is not needed.

一个 类型类 有名称，参数，和一个包含了名称和类型的类体。名字是一种代指重载运算符的方式，参数决定了哪些方面的定义可以被重载，类体提供了可重载运算的名称和类型签名。每一个可重载运算都被称为类型类的一个方法。类型类可能会提供一些方法的默认实现，使得程序员从手动实现每个重载（只要实现可以被自动完成）中解放出来。

An instance of a type class provides implementations of the methods for given parameters. Instances may be polymorphic, in which case they can work for a variety of parameters, and they may optionally provide more specific implementations of default methods in cases where a more efficient version exists for some particular type.

一个类型类的实例为给定参数提供了方法的实现。实例可能是多态的，这种情况下它能接受多种参数，同时也可能在对于一些类型存在更高效的实现时提供更具体实现。

Type class parameters are either input parameters (the default), or output parameters (indicated by an outParam modifier). Lean will not begin searching for an instance until all input parameters are no longer metavariables, while output parameters may be solved while searching for instances. Parameters to a type class need not be types—they may also be ordinary values. The OfNat type class, used to overload natural number literals, takes the overloaded Nat itself as a parameter, which allows instances to restrict the allowed numbers.

类型类参数要么是一个 输入参数（input parameters） （默认情况下），或者是一个 输出参数 （通过 outParam 修饰）。在所有输出参数变为已知前，Lean 不会开始实例搜索。输出参数会在实例搜索过程中给出。类型类的参数不一定要是一个类型，它也可以是一个常规值。 OfNat 类型类被用于重载自然数字面量，接受要被重载的 Nat 本身作为参数，这可以使实例限制允许的数字。

Instances may be marked with a @[default_instance] attribute. When an instance is a default instance, then it will be chosen as a fallback when Lean would otherwise fail to find an instance due to the presence of metavariables in the type.

实例可能会被标注为 @[default_instance] 属性。当一个实例是默认实例时，那么就会作为 Lean 因存在元变量而无法找到实例的回退。

Type Classes for Common Syntax

常见语法的类型类

Most infix operators in Lean are overridden with a type class. For instance, the addition operator corresponds to a type class called Add. Most of these operators have a corresponding heterogeneous version, in which the two arguments need not have the same type. These heterogenous operators are overloaded using a version of the class whose name starts with H, such as HAdd.

Lean 中多数中缀运算符都是用类型类来重载的。例如，加法对应于 Add 类型类。多数运算符都有与之对应的异质运算，该运算的两个参数不需要是同一种类型。这些异质运算符使用前面加个 H 的类型类来重载，比如 HAdd。

Indexing syntax is overloaded using a type class called GetElem, which involves proofs. GetElem has two output parameters, which are the type of elements to be extracted from the collection and a function that can be used to determine what counts as evidence that the index value is in bounds for the collection. This evidence is described by a proposition, and Lean attempts to prove this proposition when array indexing is used. When Lean is unable to check that list or array access operations are in bounds at compile time, the check can be deferred to run time by appending a ? to the indexing operation.

索引语法使用 GetElem 类型类来重载，该类型类包含证明。 GetElem 有两个输出参数，一个是要被从中提取出的元素的类型，另一个是用来证明索引值未越界的函数。这个证明是用命题来描述的，Lean 会在索引时尝试证明这个命题。当 Lean 在编译时不能检查列表或元组索引是否越界时，可以通过为索引操作添加 ? 来让检查发生在运行时。

Functors

函子

A functor is a polymorphic type that supports a mapping operation. This mapping operation transforms all elements “in place”, changing no other structure. For instance, lists are functors and the mapping operation may neither drop, duplicate, nor mix up entries in the list.

一个函子是一个支持映射运算的泛型。这个映射运算“在原地”映射所有的元素，不会改变其他结构。例如，列表是函子，所以列表上的映射不会删除，复制或混合列表中的元素。

While functors are defined by having map, the Functor type class in Lean contains an additional default method that is responsible for mapping the constant function over a value, replacing all values whose type are given by polymorphic type variable with the same new value. For some functors, this can be done more efficiently than traversing the entire structure.

如果定义了 map，那么这个类型就是一个函子。 Lean 中的 Functor 类型类还包含了额外的默认方法，这些方法可以将映射常数函数到值，替换所有类型是由多态变量给出的值为一个相同的新值。对于一些函子，这比转换整个结构更高效。

Deriving Instances

派生实例

Many type classes have very standard implementations. For instance, the Boolean equality class BEq is usually implemented by first checking whether both arguments are built with the same constructor, and then checking whether all their arguments are equal. Instances for these classes can be created automatically.

许多类型类都有非常标准的实现。例如，布尔等价类型类 BEq 经常被实现为先检查参数是否有一样的构造子，然后检查他们的值是否相等。这些类型类的实例可以自动创建。

When defining an inductive type or a structure, a deriving clause at the end of the declaration will cause instances to be created automatically. Additionally, the deriving instance ... for ... command can be used outside of the definition of a datatype to cause an instance to be generated. Because each class for which instances can be derived requires special handling, not all classes are derivable.

当定义一个归纳类型或者结构体时，出现在声明末尾的 deriving 会让实例自动创建。此外，deriving instance ... for ... 指令可以在数据类型定义外使用来生成一个实例。因为每个可以派生实例的类都需要特殊处理，所以并不是所有的类都是可派生的。

Coercions

强制转换

Coercions allow Lean to recover from what would normally be a compile-time error by inserting a call to a function that transforms data from one type to another. For example, the coercion from any type α to the type Option α allows values to be written directly, rather than with the some constructor, making Option work more like nullable types from object-oriented languages.

强制转换允许 Lean 向一个正常来说应该出现编译错误的地方插入一个函数调用，该调用将转换数据的类型，从而从错误中恢复。例如，一个从任意类型 α 到 Option α 的强制转换使得值可以直接写出，而不是被包裹在 some 构造子中。这样 Option 就像是有空值类型的语言中的空值那样。

There are multiple kinds of coercion. They can recover from different kinds of errors, and they are represented by their own type classes. The Coe class is used to recover from type errors. When Lean has an expression of type α in a context that expects something with type β, Lean first attempts to string together a chain of coercions that can transform αs into βs, and only displays the error when this cannot be done. The CoeDep class takes the specific value being coerced as an extra parameter, allowing either further type class search to be done on the value or allowing constructors to be used in the instance to limit the scope of the conversion. The CoeFun class intercepts what would otherwise be a “not a function” error when compiling a function application, and allows the value in the function position to be transformed into an actual function if possible.

有许多不同的强制转换。他们可以从不同的错误类型中恢复，他们都是用自己的类型类来描述的。 Coe 类型类用于从类型错误中恢复。当 Lean 有一个 α 类型的表达式，但却希望这里是一个 β 类型时，Lean 会首先尝试串起一个能将 α 强制转换为 β 的链，仅当它无法这么做的时候才会报错。 CoeDep 类将被强制转换的具体值作为额外参数，这样可以对该值进行进一步的类型类搜索，或者在实例中使用构造函数来限制转换的范围。 CoeFun 类在编译函数应用时会拦截“不是函数”的错误，并允许将函数位置的值转换为实际函数（如果可能的话）。

重载与类型类

正整数

自定义类型

类与实例

重载加法

转换为字符串

重载乘法

数字字面量

练习

类型类与多态

对多态函数的类型检查

定义含隐式实例的多态函数

方法与隐式参数

练习

控制实例搜索

异质重载

输出参数

默认实例

练习

数组与索引

数组

非空列表

Overloading Indexing

重载索引

Standard Classes

标准类

Arithmetic

算术符号

Bitwise Operators

位运算符

Equality and Ordering

相等性与有序性

Hashing

哈希

Deriving Standard Classes

派生标准类

Appending

Functors

函子

Messages You May Meet

你也许会遇到的问题

Exercises

练习

Coercions

强制转换

Positive Numbers

正数

Chaining Coercions

链式强制转换

Non-Empty Lists and Dependent Coercions

非空列表与依值强制转换

Coercing to Types

强制转换为类型（ 本节中 sort 的翻译待讨论 ）

Coercing to Functions

强制转换为函数 （ 本节翻译需要润色 ）

Aside: JSON as a String

附注：将 JSON 表示为字符串

Messages You May Meet

可能会遇到的问题

Design Considerations

设计原则

Additional Conveniences

其他便利功能

Constructor Syntax for Instances

实例的构造子语法

Examples

例子

Summary

总结

Type Classes and Overloading

类型类和重载

Type Classes for Common Syntax

常见语法的类型类

Functors

函子

Deriving Instances

派生实例

Coercions

强制转换

强制转换为类型（本节中 sort 的翻译待讨论）

强制转换为函数（本节翻译需要润色）