控制实例搜索

要方便地相加两个 Pos 类型，并产生另一个 Pos，一个 Add 类的的实例就足够了。但是，在许多情况下，参数可能有不同的类型，重载一个灵活的异质运算符是更为有用的。例如，让 Nat 和 Pos，或 Pos 和 Nat 相加总会是一个 Pos：

def addNatPos : Nat → Pos → Pos
  | 0, p => p
  | n + 1, p => Pos.succ (addNatPos n p)

def addPosNat : Pos → Nat → Pos
  | p, 0 => p
  | p, n + 1 => Pos.succ (addPosNat p n)

这些函数允许自然数与正数相加，但他们不能在 Add 类型类中，因为它希望 add 的两个参数都有同样的类型。

异质重载

就像在重载加法一节提到的，Lean 提供了名为 HAdd 的类型类来重载异质加法。 HAdd 类接受三个类型参数：两个参数的类型和一个返回类型。 HAdd Nat Pos Pos 和 HAdd Pos Nat Pos 的实例可以让常规加法符号可以接受不同类型。

instance : HAdd Nat Pos Pos where
  hAdd := addNatPos

instance : HAdd Pos Nat Pos where
  hAdd := addPosNat

有了上面两个实例，就有了下面的例子：

#eval (3 : Pos) + (5 : Nat)

#eval (3 : Nat) + (5 : Pos)

HAdd 的定义和下面 HPlus 的定义很像。下面是 HPlus 和它对应的实例：

class HPlus (α : Type) (β : Type) (γ : Type) where
  hPlus : α → β → γ

instance : HPlus Nat Pos Pos where
  hPlus := addNatPos

instance : HPlus Pos Nat Pos where
  hPlus := addPosNat

然而，HPlus 的实例明显没有 HAdd 的实例有用。当尝试用 #eval 使用这些实例时，一个错误就出现了：

#eval HPlus.hPlus (3 : Pos) (5 : Nat)

typeclass instance problem is stuck, it is often due to metavariables
  HPlus Pos Nat ?m.7527

发生错误是因为类型中有元变量，Lean 没办法解决它。

就像我们在多态一开始的描述里说的那样，元变量代表了程序无法被推断的未知部分。当一个表达式被写在 #eval 后时，Lean 会尝试去自动确定它的类型。在这种情况下，它无法做到自动确定类型。因为 HPlus 的第三个类型参数依然是未知的，Lean 没办法进行类型类实例搜索，但是实例搜索是 Lean 唯一可能确定表达式的类型的方式。也就是说，HPlus Pos Nat Pos 实例只能在表达式的类型为 Pos 时应用，但除了实例本身之外，程序中没有其他东西表明它应该具有这种类型。

一种解决方法是保证全部三个类型都是已知的，通过给整个表达式添加一个类型标记来实现这一点：

#eval (HPlus.hPlus (3 : Pos) (5 : Nat) : Pos)

然而，这种解决方式对使用我们的正数库的用户来说并不是很方便。

输出参数

刚才的问题也可以通过声明 γ 是一个 输出参数（output parameter） 来解决。多数类型类参数是作为搜索算法的输入：它们被用于选取一个实例。例如，在 OfNat 实例中，类型和自然数都被用于选取一个数字字面量的特定解释。然而，在一些情况下，在尽管有些类型参数仍然处于未知状态时就开始进行搜索是更方便的。这样就能使用在搜索中发现的实例来决定元变量的值。在开始搜索实例时不需要用到的参数就是这个过程的结果，该参数使用 outParam 修饰符来声明。

class HPlus (α : Type) (β : Type) (γ : outParam Type) where
  hPlus : α → β → γ

有了这个输出参数，类型类实例搜索就能够在不需要知道 γ 的情况下选取一个实例了。例如：

#eval HPlus.hPlus (3 : Pos) (5 : Nat)

认为输出参数相当于是定义某种函数在思考时可能会有帮助。任意给定的，类型类的实例都有一个或更多输出参数提供给 Lean。这能指导 Lean 通过输入（的类型参数）来确定输出（的类型）。一个可能是递归的实例搜索过程，最终会比简单的重载更为强大。输出参数能够决定程序中的其他类型，实例搜索能够将一族附属实例组合成具有这种类型的程序。

默认实例

确定一个参数是否是一个输入或输出参数控制了 Lean 会在何时启动类型类搜索。具体而言，直到所有输入都变为已知，类型类搜索才会开始。然而，在一些情况下，输出参数是不足的。此时，即使一些输入参数仍然处于未知状态，实例搜索也应该开始。这有点像是 Python 或 Kotlin 中可选函数参数的默认值，但在这里是默认类型。

默认实例 是 当并不是全部输入均为已知时 可用的实例。当一个默认实例能被使用时，他就将会被使用。这能帮助程序成功通过类型检查，而不是因为关于未知类型和元变量的错误而失败。但另一方面，默认类型会让实例选取变得不那么可预测。具体而言，如果一个不合适的实例被选取了，那么表达式将可能具有和预期不同的类型。这会导致令人困惑的类型错误发生在程序中。明智地选择要使用默认实例的地方！

默认实例可以发挥作用的一个例子是可以从 Add 实例派生出的 HPlus 实例。换句话说，常规的加法是异质加法在三个参数类型都相同时的特殊情况。这可以用下面的实例来实现：

instance [Add α] : HPlus α α α where
  hPlus := Add.add

有了这个实例，hPlus 就可以被用于任何可加的类型，就像 Nat：

#eval HPlus.hPlus (3 : Nat) (5 : Nat)

然而，这个实例只会用在两个参数类型都已知的情况下。例如：

#check HPlus.hPlus (5 : Nat) (3 : Nat)

产生类型

HPlus.hPlus 5 3 : Nat

就像我们预想的那样，但是

#check HPlus.hPlus (5 : Nat)

产生了一个包含剩余参数和返回值类型的两个元变量的类型：

HPlus.hPlus 5 : ?m.7706 → ?m.7708

在绝大多数情况下，当提供一个加法参数时，另一个参数也会是同一个类型。来让这个实例成为默认实例，应用 default_instance 属性：

@[default_instance]
instance [Add α] : HPlus α α α where
  hPlus := Add.add

有了默认实例，这个例子就有了更有用的类型：

#check HPlus.hPlus (5 : Nat)

结果为：

HPlus.hPlus 5 : Nat → Nat

每个同时重载了异质和同质运算的运算符，都能在默认实例需要异质运算的语境中使用同质运算。中缀运算符会被替换为异质运算，并且在需要时尽可能选择同质的默认实例。

简单来说，简单地写 5 会给出一个 Nat 而不是一个需要更多信息来选取 OfNat 实例的一个包含元变量的类型。这是因为 OfNat 以 Nat 作为默认实例。

默认实例也可以被赋予 优先级 ，这会影响在可能的应用多于一种的情况下的选择。更多关于默认实例优先级的信息，请查阅 Lean 手册。

练习

定义一个 HMul (PPoint α) α (PPoint α) 的实例，该实例将两个投影都乘以标量。它应适用于任何存在 Mul α 实例的类型 α。例如：

#eval {x := 2.5, y := 3.7 : PPoint Float} * 2.0

结果应为

{ x := 5.000000, y := 7.400000 }

Lean 函数式编程

控制实例搜索

异质重载

输出参数

默认实例

练习