3.5. 标准类
本节介绍在 Lean 中可以使用类型类重载的各种运算符和函数。每个运算符或函数都对应一个类型类的方法。
与 C++ 不同，Lean 中的中缀运算符被定义为命名函数的缩写；这意味着为新类型重载它们不是使用运算符本身，而是使用底层名称（例如 HAdd.hAdd）。
3.5.1. 算术
多数算术运算符都是可以进行异质运算的。这意味着参数可能有不同的类型，并且输出参数决定了结果表达式的类型。
对于每个异质运算符，都有一个同质运算符与其对应。可以通过删除字母 h 来找到，比如 HAdd.hAdd 变为 Add.add。
下面的算术运算符都可以被重载：
表达式 | 脱糖后 | 类名 |
|---|---|---|
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
3.5.2. 位运算符
Lean 包含许多使用类型类重载的标准位运算符。
对于固定宽度的类型，例如 UInt8、UInt16、UInt32、UInt64 和 USize，都有实例。
后者是当前平台上的字长，通常为 32 或 64 位。
以下位运算符被重载：
表达式 | 脱糖后 | 类名 |
|---|---|---|
|
| |
|
| |
|
| |
|
|
|
| ||
|
因为名称 And 和 Or 已被用作逻辑连接词的名称，所以 HAnd 和 HOr 的同质版本称为 AndOp 和 OrOp，而不是 And 和 Or。
3.5.3. 等价性与有序性
测试两个值的等价性通常使用 BEq 类，它是 Boolean equality（布尔等价）的缩写。
由于 Lean 用作定理证明器，因此 Lean 中实际上有两种等价运算符：
-
布尔等价 和你能在其他编程语言中看到的等价是一样的。它是一个接受两个值并返回一个
Bool的函数。布尔等价用两个等号书写，就像在 Python 和 C# 中一样。因为 Lean 是一种纯函数式语言，指针并不能被直接看到，所以地址和值等价并没有符号上的区别。 -
命题等价 是两个事物等价的数学陈述。命题等价不是一个函数；相反，它是一个承认证明的数学陈述。它用一个等号书写。命题等价的陈述就像一个对这种等价性的证据进行分类的类型。
这两种等价都很重要，它们有不同的用处。布尔等价在程序中很有用，有时我们需要考察两个值是否是等价的。
例如，"Octopus" == "Cuttlefish" 的结果为 false，而 "Octopodes" == "Octo".append "podes" 的结果为 true。
某些值，例如函数，无法检查其等价性。例如，(fun (x : Nat) => 1 + x) == (Nat.succ ·) 会产生错误：
正如该消息所示，== 是使用类型类重载的。
表达式 x == y 实际上是 BEq.beq x y 的简写。
命题等价性是一个数学陈述，而不是程序的调用。
因为命题就像描述某个陈述的证据的类型，所以命题等价性与像 String 和 Nat → List Int 这样的类型比与布尔等价性有更多的共同点。
这意味着它不能自动检查。然而，只要两个表达式具有相同的类型，就可以在 Lean 中陈述它们的等价性。
陈述 (fun (x : Nat) => 1 + x) = (Nat.succ ·) 是一个完全合理的陈述。
从数学的角度来看，如果两个函数将等价的输入映射到等价的输出，那么它们就是等价的，所以这个陈述甚至是正确的，尽管它需要一行证明。
一般来说，当使用 Lean 作为编程语言时，最好坚持使用布尔函数而不是命题。
然而，正如 Bool 的构造函数的名称 true 和 false 所暗示的那样，这种差异有时会变得模糊。
有些命题是可判定的，这意味着它们可以像布尔函数一样被检查。
检查命题是真还是假的函数称为判定过程，它返回命题真假的证据。
可判定命题的一些例子包括自然数的相等和不相等、字符串的相等，以及本身可判定的命题的“与”和“或”。
在 Lean 中，if 与可判定命题一起工作。
例如，2 < 4 是一个命题：
#check 2 < 4
尽管如此，将其写成 if 中的条件是完全可以接受的。
例如，if 2 < 4 then 1 else 2 的类型为 Nat，计算结果为 1。
并非所有命题都是可判定的。如果它们是，那么计算机只需运行判定过程就可以证明任何真实的命题，数学家就会失业。
更具体地说，可判定命题具有 Decidable 类型类的实例，该实例包含判定过程。
试图将不可判定的命题当作 Bool 来使用会导致找不到 Decidable 实例。
例如，if (fun (x : Nat) => 1 + x) = (Nat.succ ·) then "yes" else "no" 会导致：
以下通常是可判定的命题，使用类型类进行重载：
表达式 | 脱糖后 | 类名 |
|---|---|---|
|
| |
|
| |
|
| |
|
|
因为尚未演示如何定义新命题，所以可能很难定义 LT 和 LE 的全新实例。
但是，它们可以根据现有实例来定义。
Pos 的 LT 和 LE 实例可以使用 Nat 的现有实例：
instance : LT Pos where
lt x y := LT.lt x.toNat y.toNatinstance : LE Pos where
le x y := LE.le x.toNat y.toNat
这些命题默认情况下是不可判定的，因为 Lean 在合成实例时不会展开命题的定义。
这可以使用 inferInstanceAs 运算符来弥合，该运算符在存在时为给定类查找实例：
instance {x : Pos} {y : Pos} : Decidable (x < y) :=
inferInstanceAs (Decidable (x.toNat < y.toNat))
instance {x : Pos} {y : Pos} : Decidable (x ≤ y) :=
inferInstanceAs (Decidable (x.toNat ≤ y.toNat))类型检查器确认命题的定义匹配。 混淆它们会导致错误：
instance {x : Pos} {y : Pos} : Decidable (x ≤ y) :=
inferInstanceAs (Decidable (x.toNat < y.toNat))
使用 <、== 和 > 比较值可能效率低下。
首先检查一个值是否小于另一个值，然后检查它们是否相等，可能需要对大型数据结构进行两次遍历。
为了解决这个问题，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 就对了。
3.5.4. 哈希
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# 中对哈希的要求是一致的。
标准库包含一个类型为 UInt64 → UInt64 → UInt64 的函数 mixHash，可用于组合构造函数不同字段的哈希值。
可以通过为每个构造函数分配一个唯一的数字，然后将该数字与每个字段的哈希值混合来为归纳数据类型编写一个合理的哈希函数。
例如，可以为 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 := hashBinTree3.5.5. 派生标准类
像 BEq 和 Hashable 这样的类的实例通常很难手动实现。
Lean 包含一个称为实例派生的功能，它允许编译器自动构造许多类型类的行为良好的实例。
实际上，在 多态性的第一部分 中 Firewood 的定义中的 deriving Repr 短语就是实例派生的一个例子。
派生实例的方法有两种。第一种在定义一个结构体或归纳类型时使用。
在这种情况下，在类型声明的末尾添加 deriving，后跟应为其派生实例的类的名称。
对于已经定义的类型，可以使用独立的 deriving 命令。
事后为类型 T 派生 C1, C2, ... 的实例，请编写 deriving instanceC1, C2, ...for T。
可以使用非常少的代码为 Pos 和 NonEmptyList 派生 BEq 和 Hashable 实例：
deriving instance BEq, Hashable for Pos
deriving instance BEq, Hashable for NonEmptyList至少可以为以下类派生实例：
然而，在某些情况下，派生的 Ord 实例可能无法精确地产生应用程序中所需的排序。
在这种情况下，可以手动编写 Ord 实例。你如果对自己的 Lean 水平足够有自信的话，你也可以自己添加可以派生实例的类型类。
实例派生除了在开发效率和代码可读性上有很大的优势外，它也使得代码更易于维护，因为实例会随着类型定义的变化而更新。 对数据类型的一系列更新更易于阅读，因为不需要一行又一行地对相等性测试和哈希计算进行公式化的修改。
3.5.6. 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具有以下输出：
同样，HAppend 的定义允许将非空列表连接到普通列表：
instance : HAppend (NonEmptyList α) (List α) (NonEmptyList α) where
hAppend xs ys :=
{ head := xs.head, tail := xs.tail ++ ys }有了这个实例，
#eval idahoSpiders ++ ["Trapdoor Spider"]结果为
3.5.7. 函子
如果一个多态类型重载了一个名为 map 的函数，该函数通过一个函数映射其中包含的每个元素，那么它就是一个 函子。
虽然大多数语言都使用这个术语，但 C# 中与 map 等效的函数称为 System.Linq.Enumerable.Select。
例如，用一个函数对一个列表进行映射会产生一个新的列表，列表中的每个元素都是函数应用在原列表中元素的结果。
用函数 f 映射 Option 会使 none 保持不变，并将 some x 替换为 some (f x)。
以下是一些函子以及它们的 Functor 实例如何重载 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] -
List.reverse <$> [[1, 2, 3], [4, 5, 6]]结果为[[3, 2, 1], [6, 5, 4]]。
NonEmptyList 的 Functor 实例需要指定 map 函数。
instance : Functor NonEmptyList where
map f xs := { head := f xs.head, tail := f <$> xs.tail }
在这里，map 使用 List 的 Functor 实例将函数映射到尾部。
此实例是为 NonEmptyList 定义的，而不是为 NonEmptyList α 定义的，因为参数类型 α 在解析类型类中不起作用。
无论条目的类型是什么，都可以用函数来映射 NonEmptyList 。
如果 α 是该类的参数，那么就可以创建仅适用于 NonEmptyList Nat 的 Functor 版本，但作为函子的一部分是 map 适用于任何条目类型。
以下是 PPoint 的 Functor 实例：
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。
忽略其参数的函数称为常量函数，因为它们总是返回相同的值。
以下是 Functor 的定义，其中 mapConst 具有默认实现：
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 的一个糟糕的 Functor 实例可能会将 f x 放在 x 和 y 字段中，或者交换它们。
具体来说，Functor 实例应遵循两条规则：
-
映射恒等函数应产生原始参数。
-
映射两个组合函数应与组合它们的映射具有相同的效果。
更正式地说，第一条规则说 id <$> x 等于 x。
第二条规则说 map (fun y => f (g y)) x 等于 map f (map g x)。
组合 f ∘ g 也可以写成 fun y => f (g y)。
这些规则阻止了移动数据或删除部分数据的 map 的实现。
3.5.8. 您可能会遇到的消息
Lean 无法为所有类派生实例。 例如，代码
deriving instance ToString for NonEmptyList导致以下错误：
调用 deriving instance 会使 Lean 查阅类型类实例的代码生成器的内部表。
如果找到代码生成器，则会在提供的类型上调用它以创建实例。
然而，此消息意味着没有为 ToString 找到代码生成器。