标准类

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

算术符号

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

位运算符

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

由于 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 ·) 会报错：

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 是一个命题。

#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" 会导致：

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

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

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

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

inductive Ordering where
| lt
| eq
| gt

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

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

哈希

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

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 实例：

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

instance : Hashable Pos where
  hash := hashPos

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

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

在二叉树的 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

派生标准类

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

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

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

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

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

• Inhabited
• BEq
• Repr
• Hashable
• Ord

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

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

Appending

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

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

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

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

在定义了上面的实例后，

#eval idahoSpiders ++ idahoSpiders

就有了下面的结果：

{ 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 来使常规列表可以和一个非空列表连接。

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

有了这个实例后，

#eval idahoSpiders ++ ["Trapdoor Spider"]

结果为

{ 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]"
• 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 函数。

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 实现为一个函子的实例：

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 可以连接任何非空列表的条目，只要条目是可连接的：

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 实现方式。

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

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

就像不符合 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 不能为所有类派生实例。 例如代码

deriving instance ToString for NonEmptyList

会导致如下错误：

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

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

练习

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