类型类与多态

编写适用于给定函数的任意重载可能会很有用。例如，IO.println 适用于任何具有 ToString 实例的类型。这通过在所需实例周围使用方括号来表示： IO.println 的类型是 {α : Type} → [ToString α] → α → IO Unit。这个类型表示 IO.println 接受一个类型为 α 的参数，并且 Lean 应该自动确定这个类型，而且必须有一个可用于 α 的 ToString 实例。它返回一个 IO 操作。

对多态函数的类型检查

对接受隐式参数，或使用了类型类的函数进行类型检查时，我们需要用到一些额外的语法。简单地写

#check (IO.println)

会产生一个包含元变量的类型。

IO.println : ?m.3620 → IO Unit

这里显示出了元变量是因为即使 Lean 尽全力去寻找隐式参数，但还是没有找到足够的类型信息来做到这一点。要理解函数的签名，可以在函数名之前加上一个 at 符号（@）来抑制此特性。

#check @IO.println

@IO.println : {α : Type u_1} → [inst : ToString α] → α → IO Unit

在这个输出信息中，实例本身被给予了 inst 这个名字。此外，Type 后面有一个 u_1 ，这里使用了目前尚未介绍的 Lean 的特性。我们可以暂时忽略这些 Type 的参数。

定义含隐式实例的多态函数

一个对列表中所有条目求和的函数需要两个实例：Add允许对条目进行加法运算，而OfNat实例为0提供了一个合理的值，以便对空列表进行返回。

def List.sum [Add α] [OfNat α 0] : List α → α
  | [] => 0
  | x :: xs => x + xs.sum

这个函数可以被用于 Nat 列表：

def fourNats : List Nat := [1, 2, 3, 4]

#eval fourNats.sum

但不能被用于 Pos 列表：

def fourPos : List Pos := [1, 2, 3, 4]

#eval fourPos.sum

failed to synthesize instance
  OfNat Pos 0

在方括号中的所需实例规范被称为 隐式实例（instance implicits） 。在幕后，每个类型类都定义了一个结构，该结构具有每个重载操作的字段。实例是该结构类型的值，每个字段包含一个实现。在调用时，Lean负责为每个隐式实例参数找到一个实例值传递。普通的隐式参数和隐式实例最重要的不同就是 Lean 寻找参数值的策略。对于普通的隐式参数，Lean 使用一种被称为 归一化（unification） 的技术来找到一个唯一的能使程序通过类型检查的参数值。这个过程只依赖于函数定义中的具体类型和调用时。

就像对 Pos 的 OfNat 实例用一个自然数 n 作为自动隐式参数，实例本身也可能接受隐式实例参数。在多态那一节中展示了一个多态点类型：

structure PPoint (α : Type) where
  x : α
  y : α
deriving Repr

点之间的加法需要将从属的 x 和 y 字段相加。因此，PPoint 的 Add 实例需要这些字段所具有的类型的 Add 实例。换句话说，PPoint 的 Add 实例需要进一步的 α 的 Add 实例。

instance [Add α] : Add (PPoint α) where
  add p1 p2 := { x := p1.x + p2.x, y := p1.y + p2.y }

当 Lean 遇到两点之间的加法，它会寻找并找到这个实例。然后会更进一步寻找 Add α 实例。

用这种方式构造的实例值是类型类的结构体类型的值。一个成功的递归实例搜索会产生一个结构体值，该结构体值引用了另一个结构体值。一个 Add (PPoint Nat) 实例包含对找到的 Add Nat 实例的引用。

这种递归搜索意味着类型类显著地比普通重载函数更加强大。一个多态实例库是一个由代码砖块组成的集合，编译器会根据所需的类型自行搭建。接受实例参数的多态函数是对类型类机制的潜在请求，以在幕后组装辅助函数。 API的客户端无需手工组合所有必要的部分，从而使用户从这类烦人的工作中解放出来。

方法与隐式参数

@OfNat.ofNat 的类型可能会令人惊讶。它是 {α : Type} → (n : Nat) → [OfNat α n] → α，其中 Nat 参数 n 作为显式函数参数出现。然而，在方法的声明中，ofNat 只是类型 α。这种看似的不一致是因为声明一个类型类实际上会产生以下结果：

声明一个包含了每个重载操作的实现的结构体类型
声明一个与类同名的命名空间
对于每个方法，会在类的命名空间中声明一个函数，该函数从实例中获取其实现。

这类似于声明新结构也声明访问器函数的方式。主要区别在于结构的访问器函数将结构值作为显式参数，而类型类方法将实例值作为隐式实例，由 Lean 自动查找。

为了让Lean找到一个实例，它的参数必须是可用的。这意味着类型类的每个参数必须是出现在实例之前的方法的参数。当这些参数是隐式的时候最方便，因为Lean会发现它们的值。例如，@Add.add 的类型是 {α : Type} → [Add α] → α → α → α。在这种情况下，类型参数 α 可以是隐式的，因为对 Add.add 的参数提供了关于用户意图的类型信息。然后，可以使用这种类型来搜索 Add 实例。

而在 ofNat 的例子中，要被解码的特定 Nat 字面量并没有作为其他参数的一部分出现。这意味着 Lean 在尝试确定隐式参数 n 时将没有足够的信息可以用。如果Lean选择使用隐式参数，那么结果将是一个非常不方便的 API。因此，在这些情况下，Lean 选择为类方法提供一个显式参数。

Lean 函数式编程

类型类与多态

对多态函数的类型检查

定义含隐式实例的多态函数

方法与隐式参数

练习

偶数数字字面量

递归实例搜索深度