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

发表于 更新于 阅读次数： 字数： 21k 时间 ≈ 1:17

重载与类型类

在许多语言中，内置数据类型有特殊的优待。 例如，在 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)))))

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

1
2
3
4
def fourteen : Pos := seven + seven

failed to synthesize instance
  HAdd Pos Pos ?m.291
1
2
3
4
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 命令中的括号表示只有指定的名称才能从命名空间中访问：

1
2
3
4
5
open Plus (plus)

#eval plus 5 3

8

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

1
2
3
4
5
6
7
8
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 相加两个浮点数会失败，并显示熟悉的错误消息：

1
2
3
4
#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 值使用普通的加法语法：

1
2
3
4
5
6
7
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。

1
2
3
4
5
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 重载）是生成更简短输出的快速方法：

1
2
3
4
5
6
7
8
9
10
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 实例就足够了。

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

1
2
3
4
5
6
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

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

1
2
3
4
5
#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 并不阻止非类型参数出现在类型类的参数位置上，但一些不够灵活的语言则不允许这种操作。这种灵活性能为特定的值以及特定的类型提供运算符重载。

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

1
2
3
4
5
6
inductive LT4 where
  | zero
  | one
  | two
  | three
deriving Repr

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

1
2
3
4
5
6
7
8
9
10
11
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

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

1
2
3
4
5
#eval (3 : LT4)
LT4.three

#eval (0 : LT4)
LT4.zero

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

1
2
3
4
#eval (4 : LT4)

failed to synthesize instance
OfNat LT4 4

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

1
2
3
4
5
6
7
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

练习

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

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

解答：

1
2
3
4
5
6
7
8
9
10
11
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
  1. 定义一个只表示偶数的数据类型。定义 Add、Mul 和 ToString 的实例，使其能够方便地使用。OfNat 需要下一节中介绍的特性。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
-- 定义偶数数据类型
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
  1. 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 实例。

1
2
3
4
5
6
-- 为具体类型直接定义实例
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 列表：

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

#eval fourNats.sum

10

由于 Pos 在 0 处没有定义， [OfNat α 0] 匹配失败，无法用于 Pos 列表：

1
2
3
4
5
6
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 作为自动隐式参数，实例本身也可能接受隐式实例参数。 在 多态那一节 中展示了一个多态点类型：

1
2
3
4
structure PPoint (α : Type) where
  x : α
  y : α
deriving Repr

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

1
2
3
-- α 为 Add 实例时，PPoint α 也有 Add 实例
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 实例的引用。

举个例子：

1
2
3
4
-- 假设我们有：
def point1 : PPoint Nat := { x := 1, y := 2 }
def point2 : PPoint Nat := { x := 3, y := 4 }
def result := point1 + point2  -- 这里发生了什么？

当 Lean 执行 point1 + point2 时：

  1. 寻找实例：需要 Add (PPoint Nat) 实例
  2. 找到条件实例：instance [Add α] : Add (PPoint α)
  3. 递归搜索：需要 Add Nat 实例
  4. 构造实例值：创建一个包含引用的结构体

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

方法与隐式参数

1
2
3
4
5
6
7
8
9
10
11
class OfNat (α : Type u) (_ : Nat) where
  ofNat : α

#check OfNat.ofNat
-- {α : Type} → (n : Nat) → [OfNat α n] → α

class Add (α : Type u) where
  add : α → α → α

#check Add.add
-- {α : Type u} [self : Add α] : α → α → α

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

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

这类似于声明新结构也声明访问器函数的方式。主要区别在于结构体的访问器函数（比如 PPoint.mk ）将结构值作为显式参数，而类型类方法将实例值作为隐式实例（比如 [Add α] ），由 Lean 自动查找。

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

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

题外话：在表达类型时，中间参数允许用非类型的 (n : Nat)，但不能放在最后

1
2
3
4
5
6
7
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)

练习

  1. 偶数数字字面量为 上一节的练习题 中的偶数数据类型写一个使用递归实例搜索的 OfNat 实例。
1
2
3
4
5
6
7
8
9
10
-- 基本的 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)
  1. 递归实例搜索深度：Lean 编译器尝试进行递归实例搜素的次数是有限的。这限制了前面的练习中定义的偶数字面量的尺寸。实验性地确定这个上限是多少。

实测为 256：

1
#check (256 : Even)

Lean 在寻找 OfNat Even 256 实例时，会递归地寻找 OfNat Even 254 实例，以此类推，直到找到 OfNat Even 0 实例。

控制实例搜索

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

1
2
3
4
5
6
7
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 的实例可以让常规加法符号可以接受不同类型。

1
2
3
4
5
instance : HAdd Nat Pos Pos where
  hAdd := addNatPos

instance : HAdd Pos Nat Pos where
  hAdd := addPosNat

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

1
2
3
4
5
#eval (3 : Pos) + (5 : Nat)
8

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

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

1
2
3
4
5
6
7
8
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 使用这些实例时，一个错误就出现了：

1
2
3
4
#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 手册。

自然数 Nat 是 OfNat 的默认实例，源码可以看到：

1
2
3
@[default_instance 100] /- low prio -/
instance instOfNatNat (n : Nat) : OfNat Nat n where
  ofNat := n

练习

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

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

结果应为

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

数组与索引

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

回顾目前为止，我们学到的一些缩写记号包括：

  • {} 用于构造结构体：{a:= .., b:= .., c:= ...}，结合 with 来构造结构体 `{p with a := …}
  • ⟨⟩ 用于按顺序构造结构体：⟨a, b, c⟩ 是一个结构体
  • [] 用于构造列表 List，用 x :: xs 表达列表的拼接

数组

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] 的结果为：

1
2
3
4
5
6
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" 和四种其它蜘蛛构成，一共有五种蜘蛛：

1
2
3
4
5
6
7
8
9
def idahoSpiders : NonEmptyList String := {
  head := "Banded Garden Spider",
  tail := [
    "Long-legged Sac Spider",
    "Wolf Spider",
    "Hobo Spider",
    "Cat-faced Spider"
  ]
}

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

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

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

1
2
3
4
5
6
def NonEmptyList.get? : NonEmptyList α → Nat → Option α
  | xs, 0 => some xs.head
  -- 如果 tail 空白，且越界
  | {head := _, tail := []}, _ + 1 => none
  -- 如果 tail 非空，递归
  | {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

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

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

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

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

1
2
3
theorem atLeastThreeSpiders : idahoSpiders.inBounds 2 := by simp

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

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

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

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

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

重载索引

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

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

元素类型和证明函数都是输出参数。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

在 NonEmptyList α 中，这些参数是：

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

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

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

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

1
2
3
4
5
6
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

因为列表的类型和索引的类型都是 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]

使用非数字索引值来进行索引也可以是合理的。例如：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

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

标准类

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

算术符号

多数算术运算符都是可以进行异质运算的。这意味着参数可能有不同的类型，并且输出参数决定了结果表达式的类型。对于每个异质运算符，都有一个同质运算符与其对应。只要把字母 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

位运算符

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

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

相等性与有序性

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

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

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

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

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

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

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

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

1
2
3
#check 2 < 4

2 < 4 : Prop

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

并不是所有的命题都是可判定的。如果所有的命题都是可判定的，那么计算机通过运行判定程序就可以证明任何的真命题，数学家们就此失业了。更具体来说，可判定的命题都会有一个 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)

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

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

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

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

1
2
3
4
inductive Ordering where
| lt
| eq
| gt

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

1
2
3
4
5
6
7
8
9
10
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

#eval Ord.compare 1 2 == Ordering.lt -- true

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

哈希

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

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

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

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

1
2
3
4
5
6
def hashPos : Pos → UInt64
  | Pos.one => 0
  | Pos.succ n => mixHash 1 (hashPos n)

instance : Hashable Pos where
  hash := hashPos

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

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

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

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
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
  -- 叶子节点的哈希值为 0
  | BinTree.leaf =>
    0
  -- 分支节点的哈希值：混合常数1、左子树哈希、节点值哈希、右子树哈希
  | BinTree.branch left x right =>
    mixHash 1 (mixHash (hashBinTree left) (mixHash (hash x) (hashBinTree right)))

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

派生标准类

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

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

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

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

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

  • Inhabited
  • BEq
  • Repr
  • Hashable
  • Ord

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

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

连接符

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

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

语法 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 }

在定义了上面的实例后，

1
#eval idahoSpiders ++ idahoSpiders

就有了下面的结果：

1
2
3
4
5
6
7
8
9
10
{ 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"] }

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

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

有了这个实例后，

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

结果为

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

函子

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

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

  • Functor.map (· + 5) [1, 2, 3] 结果为 [6, 7, 8]
  • Functor.map toString (some (List.cons 5 List.nil)) 结果为 some "[5]"，打开了 Option 类型，而非 List
  • Functor.map List.reverse [[1, 2, 3], [4, 5, 6]] 结果为 [[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]]

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

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

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

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

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

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

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

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

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

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

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

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

1
2
3
4
5
class Functor (f : Type → Type) where
  map : {α β : Type} → (α → β) → f α → f β

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

可以使用默认实现：

1
2
3
4
5
6
7
8
-- 使用默认的 mapConst
[1, 2, 3, 4].mapConst "hello"
===>
Functor.mapConst "hello" [1, 2, 3, 4]
===>
Functor.map (fun _ => "hello") [1, 2, 3, 4]
===>
["hello", "hello", "hello", "hello"]

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

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

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

你也许会遇到的问题

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

1
deriving instance ToString for NonEmptyList

会导致如下错误：

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

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

练习

  • 写一个 HAppend (List α) (NonEmptyList α) (NonEmptyList α) 的实例并测试它
  • 为二叉树实现一个 Functor 的实例。

强制转换

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

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

正数

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

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

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

1
2
3
4
5
6
7
8
9
10
[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

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

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

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

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

1
2
3
4
5
6
instance : Coe Pos Nat where
  coe x := x.toNat

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

[3, 4]

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

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

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

链式强制转换

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

1
def oneInt : Int := Pos.one

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

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

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
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 := ()

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

1
#eval coercedToB

结果为：

1
B.b

整个过程，() 先被强制转换为 Unit A，然后再被强制转换为 B。

1
2
3
4
5
(() : B)
===>
(() : Unit A)
===>
((() : Unit A) : B)

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

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

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

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

#eval perhapsPerhapsPerhaps

-- some (some "Please don't tell me")

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

1
2
def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
  392
1
2
failed to synthesize instance
  OfNat (Option (Option (Option Nat))) 392

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

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

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

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

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

非空列表与依值强制转换

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

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

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

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

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

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

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

强制转换为类型

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

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
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 }

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

1
2
3
4
5
6
7
8
9
10
-- M 是一个的幺半群，f 映射到 M 的群元素，xs 是一个 α 列表
-- 记 op 为乘法，结果为 1 * f(x1) * f(x2) * ... * f(xn)
def foldMap (M : Monoid) (f : α → M.Carrier) (xs : List α) : M.Carrier :=
  let rec go (soFar : M.Carrier) : List α → M.Carrier
    -- 递归终点
    | [] => soFar
    -- 通过 M.op 吞掉头部元素（左乘 soFar）
    | y :: ys => go (M.op soFar (f y)) ys
  -- 从单位元开始作用
  go M.neutral xs

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

在 Lean 中，Sort 是一个特殊概念，指的是用来分类其他类型的"元类型"：

  • Type：分类那些用来描述数据的类型
    • 例如：Nat、String、List Nat 都是 Type
    • 这些类型的值是具体的数据：42 : Nat、"hello" : String
  • Prop：分类那些用来描述命题的类型
    • 例如：2 + 2 = 4、∀ n : Nat, n + 0 = n 都是 Prop
    • 这些类型的值是证明：2 + 2 = 4 的证明

CoeSort 类型类和 Coe 大同小异，只是要求强制转换的目标一定要是一个 sort ，即 Type 或 Prop。

正如在类型不匹配时会检查 Coe 一样，当在预期为 sort 的上下文中提供了其他东西时，会使用 CoeSort。

比如，当 Lean 期望一个 类型，但你提供了一个 值 时， CoeSort 会被触发

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

这意味着：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
-- 定义一个具体的幺半群
def NatAddMonoid : Monoid := {
  Carrier := Nat,
  neutral := 0,
  op := (· + ·),
}

-- 现在可以直接使用 NatAddMonoid 作为类型！
def example_value : NatAddMonoid := (42 : Nat)
-- 如果用 Coe，此时需要显式地写出转化
-- def example_value : (NatAddMonoid : Type) := (42 : Nat)

-- 等价于
def example_value' : NatAddMonoid.Carrier := (42 : Nat)

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

1
2
3
4
5
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

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

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

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

因此，这个定义语句是合法的：

1
def a : true := by rfl

强制转换为函数

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

CoeFun 类型类能够将非函数类型的值转换为函数类型的值。CoeFun 接受两个参数：第一个是待转换为函数的值的类型，第二个是输出参数，用于确定应转换为哪种具体的函数类型。

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

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

例如，一个给参数加上常量的函数可以表示为对待加数值的包装，而无需定义实际的函数：

1
2
structure Adder where
  howMuch : Nat

一个给参数加 5 的函数，其 howMuch 字段为 5：

1
def add5 : Adder := ⟨5⟩

Adder 类型本身并非函数，直接将其应用于参数会产生错误：

1
2
3
4
5
6
#eval add5 3

function expected at
  add5
term has type
  Adder

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

1
2
3
4
5
6
instance : CoeFun Adder (fun _ => Nat → Nat) where
  coe a := (· + a.howMuch)

#eval add5 3

8

由于所有 Adder 都应转换为 Nat → Nat 函数，CoeFun 的第二个参数被忽略了（使用 fun _ =>）。

当需要根据值来确定正确的函数类型时，CoeFun 的第二个参数就发挥作用了。例如，给定以下 JSON 值表示：

1
2
3
4
5
6
7
8
9
10
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

JSON 序列化器是一个结构体，它需要包含如何序列化的类型，以及序列化的代码本身：

1
2
3
structure Serializer where
  Contents : Type
  serialize : Contents → JSON

字符串序列化器只需将给定字符串包装在 JSON.string 构造子中：

1
2
3
4
def Str : Serializer :=
  { Contents := String,
    serialize := JSON.string
  }

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

1
2
3
-- 把 Serializer 转化成函数，通过内部的 Contents 函数，来序列化对象
instance : CoeFun Serializer (fun s => s.Contents → JSON) where
  coe s := s.serialize

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

1
2
3
4
5
6
def buildResponse (title : String) (R : Serializer) (record : R.Contents) : JSON :=
  JSON.object [
    ("title", JSON.string title),
    ("status", JSON.number 200),
    ("record", R record)
  ]

序列化器可以直接传递给 buildResponse：

1
2
3
4
5
6
#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!")]

这里虽然 Str "hello" 的效果看起来和 JSON.string "hello" 等价，但前者用 Serializer 统一了这类函数接口，使得其他定义类型的转化器也可以用 buildResponse 函数。

附注：将 JSON 表示为字符串

当 JSON 被编码为 Lean 对象时可能有点难以理解。为了确保序列化的响应符合预期，编写一个简单的从 JSON 到 String 的转换器会很方便。第一步是简化数字的显示。JSON 不区分整数和浮点数，Float 类型可以表示两者。在 Lean 中，Float.toString 包含尾随零。

1
2
3
#eval (5 : Float).toString

"5.000000"

解决方案是编写一个小函数来清理所有尾随零和尾随小数点：

1
2
3
4
5
def dropDecimals (numString : String) : String :=
  if numString.contains '.' then
    let noTrailingZeros := numString.dropRightWhile (· == '0')
    noTrailingZeros.dropRightWhile (· == '.')
  else numString

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

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

1
2
3
def String.separate (sep : String) : List String -> String
  | [] => ""
  | x :: xs => String.join (x :: xs.map (sep ++ ·))

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

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

将 JSON 值转换为字符串的函数被声明为 partial，因为 Lean 无法确定它是否终止。这是因为函数中 asString 的递归调用被应用于 List.map，这种递归模式过于复杂，Lean 无法确定递归过程中值的规模是否在减小。在只需要生成 JSON 字符串而不需要数学推理的应用中，函数为 partial 不太可能造成问题。

1
2
3
4
5
6
7
8
9
10
11
12
13
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) ++ "]"

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

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

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

如果不加 partial，这里会报错：

1
2
3
4
5
6
7
failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
a✝ : List JSON
val : JSON
⊢ sizeOf val < 1 + sizeOf a✝

可能会遇到的问题

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

1
2
def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
  392
1
2
failed to synthesize instance
  OfNat (Option (Option (Option Nat))) 392

设计原则

强制转换是一个强大的工具，应当负责任地使用。一方面，它可以使 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.

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

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

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

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

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

1
2
3
4
5
6
7
8
9
10
11
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

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

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

其他便利功能

实例的构造子语法

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

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

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
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"]

这些语法都是等价的

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

1
2
3
4
5
6
7
8
9
10
11
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

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

例子

在使用 Lean 代码进行实验时，定义往往比 #eval 或 #check 指令更加便利。首先，定义不会产生任何输出，这有助于让读者将注意力集中在最重要的输出上。其次，从类型签名开始编写 Lean 程序是最简单的方式，这样 Lean 能够提供更多帮助和更好的错误信息。相比之下，#eval 和 #check 在 Lean 能够从表达式推断出类型时使用起来最为简单。第三，#eval 无法用于那些类型没有 ToString 或 Repr 实例的表达式，比如函数。最后，多步骤的 do 语法块、let 表达式以及其他多行语法形式在 #eval 或 #check 中往往需要复杂的括号来区分优先级，在这种情况下插入类型标注会使代码变得难以阅读。

为了解决这些问题，Lean 支持在源码中显式指定示例。示例就像是一个没有名称的定义。例如，一个包含哥本哈根绿地中常见鸟类的非空列表可以这样写：

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

示例也可以通过接受参数来定义函数：

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

虽然这会在幕后创建一个函数，但这个函数没有名称，无法被调用。不过，这对于演示如何在给定类型的任意值或未知值上使用库函数非常有用。在源码中，example 声明最好与解释相关概念的注释配合使用。

总结

类型类和重载

类型类是 Lean 中重载函数和运算符的机制。多态函数可以用于多种类型，但无论使用什么类型，其行为都是一致的。例如，一个连接两个列表的多态函数在使用时不关心列表中元素的类型，但它无法根据具体的元素类型表现出不同的行为。相比之下，使用类型类重载的运算符同样可以用于多种类型，但每个类型都需要提供自己的重载运算实现，这意味着可以根据不同的类型表现出不同的行为。

一个 类型类 包含名称、参数和类体，其中类体由若干个带有类型的名称组成。名称用于引用重载的运算，参数决定了定义的哪些方面可以被重载，类体提供了可重载运算的名称和类型签名。每一个可重载运算都被称为类型类的一个方法。类型类可以为某些方法提供基于其他方法的默认实现，从而使程序员无需手动实现每个重载（当可以自动完成时）。

类型类的 实例 为给定参数提供方法的具体实现。实例可以是多态的，在这种情况下它们能够适用于多种参数，同时也可以在某些类型存在更高效实现时提供更加特化的实现。

类型类参数分为 输入参数（默认情况）和 输出参数（通过 outParam 修饰）。Lean 只有在所有输入参数不再是元变量时才会开始实例搜索，而输出参数可以在实例搜索过程中被确定。类型类的参数不一定是类型，也可以是普通值。例如，OfNat 类型类用于重载自然数字面量，它将要被重载的 Nat 值本身作为参数，这使得实例可以限制允许的数字范围。

实例可以被标注为 @[default_instance] 属性。当一个实例是默认实例时，它会作为 Lean 因类型中存在元变量而无法找到实例时的回退选择。

常见语法的类型类

Lean 中的大多数中缀运算符都通过类型类进行重载。例如，加法运算符对应于 Add 类型类。大多数运算符都有对应的异构版本，其中两个参数不需要是相同类型。这些异构运算符使用以 H 开头的类型类进行重载，如 HAdd。

索引语法通过 GetElem 类型类进行重载，该类型类涉及证明。GetElem 有两个输出参数：要从集合中提取的元素类型，以及用于确定索引值是否在集合边界内的证据函数。这个证据通过命题来描述，Lean 在使用数组索引时会尝试证明这个命题。当 Lean 在编译时无法检查列表或数组访问操作是否越界时，可以通过在索引操作后添加 ? 将检查推迟到运行时。

函子

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

虽然函子是通过拥有 map 方法来定义的，但 Lean 中的 Functor 类型类还包含一个额外的默认方法，该方法负责将常量函数映射到值上，将所有类型由多态类型变量给出的值替换为同一个新值。对于某些函子，这比遍历整个结构更加高效。

派生实例

许多类型类都有非常标准的实现。例如，布尔相等类型类 BEq 通常的实现方式是先检查两个参数是否使用相同的构造器，然后检查它们的所有参数是否相等。这些类型类的实例可以 自动 创建。

在定义归纳类型或结构体时，在声明末尾添加 deriving 子句会使实例自动创建。此外，deriving instance ... for ... 命令可以在数据类型定义之外使用来生成实例。由于每个可以派生实例的类都需要特殊处理，因此并非所有类都是可派生的。

强制转换

强制转换允许 Lean 通过插入一个将数据从一种类型转换为另一种类型的函数调用，从原本会出现的编译时错误中恢复。例如，从任意类型 α 到类型 Option α 的强制转换使得值可以直接写出，而不需要用 some 构造器包装，这使得 Option 的工作方式更像面向对象语言中的可空类型。

存在多种不同类型的强制转换，它们可以从不同类型的错误中恢复，并且都由各自的类型类来表示。Coe 类型类用于从类型错误中恢复。当 Lean 遇到类型为 α 的表达式，但上下文期望类型为 β 的表达式时，Lean 会首先尝试构建一个能将 α 强制转换为 β 的转换链，只有在无法做到这一点时才会显示错误。CoeDep 类将被强制转换的具体值作为额外参数，这允许对该值进行进一步的类型类搜索，或者在实例中使用构造器来限制转换的适用范围。CoeFun 类在编译函数应用时会拦截“不是函数”的错误，并允许将函数位置的值转换为实际函数（如果可能的话）。