3.1. 正数
在某些应用中，只有正数才有意义。 例如，编译器和解释器通常对源代码位置使用从一开始计数的行号和列号，而表示非空列表的数据类型永远不会报告长度为零。 与其依赖自然数，并在代码中到处加入该数不为零的断言，不如设计一种只表示正数的数据类型。
表示正数的一种方式与 Nat 非常相似，只是以 one 作为基本情形，而不是 zero：
inductive Pos : Type where
| one : Pos
| succ : Pos → Pos此数据类型精确地表示了预期的值集合，但使用起来并不十分方便。 例如，数值字面量会被拒绝：
def seven : Pos := 7相反，必须直接使用构造子：
def seven : Pos :=
Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ Pos.one)))))类似地，加法和乘法也不容易使用：
def fourteen : Pos := seven + sevendef fortyNine : Pos := seven * seven
这些错误消息中的每一条都以 failed to synthesize 开头。
这表明错误是由尚未实现的重载操作导致的，并且它描述了必须实现的类型类。
3.1.1. 类与实例
类型类由一个名称、若干参数以及一组 方法 组成。 这些参数描述正在为哪些类型定义可重载操作，而方法则是这些可重载操作的名称和类型签名。 这里再次出现了与面向对象语言的术语冲突。 在面向对象编程中，方法本质上是一个与内存中特定对象相连接的函数，并且能够特殊地访问该对象的私有状态。 对象通过其方法进行交互。 在 Lean 中，“方法”一词指的是一个已声明为可重载的操作，它与对象、值或私有字段没有特殊联系。
重载加法的一种方式是定义一个名为 Plus 的类型类，其中包含一个名为 plus 的加法方法。
一旦为 Nat 定义了 Plus 的实例，就可以使用 Plus.plus 将两个 Nat 相加：
#eval Plus.plus 5 3
添加更多实例会使 Plus.plus 能够接受更多类型的参数。
在下面的类型类声明中，Plus 是类名，α : Type 是唯一的参数，plus : α → α → α 是唯一的方法：
class Plus (α : Type) where
plus : α → α → α
这个声明表示存在一个类型类 Plus，它针对类型 α 对操作进行重载。
特别地，其中有一个名为 plus 的重载操作，它接受两个 α 并返回一个 α。
类型类是一等的，正如类型是一等的一样。
特别地，类型类是另一种类型。
Plus 的类型是 Type → Type，因为它接受一个类型作为实参（α），并产生一个新的类型，该类型描述了 α 上 Plus 操作的重载。
要为某个特定类型重载 plus，请编写一个实例：
instance : Plus Nat where
plus := Nat.add
instance 后面的冒号表明 Plus Nat 确实是一个类型。
类 Plus 的每个方法都应当使用 := 赋予一个值。
在此例中，只有一个方法：plus。
默认情况下，类型类方法定义在与该类型类同名的命名空间中。
对该命名空间执行 open 可能很方便，这样用户就不需要先键入类名。
open 命令中的圆括号表示只使该命名空间中所指明的名称可访问：
open Plus (plus)#eval plus 5 3
为 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这些错误表示 Lean 无法为给定的类型类找到实例。
3.1.2. 重载加法
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.plusdef fourteen : Pos := seven + seven3.1.3. 转换为字符串
另一个有用的内建类称为 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 实例：
instance : ToString Pos where
toString := posToString true会得到信息丰富但令人难以招架的输出：
#eval s!"There are {seven}"
另一方面，每个正数都有一个对应的 Nat。
将它转换为一个 Nat，然后使用 ToString Nat 实例（也就是 Nat 上 ToString 的重载），是一种快速生成短得多的输出的方法：
def Pos.toNat : Pos → Nat
| Pos.one => 1
| Pos.succ n => n.toNat + 1instance : ToString Pos where
toString x := toString (x.toNat)#eval s!"There are {seven}"
当定义了多个实例时，最近定义的实例具有优先权。
此外，如果一个类型具有 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 使用通常的乘法语法：
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]3.1.5. 数字字面量
为正数写出一串构造子相当不便。
解决这个问题的一种方法是提供一个函数，将 Nat 转换为 Pos。
然而，这种方法有其缺点。
首先，由于 Pos 不能表示 0，所得函数要么会把一个 Nat 转换为更大的数，要么会返回 Option Pos。
这两种方式对用户来说都并不特别方便。
其次，必须显式调用该函数，会使使用正数的程序比使用 Nat 的程序书写起来不方便得多。
精确类型与便利 API 之间存在取舍，意味着精确类型会变得不那么有用。
有三个类型类用于重载数值字面量：Zero、One 和 OfNat。
由于许多类型都有一些自然地用 0 书写的值，Zero 类允许重写这些特定的值。
它定义如下：
class Zero (α : Type) where
zero : α
因为 0 不是正数，所以不应存在 Zero Pos 的实例。
类似地，许多类型具有自然地用 1 书写的值。
One 类允许重写这些表示：
class One (α : Type) where
one : α
One Pos 的一个实例完全合理：
instance : One Pos where
one := Pos.one
有了这个实例，1 就可以用于 Pos.one：
#eval (1 : Pos)
在 Lean 中，自然数字面量通过一个名为 OfNat 的类型类来解释：
class OfNat (α : Type) (_ : Nat) where
ofNat : α
这个类型类接受两个参数：α 是对自然数进行重载的目标类型，而未命名的 Nat 参数是在程序中实际遇到的字面量数字。
随后，方法 ofNat 被用作该数值字面量的值。
由于该类包含 Nat 参数，因此可以只为那些数字有意义的值定义实例。
OfNat 表明，类型类的参数不必是类型。
由于 Lean 中的类型是该语言中的一等参与者，可以作为参数传递给函数，也可以用 def 和 abbrev 给出定义，因此不存在任何障碍会阻止在某些位置使用非类型参数；在灵活性较低的语言中，这些位置可能不允许这样的参数。
这种灵活性使得可以为特定值以及特定类型提供重载运算。
此外，它还使 Lean 标准库能够安排在存在 OfNat α 0 实例时也存在 Zero α 实例，反之亦然。
类似地，One α 的实例蕴含 OfNat α 1 的实例，正如 OfNat α 1 的实例蕴含 One α 的实例一样。
表示小于四的自然数的和类型可以定义如下：
inductive LT4 where
| zero
| one
| two
| three虽然允许任意数字字面量用于此类型并不合理，但小于四的数字显然是合理的：
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)#eval (0 : LT4)另一方面，越界字面量仍然是不允许的：
#eval (4 : LT4)
对于 Pos，OfNat 实例应当适用于除 Nat.zero 之外的任意 Nat。
另一种表述方式是：对于所有自然数 n，该实例应当适用于 n + 1。
正如像 α 这样的名称会自动成为由 Lean 自行填充的函数隐式参数一样，实例也可以接受自动隐式参数。
在这个实例中，参数 n 代表任意 Nat，而该实例是为大一的 Nat 定义的：
instance : OfNat Pos (n + 1) where
ofNat :=
let rec natPlusOne : Nat → Pos
| 0 => Pos.one
| k + 1 => Pos.succ (natPlusOne k)
natPlusOne n
由于 n 表示比用户所写的数小一的 Nat，辅助函数 natPlusOne 返回一个比其参数大一的 Pos。
这使得可以将自然数文字用于正数，但不能用于零：
def eight : Pos := 8def zero : Pos := 03.1.6. 练习
3.1.6.1. 另一种表示
表示正数的另一种方式是把它表示为某个 Nat 的后继。
请将 Pos 的定义替换为一个结构，其构造子名为 succ，并包含一个 Nat：
structure Pos where
succ ::
pred : Nat
3.1.6.2. 偶数
定义一个只表示偶数的数据类型。定义 Add、Mul 和 ToString 的实例，使其能够被方便地使用。
OfNat 需要 下一节 中引入的特性。
3.1.6.3. HTTP 请求
一个 HTTP 请求以标识 HTTP 方法开始，例如 GET 或 POST，并伴随一个 URI 和一个 HTTP 版本。
定义一个归纳类型来表示 HTTP 方法中一个有意义的子集，并定义一个结构来表示 HTTP 响应。
响应应当具有一个 ToString 实例，使其能够被调试。
使用一个类型类将不同的 IO 动作与每个 HTTP 方法关联起来，并编写一个作为 IO 动作的测试框架，调用每个方法并打印结果。