正数

在一些应用场景下，我们只需要用到正数。对于编译器和解释器来说，它们通常使用起始于1的行和列数来表示源代码位置，并且一个用于表示非空列表的数据结构永远不会出现长度为零的情况。

一种表示正数的方法其实和 Nat 十分相似，只是用 one 作为基本情况而不是 zero 。

inductive Pos : Type where
  | one : Pos
  | succ : Pos → Pos

这个数据类型很好的代表了我们期望的值的集合，但是它用起来并不是很方便。比如说，无法使用数字字面量。

def seven : Pos := 7

failed to synthesize instance
  OfNat Pos 7

而是必须要直接使用构造子。

def seven : Pos :=
  Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ Pos.one)))))

类似地，加法和乘法用起来也很费劲。

def fourteen : Pos := seven + seven

failed to synthesize instance
  HAdd Pos Pos ?m.291

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 相加成为可能：

#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

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 类型的值可以使用常规的加法语法。

instance : Add Pos where
  add := Pos.plus

def fourteen : Pos := seven + seven

转换为字符串

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

例如，一种将 Pos 转换为 String 的方式就是解析它的内部结构。函数 posToString 接受一个决定是否给Pos.succ加上括号的 Bool 值，该值在第一次调用时应该为 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}"

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

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

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 实例，那么它可以用来显示 #eval 的结果，即使该类型并没有使用 deriving Repr 定义，所以 #eval seven 输出 7。

重载乘法运算符

对乘法来说，也有一个被称为 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]

[7, 49, 14]

数字字面量

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

Lean 是通过使用一个叫做 OfNat 的类型类来解释数字字面量的：

class OfNat (α : Type) (_ : Nat) where
  ofNat : α

这个类型类接受两个参数：α 是需要重载自然数的类型，未命名的 Nat 类型参数是你希望在程序中实际使用的数字字面量。 ofNat 方法被用作数字字面量的值。由于原类包含了 Nat 参数，因此可以仅为那些使数字有意义的值定义实例。

OfNat展示了类型类的参数不需要是类型。因为在 Lean 中，类型是语言中的一等公民，可以作为参数传递给函数，并且可以使用 def 和 abbrev 给出定义。 Lean 并不阻止非类型参数出现在类型类的参数位置上，但一些不够灵活的语言则不允许这种操作。这种灵活性能为特定的值以及特定的类型提供运算符重载。

例如，一个表示小于4的自然数的和类型可被定义如下：

inductive LT4 where
  | zero
  | one
  | two
  | three
deriving Repr

然而，并不是每个数字字面量对于这个类型都是合理的，只有小于4的数是合理的：

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)

LT4.three

#eval (0 : LT4)

LT4.zero

另一方面，越界的字面量也是不行的。

#eval (4 : LT4)

failed to synthesize instance
OfNat LT4 4

对于 Pos 来说，OfNat 实例应该适用于除 Nat.zero 外的任何 Nat。另一种表达方式是说，对于所有的自然数 n，该实例应该适用于 n + 1。就像 α 这样的名称会自动成为 Lean 自动填充的函数的隐式参数一样，实例也可以接受自动隐式参数。在这个实例中，参数 n 代表任何 Nat，并且该实例是为一个比给定 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 代表的数比用户实际写的要小一，所以辅助函数 natPlusOne 返回一个比它的参数大一的 Pos。这使得用自然数字面量表示正数成为可能，同时不会表示零：

def eight : Pos := 8

def zero : Pos := 0

failed to synthesize instance
  OfNat Pos 0

练习

另一种表示

另一种方式来表示正数是用某个 Nat 的后继。用一个名为 succ 的结构体替换 Pos 的定义，该结构体包含一个 Nat：

structure Pos where
  succ ::
  pred : Nat

定义 Add，Mul，ToString，和 OfNat的实例来让这个版本的 Pos 用起来更方便。

偶数

定义一个只表示偶数的数据类型。定义Add，Mul，和 ToString来让它用起来更方便。定义 OfNat 需要下一节中介绍的特性。

HTTP 请求

一个 HTTP 请求以一个 HTTP 方法的标识开始，比如 GET 或 POST，还包括一个 URI 和一个 HTTP 版本。定义一个归纳类型，代表 HTTP 方法的一个有趣的子集，并且定义一个表示 HTTP 响应的结构体。响应应该有一个 ToString 实例，使得可以对其进行调试。使用一个类型类来将不同的 IO 操作与每个 HTTP 方法关联起来，并编写一个测试工具作为一个 IO 操作，调用每个方法并打印结果。

Lean 函数式编程