3.1.1. 类和实例🔗

一个类型类是由名称，一些参数，和一族 方法（Method） 组成。参数定义了可重载运算符的类型，而方法则是可重载运算符的名称和类型签名。这里再次出现了与面向对象语言之间的术语冲突。在面向对象编程中，一个方法本质上是一个与内存中的一个特定对象有关联的函数，并且具有访问该对象的私有状态的特权。我们通过方法与对象进行交互。在 Lean 中，“方法”这个词项指的是一个被声明为可重载的运算符，与对象、值或是私有字段并无特殊关联。

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

8

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

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

该声明表示存在一个类型类 Plus，它重载了关于类型 α 的操作。 具体到这段代码，存在一个名为 plus 的重载操作，它接受两个 α 并返回一个 α。

类型类是一等公民，就像类型是一等公民一样。我们其实可以说，类型类是另一种类型。 Plus 的类型是 Type → Type，因为它接受一个类型作为参数 (α) 并产生一个新类型，该类型描述了 Plus 的运算符对 α 的重载。

写一个实例来为特定类型重载 plus ：

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

默认情况下，类型类方法定义在与类型类同名的命名空间中。 如果将该命名空间打开（使用 open 指令）会使该方法使用起来十分方便——这样用户就不用先输入类名了。 open 指令后跟的括号表示只有括号内指定的名称才可以被访问。

8

为 Pos 定义加法函数和 Plus Pos 的实例允许 plus 用于将 Pos 和 Nat 值相加：

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

failed to synthesize
  Plus Float

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

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

3.1.2. 重载加法🔗

Lean 的内置加法运算符是名为 HAdd 的类型类的语法糖，它灵活地允许加法参数具有不同的类型。 HAdd 是异构加法的缩写。 例如，可以编写一个 HAdd 实例，以允许将 Nat 添加到 Float 中，从而产生一个新的 Float。 当程序员编写 x + y 时，它被解释为 HAdd.hAdd x y。

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

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

3.1.3. 转换为字符串🔗

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

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

将此函数用于 ToString 实例：

结果是信息丰富但又但可能过于冗长的输出：

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

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

"There are 7"

当定义了多个实例时，最新的实例优先。 此外，如果一个类型具有 ToString 实例，那么它也可以用于显示 #eval 的结果，因此 #eval seven 输出 7。

3.1.4. 重载乘法🔗

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

Mul 的实例允许将普通乘法语法与 Pos 一起使用：

有了这个实例，乘法就可以正常工作了：

[7, 49, 14]

3.1.5. 数字字面量🔗

写一串构造器来表示正数是非常不方便的。一种解决问题的方法是提供一个将 Nat 转换为 Pos 的函数。 然而，这种方法也有缺点。 首先，因为 Pos 不能表示 0，所以生成的函数要么将 Nat 转换为更大的数字，要么返回 Option Pos。 这两种方法对用户来说都不是特别方便。其次，需要显式调用函数会让使用正数的程序不如使用 Nat 的程序那么方便。 在精确的类型和方便的 API 之间权衡一下后，精确的类型还是没那么有用。

有三个类型类用于重载数字字面量：Zero，One，和 OfNat。 因为许多类型的值很自然地写作 0 ，所以 Zero 类允许重写这些特定值。 它的定义如下：

因为 0 不是正数，所以不应该有 Zero Pos 的实例。

类似地，许多类型的值很自然地写作 1 。所以 One 类允许重写这些特定值：

One Pos 的实例很有意义：

有了这个实例，1 可以用于 Pos.one：

1

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

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

OfNat 表明类型类的参数不必是类型。 因为 Lean 中的类型是语言的一等公民，可以作为参数传递给函数，并使用 def 和 abbrev 进行定义，所以在灵活性较差的语言无法允许的位置，没有障碍阻止非类型参数。 这种灵活性允许为特定值和特定类型提供重载操作。 此外，它还允许 Lean 标准库安排在存在 OfNat α 0 实例时存在 Zero α 实例，反之亦然。 类似地，One α 的实例意味着 OfNat α 1 的实例，就像 OfNat α 1 的实例意味着 One α 的实例一样。

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

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

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

LT4.three

LT4.zero

另一方面，仍然不允许使用越界字面量：

failed to synthesize
  OfNat LT4 4
numerals are polymorphic in Lean, but the numeral `4` cannot be used in a context where the expected type is
  LT4
due to the absence of the instance above

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

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

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

failed to synthesize
  OfNat Pos 0
numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
  Pos
due to the absence of the instance above

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

3.1.6. 练习🔗