10. 类型类（Type Classes）10. Type Classes🔗

类型类（Type classes）被引入作为在函数式编程语言中实现特设多态（ad-hoc polymorphism）的一种有原则的方式。我们首先观察到，如果函数简单地将加法的类型特定实现作为一个参数，然后在该参数上调用该实现，那么实现一个特设多态函数（如加法）将是容易的。例如，假设我们在 Lean 中声明一个结构体（structure）来保存加法的实现。

namespace Ex

structure Add (α : Type) where
add : α → α → α

@Add.add : {α : Type} → Add α → α → α → α#check @Add.add

@Add.add : {α : Type} → Add α → α → α → α

end Ex

在上述 Lean 代码中，字段 add 的类型是 Add.add : {α : Type} → Add α → α → α → α，其中类型 α 周围的花括号表示它是一个隐式参数（implicit argument）。我们可以按如下方式实现 double：

namespace Ex
structure Add (α : Type) where
add : α → α → α

def double (s : Add α) (x : α) : α :=
s.add x x

20#eval double { add := Nat.add } 10

100#eval double { add := Nat.mul } 10

20#eval double { add := Int.add } 10

end Ex

注意，你可以通过 double { add := Nat.add } n 来翻倍一个自然数 n。当然，要求用户以这种方式手动传递实现将非常繁琐。事实上，这将破坏特设多态的大部分潜在好处。

类型类背后的主要思想是使诸如 Add α 这样的参数变为隐式（implicit），并使用用户定义实例（instance）的数据库，通过一个称为类型类解析（typeclass resolution）的过程来自动合成所需的实例。在 Lean 中，将上例中的 structure 改为 class 后，Add.add 的类型变为：

namespace Ex

class Add (α : Type) where
add : α → α → α

@Add.add : {α : Type} → [self : Add α] → α → α → α#check @Add.add

@Add.add : {α : Type} → [self : Add α] → α → α → α

end Ex

其中方括号表示 Add α 类型的参数是 实例隐式（instance implicit），即它应通过类型类解析来合成。add 的这个版本是 Lean 对 Haskell 术语 add :: Add a => a -> a -> a 的类比。类似地，我们可以通过以下方式注册实例（instance）：

namespace Ex
class Add (α : Type) where
add : α → α → α

instance : Add Nat where
add := Nat.add

instance : Add Int where
add := Int.add

instance : Add Float where
add := Float.add

end Ex

那么对于 n : Nat 和 m : Nat，项 Add.add n m 会触发以 Add Nat 为目标的类型类解析，类型类解析将合成为 Nat 的实例。我们现在可以按如下方式使用实例隐式（instance implicit）重新实现 double：

namespace Ex
class Add (α : Type) where
add : α → α → α
instance : Add Nat where
add := Nat.add
instance : Add Int where
add := Int.add
instance : Add Float where
add := Float.add

def double [Add α] (x : α) : α :=
Add.add x x

@double : {α : Type} → [Add α] → α → α#check @double

@double : {α : Type} → [Add α] → α → α

20#eval double 10

20#eval double (10 : Int)

14.000000#eval double (7 : Float)

14.000000

482.000000#eval double (239.0 + 2)

482.000000

end Ex

一般来说，实例可能以复杂的方式依赖于其他实例。例如，你可以声明一个实例：如果 α 具有加法，那么 Array α具有加法：

instance [Add α] : Add (Array α) where
add x y := Array.zipWith (· + ·) x y

#[4, 6]#eval Add.add #[1, 2] #[3, 4]

#[4, 6]

#[4, 6]#eval #[1, 2] + #[3, 4]

#[4, 6]

注意，(· + ·) 是 Lean 中 fun x y => x + y 的记号。

上面的示例演示了如何使用类型类来重载记号（notation）。现在，我们探索另一个应用。我们经常需要某个给定类型的一个任意元素。回想一下，在 Lean 中类型可能没有任何元素。我们经常希望在一个"边界情况"下返回一个任意元素。例如，当 xs 的类型为 List α 时，我们希望表达式 head xs 的类型为 α。类似地，许多定理在附加假设一个类型非空的情况下成立。例如，如果 α 是一个类型，∃ x : α, x = x 仅当 α 非空时才为真。标准库定义了一个类型类 Inhabited 以允许类型类推断来推断一个居留类型（inhabited type）的"默认"元素。让我们从上面程序的第一步开始，声明一个合适的类（class）：

namespace Ex

class Inhabited (α : Type u) where
default : α

@Inhabited.default : {α : Type u_1} → [self : Inhabited α] → α#check @Inhabited.default

@Inhabited.default : {α : Type u_1} → [self : Inhabited α] → α

end Ex

注意 Inhabited.default 没有任何显式参数（explicit arguments）。

类 Inhabited α 的一个元素就是形如 Inhabited.mk x 的表达式，其中 x : α 是某个元素。投影（projection）Inhabited.default 允许我们从 Inhabited α 的元素中"提取"出 α 的一个元素。现在我们用一些实例来填充这个类：

namespace Ex
class Inhabited (a : Type _) where
default : a

instance : Inhabited Bool where
default := true

instance : Inhabited Nat where
default := 0

instance : Inhabited Unit where
default := ()

instance : Inhabited Prop where
default := True

0#eval (Inhabited.default : Nat)

true#eval (Inhabited.default : Bool)

true

end Ex

你可以使用命令 export 为 Inhabited.default 创建别名 default。

namespace Ex
class Inhabited (a : Type _) where
default : a
instance : Inhabited Bool where
default := true
instance : Inhabited Nat where
default := 0
instance : Inhabited Unit where
default := ()
instance : Inhabited Prop where
default := True

export Inhabited (default)

0#eval (default : Nat)

true#eval (default : Bool)

true

end Ex

10.1. 链接实例（Chaining Instances）10.1. Chaining Instances🔗

如果类型类推断仅限于此，那它并不令人印象深刻；它只不过是一种在查找表中存储实例列表以供精化器（elaborator）查找的机制。使类型类推断强大的是可以链接（chain）实例。也就是说，一个实例声明可以依次依赖于一个类型类的隐式实例。这导致类推断递归地链接实例，必要时进行回溯，类似于 Prolog 的搜索。

例如，以下定义表明如果两个类型 α 和 β 是居留的（inhabited），那么它们的积类型也是居留的：

instance [Inhabited α] [Inhabited β] : Inhabited (α × β) where
default := (default, default)

将其添加到之前的实例声明后，类型类实例可以推断出，例如，Nat × Bool 的一个默认元素：

namespace Ex
class Inhabited (α : Type u) where
default : α
instance : Inhabited Bool where
default := true
instance : Inhabited Nat where
default := 0
opaque default [Inhabited α] : α :=
Inhabited.default

instance [Inhabited α] [Inhabited β] : Inhabited (α × β) where
default := (default, default)

(0, true)#eval (default : Nat × Bool)

(0, true)

end Ex

类似地，我们可以用合适的常量函数来居留函数类型（function type）：

instance [Inhabited β] : Inhabited (α → β) where
default := fun _ => default

作为练习，尝试为其他类型定义默认实例，例如 List 和 Sum 类型。

Lean 标准库包含定义 inferInstance。它的类型为 {α : Sort u} → [i : α] → α，并且在期望类型是一个实例时，用于触发类型类解析过程。

inferInstance : Inhabited Nat#check (inferInstance : Inhabited Nat)

inferInstance : Inhabited Nat

def foo : Inhabited (Nat × Nat) :=
inferInstance

theorem ex : foo.default = (default, default) :=
rfl

你可以使用命令 #print 来检查 inferInstance 是多么简单。

@[reducible] def inferInstance.{u} : {α : Sort u} → [i : α] → α :=
fun {α} [i : α] => i#print inferInstance

@[reducible] def inferInstance.{u} : {α : Sort u} → [i : α] → α :=
fun {α} [i : α] => i

10.2. ToString10.2. ToString🔗

多态方法 toString 的类型为 {α : Type u} → [ToString α] → α → String。你为你自己的类型实现实例并使用链接（chaining）将复杂值转换为字符串。Lean 为大多数内置类型提供了 ToString 实例。

structure Person where
name : String
age : Nat

instance : ToString Person where
toString p := p.name ++ "@" ++ toString p.age

"Leo@542"#eval toString { name := "Leo", age := 542 : Person }

"Leo@542"

"(Daniel@18, hello)"#eval toString ({ name := "Daniel", age := 18 : Person }, "hello")

"(Daniel@18, hello)"

10.3. 数字字面量（Numerals）10.3. Numerals🔗

数字字面量在 Lean 中是多态的。你可以使用一个数字字面量（例如 2）来表示任何实现了类型类 OfNat 的类型的元素。

structure Rational where
num : Int
den : Nat
inv : den ≠ 0

instance : OfNat Rational n where
ofNat := { num := n, den := 1, inv := byn:Nat⊢ 1 ≠ 0 decideAll goals completed! 🐙 }

instance : ToString Rational where
toString r := s!"{r.num}/{r.den}"

2/1#eval (2 : Rational)

2/1

2 : Rational#check (2 : Rational)

2 : Rational

2 : Nat#check (2 : Nat)

2 : Nat

Lean 将项 (2 : Nat) 和 (2 : Rational) 分别精化为@OfNat.ofNat Nat 2 (@instOfNatNat 2) 和@OfNat.ofNat Rational 2 (@instOfNatRational 2)。我们说出现在精化后的项中的数字字面量 2 是原始（raw）自然数。你可以使用宏 nat_lit 2 输入原始自然数 2。

2 : Nat#check nat_lit 2

2 : Nat

原始自然数（Raw natural numbers）不是多态的。

OfNat 实例是参数化于数字字面量本身的。因此，你可以为特定的数字字面量定义实例。第二个参数通常是一个变量，如上面的例子所示，或者是一个原始（raw）自然数。

class Monoid (α : Type u) where
unit : α
op : α → α → α
instance [s : Monoid α] : OfNat α (nat_lit 1) where
ofNat := s.unit
def getUnit [Monoid α] : α :=
1

10.4. 输出参数（Output Parameters）10.4. Output Parameters🔗

默认情况下，Lean 仅在项 T 已知且不包含缺失部分时尝试合成实例 Inhabited T。以下命令会产生错误typeclass instance problem is stuck, it is often due to metavariables，因为该类型有一个缺失部分（即 _）。

/--
error: typeclass instance problem is stuck, it is often due to metavariables
  Inhabited (Nat × ?m.2)
-/
#guard_msgs (error) in
#eval (inferInstance : Inhabited (Nat × _))

你可以将类型类 Inhabited 的参数视为类型类合成器的输入（input）值。当一个类型类有多个参数时，你可以将其中一些标记为输出参数（output parameters）。即使这些参数有缺失部分，Lean 也会启动类型类合成器。在下面的例子中，我们使用输出参数来定义一个异质（heterogeneous）多态乘法。

namespace Ex

class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
hMul : α → β → γ

export HMul (hMul)

instance : HMul Nat Nat Nat where
hMul := Nat.mul

instance : HMul Nat (Array Nat) (Array Nat) where
hMul a bs := bs.map (fun b => hMul a b)

12#eval hMul 4 3

#[8, 12, 16]#eval hMul 4 #[2, 3, 4]

#[8, 12, 16]

end Ex

参数 α 和 β 被视为输入参数（input parameters），而 γ 是输出参数（output parameter）。给定一个应用 hMul a b，在 a 和 b 的类型已知后，类型类合成器被调用，结果的类型从输出参数 γ 中获得。在上面的例子中，我们定义了两个实例。第一个是自然数的同质（homogeneous）乘法。第二个是数组的标量乘法。注意你可以链接实例并对第二个实例进行泛化。

namespace Ex

class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
hMul : α → β → γ

export HMul (hMul)

instance : HMul Nat Nat Nat where
hMul := Nat.mul

instance : HMul Int Int Int where
hMul := Int.mul

instance [HMul α β γ] : HMul α (Array β) (Array γ) where
hMul a bs := bs.map (fun b => hMul a b)

12#eval hMul 4 3

#[8, 12, 16]#eval hMul 4 #[2, 3, 4]

#[8, 12, 16]

#[-6, 2, -8]#eval hMul (-2) #[3, -1, 4]

#[-6, 2, -8]

#[#[4, 6], #[0, 8]]#eval hMul 2 #[#[2, 3], #[0, 4]]

#[#[4, 6], #[0, 8]]

end Ex

只要你有实例 HMul α β γ，你就可以在我们的新标量数组乘法实例上用于类型为 Array β 的数组和类型为 α 的标量。在最后一个 #eval 中，注意该实例在数组的数组上被使用了两次。

输出参数在实例合成（instance synthesis）期间被忽略。即使在实例合成发生的上下文中输出参数的值已经被确定，它们的值也会被忽略。一旦使用其输入参数找到了一个实例，Lean 确保输出参数已经已知的值与找到的值匹配。

Lean 还提供了半输出参数（semi-output parameters），它们兼具输入参数的某些特征和输出参数的某些特征。与输入参数一样，半输出参数在选择实例时被考虑。与输出参数一样，它们可用于实例化未知的值。然而，它们并非唯一地这样做。使用半输出参数的实例合成可能更难以预测，因为考虑实例的顺序可以决定选择哪一个实例，但它也更加灵活。

10.5. 默认实例（Default Instances）10.5. Default Instances🔗

在类 HMul 中，参数 α 和 β 被视为输入值。因此，类型类合成只在这两个类型已知后才开始。这通常可能过于严格。

namespace Ex

class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
hMul : α → β → γ

export HMul (hMul)

instance : HMul Int Int Int where
hMul := Int.mul

def xs : List Int := [1, 2, 3]

/--
error: typeclass instance problem is stuck
  HMul Int ?m.2 (?m.11 y)

Note: Lean will not try to resolve this typeclass instance problem because the second type argument to `HMul` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.

Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
-/
#guard_msgs (error) in
#eval fun y => xs.map (fun x => hMul x y)

end Ex

Lean 不会合成实例 HMul，因为 y 的类型尚未提供。然而，在这种情况下，很自然地假设 y 的类型与 x 的类型相同。我们可以通过默认实例（default instances）来实现这一点。

namespace Ex

class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
hMul : α → β → γ

export HMul (hMul)

@[default_instance]
instance : HMul Int Int Int where
hMul := Int.mul

def xs : List Int := [1, 2, 3]

fun y => List.map (fun x => hMul x y) xs : Int → List Int#check fun y => xs.map (fun x => hMul x y)

fun y => List.map (fun x => hMul x y) xs : Int → List Int

end Ex

通过用属性 [default_instance] 标记上面的实例，我们指示 Lean在未决的类型类合成问题上使用此实例。实际的 Lean 实现为算术运算符定义了同质和异质类。此外，a + b、a * b、a - b、a / b 和 a % b 是异质版本的记号。实例 OfNat Nat n 是 OfNat 类的默认实例（优先级为 100）。这就是为什么当期望类型未知时，数字字面量2 的类型为 Nat。你可以定义具有更高优先级的默认实例来覆盖内置实例。

structure Rational where
num : Int
den : Nat
inv : den ≠ 0

@[default_instance 200]
instance : OfNat Rational n where
ofNat := { num := n, den := 1, inv := byn:Nat⊢ 1 ≠ 0 decideAll goals completed! 🐙 }

instance : ToString Rational where
toString r := s!"{r.num}/{r.den}"

2 : Rational#check 2

2 : Rational

优先级对于控制不同默认实例之间的交互也很有用。例如，假设 xs 的类型为 List α。在精化 xs.map (fun x => 2 * x) 时，我们希望乘法的同质实例比 OfNat α 2 的默认实例具有更高的优先级。当我们只实现了实例HMul α α α 而没有实现 HMul Nat α α 时，这一点尤其重要。现在，我们揭示记号 a * b 在 Lean 中是如何定义的。

namespace Ex

class OfNat (α : Type u) (n : Nat) where
ofNat : α

@[default_instance]
instance (n : Nat) : OfNat Nat n where
ofNat := n

class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
hMul : α → β → γ

class Mul (α : Type u) where
mul : α → α → α

@[default_instance 10]
instance [Mul α] : HMul α α α where
hMul a b := Mul.mul a b

infixl:70 " * " => HMul.hMul

end Ex

Mul 类对于仅实现同质乘法的类型很方便。

10.6. 局部实例（Local Instances）10.6. Local Instances🔗

类型类在 Lean 中是使用属性（attributes）实现的。因此，你可以使用 local 修饰符来指示它们仅在当前 section 或 namespace 关闭之前，或当前文件结束之前有效。

structure Point where
x : Nat
y : Nat
section
local instance : Add Point where
add a b := { x := a.x + b.x, y := a.y + b.y }
def double (p : Point) :=
p + p
end -- instance `Add Point` is not active anymore

/--
error: failed to synthesize
  HAdd Point Point ?m.5

Hint: Additional diagnostic information may be available using
the `set_option diagnostics true` command.
-/
#guard_msgs in
def triple (p : Point) :=
p + p + p

你也可以使用 attribute 命令临时禁用一个实例，直到当前 section 或 namespace 关闭，或当前文件结束。

structure Point where
x : Nat
y : Nat
instance addPoint : Add Point where
add a b := { x := a.x + b.x, y := a.y + b.y }
def double (p : Point) :=
p + p
attribute [-instance] addPoint
/--
error: failed to synthesize
  HAdd Point Point ?m.5

Hint: Additional diagnostic information may be available using
the `set_option diagnostics true` command.
-/
#guard_msgs in
def triple (p : Point) :=
p + p + p  -- Error: failed to synthesize instance

我们建议你仅使用此命令来诊断问题。

10.7. 作用域实例（Scoped Instances）10.7. Scoped Instances🔗

你也可以在命名空间（namespace）中声明作用域实例（scoped instances）。这种实例仅当你位于该命名空间内部或打开该命名空间时才生效。

structure Point where
x : Nat
y : Nat

namespace Point

scoped instance : Add Point where
add a b := { x := a.x + b.x, y := a.y + b.y }

def double (p : Point) :=
p + p

end Point

-- instance `Add Point` is not active anymore

/--
error: failed to synthesize
  HAdd Point Point ?m.3

Hint: Additional diagnostic information may be available using
the `set_option diagnostics true` command.
-/
#guard_msgs (error) in
fun p => sorry : (p : Point) → ?m.6 p#check fun (p : Point) => p + p + p

fun p => sorry : (p : Point) → ?m.6 p

namespace Point

-- instance `Add Point` is active again
fun p => p + p + p : Point → Point#check fun (p : Point) => p + p + p

fun p => p + p + p : Point → Point

end Point

open Point -- activates instance `Add Point`

fun p => p + p + p : Point → Point#check fun (p : Point) => p + p + p

fun p => p + p + p : Point → Point

你可以使用命令 open scoped <namespace> 来激活作用域属性，但不会"打开"命名空间中的名称。

structure Point where
x : Nat
y : Nat

namespace Point

scoped instance : Add Point where
add a b := { x := a.x + b.x, y := a.y + b.y }

def double (p : Point) :=
p + p

end Point

open scoped Point -- activates instance `Add Point`

fun p => p + p + p : Point → Point#check fun (p : Point) => p + p + p

fun p => p + p + p : Point → Point

/--
error: Unknown identifier `double`
-/
#guard_msgs (error) in
fun p => sorry : (p : Point) → ?m.2 p#check fun (p : Point) => double p

fun p => sorry : (p : Point) → ?m.2 p

10.8. 可判定命题（Decidable Propositions）10.8. Decidable Propositions🔗

让我们考虑标准库中定义的另一个类型类示例，即 Decidable类型类。粗略地说，Prop 的一个元素被称为可判定的（decidable），如果我们可以判定它是真还是假。这个区分仅在构造性数学中有用；在经典数学中，每个命题都是可判定的。但如果使用经典原理，例如，通过情况分析来定义一个函数，该函数将不是可计算的。从算法上讲，Decidable 类型类可以用于推断一个能有效确定该命题是否为真的过程。因此，该类型类在支持这种计算性定义（当它们可能时）的同时，也允许平滑地过渡到使用经典定义和经典推理。

在标准库中，Decidable 被形式化地定义如下：

namespace Hidden

class inductive Decidable (p : Prop) where
| isFalse (h : ¬p) : Decidable p
| isTrue (h : p) : Decidable p

end Hidden

从逻辑上讲，拥有一个元素 t : Decidable p 比拥有一个元素 t' : p ∨ ¬p 更强；它使我们能够根据 p 的真值来定义任意类型的值。例如，对于表达式 if p then a else b 有意义，我们需要知道 p 是可判定的。该表达式是ite p a b 的语法糖，其中 ite 的定义如下：

namespace Hidden

def ite {α : Sort u}
(c : Prop) [h : Decidable c]
(t e : α) : α :=
h.casesOn (motive := fun _ => α) (fun _ => e) (fun _ => t)

end Hidden

标准库还包含 ite 的一个变体，称为 dite，即依赖的 if-then-else 表达式。它的定义如下：

namespace Hidden

def dite {α : Sort u}
(c : Prop) [h : Decidable c]
(t : c → α) (e : Not c → α) : α :=
Decidable.casesOn (motive := fun _ => α) h e t

end Hidden

也就是说，在 dite c t e 中，我们可以在"then"分支中假设 hc : c，在"else"分支中假设 hnc : ¬c。为了使 dite 更方便使用，Lean 允许我们写 if h : c then t else e来代替 dite c (fun h : c => t h) (fun h : ¬c => e h<...}

没有经典逻辑，我们不能证明每个命题都是可判定的。但我们可以证明某些命题是可判定的。例如，我们可以证明自然数和整数上的基本操作（如相等和比较）的可判定性。此外，可判定性在命题联结词下保持封闭：

@instDecidableAnd : {p q : Prop} → [dp : Decidable p] → [dq : Decidable q] → Decidable (p ∧ q)#check @instDecidableAnd

@instDecidableAnd : {p q : Prop} → [dp : Decidable p] → [dq : Decidable q] → Decidable (p ∧ q)

@instDecidableOr : {p q : Prop} → [dp : Decidable p] → [dq : Decidable q] → Decidable (p ∨ q)#check @instDecidableOr

@instDecidableOr : {p q : Prop} → [dp : Decidable p] → [dq : Decidable q] → Decidable (p ∨ q)

@instDecidableNot : {p : Prop} → [dp : Decidable p] → Decidable ¬p#check @instDecidableNot

@instDecidableNot : {p : Prop} → [dp : Decidable p] → Decidable ¬p

因此，我们可以对自然数上的可判定谓词进行按情况定义：

def step (a b x : Nat) : Nat :=
if x < a ∨ x > b then 0 else 1

set_option pp.explicit true

def step : Nat → Nat → Nat → Nat :=
fun a b x =>
@ite Nat (Or (@LT.lt Nat instLTNat x a) (@GT.gt Nat instLTNat x b))
(@instDecidableOr (@LT.lt Nat instLTNat x a) (@GT.gt Nat instLTNat x b) (Nat.decLt x a) (Nat.decLt b x))
(@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0))) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))#print step

def step : Nat → Nat → Nat → Nat :=
fun a b x =>
  @ite Nat (Or (@LT.lt Nat instLTNat x a) (@GT.gt Nat instLTNat x b))
    (@instDecidableOr (@LT.lt Nat instLTNat x a) (@GT.gt Nat instLTNat x b) (Nat.decLt x a) (Nat.decLt b x))
    (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0))) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))

打开隐式参数显示，精化器已经推断出命题 x < a ∨ x > b 的可判定性，仅仅是通过应用适当的实例。

使用经典公理，我们可以证明每个命题都是可判定的。你可以导入经典公理并通过打开 Classical 命名空间使可判定性的通用实例可用。

open Classical

此后，Decidable p 对于每个 p 都有一个实例。因此，库中所有依赖于可判定性假设的定理在你想要进行经典推理时都可以自由使用。在 Axioms and Computation 中，我们将看到，使用排中律来定义函数可能会阻止它们被计算性地使用。因此，标准库为 propDecidable 实例分配了一个低优先级。

namespace Hidden

open Classical

noncomputable scoped
instance (priority := low) propDecidable (a : Prop) : Decidable a :=
choice <| match em a with
| Or.inl h => ⟨isTrue h⟩
| Or.inr h => ⟨isFalse h⟩

end Hidden

这保证了 Lean 会优先选择其他实例，只在其他尝试推断可判定性失败后才回退到 propDecidable。

Decidable 类型类还提供了一点小规模的自动化来证明定理。标准库引入了策略（tactic）decide，它使用 Decidable 实例来求解简单目标，以及一个函数 decide，它使用 Decidable 实例来计算对应的 Bool。

example : 10 < 5 ∨ 1 > 0 := by⊢ 10 < 5 ∨ 1 > 0
decideAll goals completed! 🐙

example : ¬(True ∧ False) := by⊢ ¬(True ∧ False)
decideAll goals completed! 🐙

example : 10 * 20 = 200 := by⊢ 10 * 20 = 200
decideAll goals completed! 🐙

theorem ex : True ∧ 2 = 1 + 1 := by⊢ True ∧ 2 = 1 + 1
decideAll goals completed! 🐙

theorem ex : True ∧ 2 = 1 + 1 :=
of_decide_eq_true (id (Eq.refl true))#print ex

theorem ex : True ∧ 2 = 1 + 1 :=
of_decide_eq_true (id (Eq.refl true))

@of_decide_eq_true : ∀ {p : Prop} [inst : Decidable p], decide p = true → p#check @of_decide_eq_true

@of_decide_eq_true : ∀ {p : Prop} [inst : Decidable p], decide p = true → p

decide : (p : Prop) → [h : Decidable p] → Bool#check @decide

decide : (p : Prop) → [h : Decidable p] → Bool

它们的工作原理如下。表达式 decide p 尝试推断p 的一个判定过程，如果成功，则求值为 true 或 false。特别地，如果 p 是一个真的封闭表达式，decide p 会定义性地归约到布尔值 true。在假设 decide p = true 成立的情况下，of_decide_eq_true生成一个 p 的证明。策略 decide 将这一切整合起来以证明目标 p。根据先前的观察，decide 将在推断出的 p 的判定过程有足够信息定义性地求值为isTrue 情况时成功。

10.9. 管理类型类推断（Managing Type Class Inference）10.9. Managing Type Class Inference🔗

如果你在需要提供一个 Lean 可以通过类型类推断推断出的表达式的情况下，你可以要求 Lean 使用 inferInstance 执行推断：

def foo : Add Nat := inferInstance

def bar : Inhabited (Nat → Nat) := inferInstance

@inferInstance : {α : Sort u_1} → [i : α] → α#check @inferInstance

@inferInstance : {α : Sort u_1} → [i : α] → α

事实上，你可以使用 Lean 的 (t : T) 记号来以简洁的方式指定你要查找其实例的类：

inferInstance : Add Nat#check (inferInstance : Add Nat)

inferInstance : Add Nat

你也可以使用辅助定义 inferInstanceAs：

inferInstanceAs (Add Nat) : Add Nat#check inferInstanceAs (Add Nat)

inferInstanceAs (Add Nat) : Add Nat

inferInstanceAs : (α : Sort u_1) → [i : α] → α#check @inferInstanceAs

inferInstanceAs : (α : Sort u_1) → [i : α] → α

有时 Lean 找不到一个实例，因为该类隐藏在一个定义之下。例如，Lean 无法找到 Inhabited (Set α) 的一个实例。我们可以显式地声明一个：

def Set (α : Type u) := α → Prop
/--
error: failed to synthesize
  Inhabited (Set α)

Hint: Additional diagnostic information may be available using
the `set_option diagnostics true` command.
-/
#guard_msgs in
example : Inhabited (Set α) :=
inferInstance
instance : Inhabited (Set α) :=
inferInstanceAs (Inhabited (α → Prop))

有时，你可能会发现类型类推断未能找到预期的实例，或者更糟，陷入无限循环并超时。为了帮助在这些情况下进行调试，Lean 允许你请求搜索的跟踪信息：

set_option trace.Meta.synthInstance true

如果你使用 VS Code，你可以通过将鼠标悬停在相关的定理或定义上，或者按 CtrlShiftEnter 打开消息窗口来读取结果。

你也可以使用以下选项来限制搜索：

set_option synthInstance.maxHeartbeats 10000
set_option synthInstance.maxSize 400

选项 synthInstance.maxHeartbeats 指定每个类型类解析问题的最大心跳数。心跳是（小的）内存分配数（以千计），0 表示没有限制。选项 synthInstance.maxSize 是在类型类实例合成过程中用于构建解决方案的最大实例数。

还要记住，在 VS Code 和 Emacs 编辑器模式中，Tab 补全在 set_option 中都可以工作，以帮助你找到合适的选项。

如上所述，给定上下文中的类型类实例表示一个类似 Prolog 的程序，它产生一个回溯搜索。程序的效率和找到的解决方案都可能取决于系统尝试实例的顺序。最后声明的实例最先被尝试。此外，如果实例在其他模块中声明，尝试它们的顺序取决于命名空间被打开的顺序。在较晚打开的命名空间中声明的实例会被较早尝试。

你可以通过为类型类实例分配优先级（priority）来改变它们被尝试的顺序。在声明一个实例时，它被分配一个默认优先级值。你可以在定义实例时分配其他优先级。以下示例说明了如何完成：

class Foo where
a : Nat
b : Nat
instance (priority := default + 1) i1 : Foo where
a := 1
b := 1
instance i2 : Foo where
a := 2
b := 2
example : Foo.a = 1 :=
rfl
instance (priority := default + 2) i3 : Foo where
a := 3
b := 3
example : Foo.a = 3 :=
rfl

10.10. 使用类型类的强制类型转换（Coercions using Type Classes）10.10. Coercions using Type Classes🔗

最基本的强制类型转换类型将一种类型的元素映射到另一种类型。例如，从 Nat 到 Int 的强制类型转换允许我们将 n : Nat 的任何元素视为 Int 的一个元素。但有些强制类型转换依赖于参数；例如，对于任何类型 α，我们可以将 as : List α 的任何元素视为 Array α 的一个元素。这些被称为依赖（dependent）强制类型转换。使用类型类来管理强制类型转换非常优雅。

Lean 允许我们声明三种强制类型转换：

从一个类型族到另一个类型族
从一个类型族到 sort 类
从一个类型族到函数类型类

第一种强制类型转换允许我们将源族中某个成员的任意元素视为目标族中相应成员的元素。第二种强制类型转换允许我们将源族中某个成员的任意元素视为一个类型。第三种强制类型转换允许我们将源族中的任意元素视为一个函数。让我们依次考虑每一种。

在 Lean 中，强制类型转换是基于类型类解析框架实现的。我们通过声明一个 Coe α β 的实例来定义从 α 到 β 的强制类型转换。例如，我们可以按如下方式定义从 Bool 到 Prop 的强制类型转换：

instance : Coe Bool Prop where
coe b := b = true

这使我们能够在 if-then-else 表达式中使用布尔项：

5#eval if true then 5 else 3

3#eval if false then 5 else 3

我们可以按如下方式定义从 List α 到 Set α 的强制类型转换：

def Set (α : Type u) := α → Prop
def Set.empty {α : Type u} : Set α := fun _ => False
def Set.mem (a : α) (s : Set α) : Prop := s a
def Set.singleton (a : α) : Set α := fun x => x = a
def Set.union (a b : Set α) : Set α := fun x => a x ∨ b x
notation "{ " a " }" => Set.singleton a
infix:55 " ∪ " => Set.union

def List.toSet : List α → Set α
| [] => Set.empty
| a::as => {a} ∪ as.toSet

instance : Coe (List α) (Set α) where
coe a := a.toSet

def s : Set Nat := {1}

s ∪ [2, 3].toSet : Set Nat#check s ∪ [2, 3]

s ∪ [2, 3].toSet : Set Nat

我们可以使用记号 ↑ 来强制在特定位置引入一个强制类型转换。这也有助于使我们的意图清晰，并绕过强制类型转换解析系统的限制。

def Set (α : Type u) := α → Prop
def Set.empty {α : Type u} : Set α := fun _ => False
def Set.mem (a : α) (s : Set α) : Prop := s a
def Set.singleton (a : α) : Set α := fun x => x = a
def Set.union (a b : Set α) : Set α := fun x => a x ∨ b x
notation "{ " a " }" => Set.singleton a
infix:55 " ∪ " => Set.union
def List.toSet : List α → Set α
| [] => Set.empty
| a::as => {a} ∪ as.toSet
instance : Coe (List α) (Set α) where
coe a := a.toSet

def s : Set Nat := {1}

let x := [2, 3].toSet;
s ∪ x : Set Nat#check let x := ↑[2, 3]; s ∪ x

let x := [2, 3].toSet;
s ∪ x : Set Nat

let x := [2, 3];
s ∪ x.toSet : Set Nat#check let x := [2, 3]; s ∪ x

let x := [2, 3];
s ∪ x.toSet : Set Nat

Lean 还通过类型类 CoeDep 支持依赖强制类型转换。例如，我们不能将任意命题强制转换为 Bool，只能强制转换那些实现了 Decidable 类型类的命题。

instance (p : Prop) [Decidable p] : CoeDep Prop p Bool where
coe := decide p

Lean 还会根据需要链接（非依赖的）强制类型转换。实际上，类型类 CoeT 是 Coe 的传递闭包。

现在让我们考虑第二种强制类型转换。通过sort 类，我们指宇宙（universe）的集合 Type u。第二种强制类型转换的形式是：

    c : (x1 : A1) → ... → (xn : An) → F x1 ... xn → Type u

其中 F 是一个类型族（family of types），如上所述。这允许我们在 t 的类型为 F a₁ ... aₙ 时写 s : t。换句话说，该强制类型转换允许我们将 F a₁ ... aₙ 的元素视为类型。这在定义代数结构时非常有用，因为其中一个组件——结构的载体（carrier）——是一个 Type。例如，我们可以按如下方式定义一个半群（semigroup）：

structure Semigroup where
carrier : Type u
mul : carrier → carrier → carrier
mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)
instance (S : Semigroup) : Mul S.carrier where
mul a b := S.mul a b

换句话说，一个半群由一个类型 carrier 和一个乘法 mul 组成，并且该乘法满足结合律。instance 命令允许我们在拥有 a b : S 时写 a * b 来代替 Semigroup.mul S a b。

structure Semigroup where
carrier : Type u
mul : carrier → carrier → carrier
mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)
instance (S : Semigroup) : Mul S.carrier where
mul a b := S.mul a b

Semigroup.carrier.{u} (self : Semigroup) : Type u#check Semigroup.carrier

Semigroup.carrier.{u} (self : Semigroup) : Type u

如果我们声明这个函数为一个强制类型转换，那么每当我们有一个半群 S : Semigroup 时，我们可以写 a : S 来代替 a : S.carrier：

structure Semigroup where
carrier : Type u
mul : carrier → carrier → carrier
mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)
instance (S : Semigroup) : Mul S.carrier where
mul a b := S.mul a b

instance : CoeSort Semigroup (Type u) where
coe s := s.carrier

example (S : Semigroup) (a b c : S) : (a * b) * c = a * (b * c) :=
Semigroup.mul_assoc _ a b c

正是这种强制类型转换使得写 (a b c : S) 成为可能。注意，我们定义了 CoeSort Semigroup (Type u) 的实例而不是 Coe Semigroup (Type u) 的实例。

通过函数类型类，我们指 Pi 类型（Pi types）的集合 (z : B) → C。第三种强制类型转换的形式是：

    c : (x₁ : A₁) → ... → (xₙ : Aₙ) → (y : F x₁ ... xₙ) → (z : B) → C

其中 F 再次是一个类型族，B 和 C 可以依赖于 x₁, ..., xₙ, y。这使得当 t 是 F a₁ ... aₙ 的一个元素时可以写 t s。换句话说，该强制类型转换使我们能够将 F a₁ ... aₙ 的元素视为函数。延续上面的例子，我们可以定义半群 S1 和 S2 之间的态射（morphism）的概念。也就是说，一个从 S1 的载体到 S2 的载体的函数（注意隐式强制类型转换），并且该函数保持乘法。投影 Morphism.mor 将一个态射映射到底层函数：

structure Semigroup where
carrier : Type u
mul : carrier → carrier → carrier
mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)
instance (S : Semigroup) : Mul S.carrier where
mul a b := S.mul a b
instance : CoeSort Semigroup (Type u) where
coe s := s.carrier

structure Morphism (S1 S2 : Semigroup) where
mor : S1 → S2
resp_mul : ∀ a b : S1, mor (a * b) = (mor a) * (mor b)

@Morphism.mor : {S1 : Semigroup} → {S2 : Semigroup} → Morphism S1 S2 → S1.carrier → S2.carrier#check @Morphism.mor

@Morphism.mor : {S1 : Semigroup} → {S2 : Semigroup} → Morphism S1 S2 → S1.carrier → S2.carrier

因此，它是第三种强制类型转换的主要候选者。

structure Semigroup where
carrier : Type u
mul : carrier → carrier → carrier
mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)
instance (S : Semigroup) : Mul S.carrier where
mul a b := S.mul a b
instance : CoeSort Semigroup (Type u) where
coe s := s.carrier
structure Morphism (S1 S2 : Semigroup) where
mor : S1 → S2
resp_mul : ∀ a b : S1, mor (a * b) = (mor a) * (mor b)

instance (S1 S2 : Semigroup) :
CoeFun (Morphism S1 S2) (fun _ => S1 → S2) where
coe m := m.mor

theorem resp_mul {S1 S2 : Semigroup} (f : Morphism S1 S2) (a b : S1)
: f (a * b) = f a * f b :=
f.resp_mul a b

example (S1 S2 : Semigroup) (f : Morphism S1 S2) (a : S1) :
f (a * a * a) = f a * f a * f a :=
calc f (a * a * a)
_ = f (a * a) * f a := byS1:SemigroupS2:Semigroupf:Morphism S1 S2a:S1.carrier⊢ f.mor (a * a * a) = f.mor (a * a) * f.mor a rw [resp_mul f]All goals completed! 🐙
_ = f a * f a * f a := byS1:SemigroupS2:Semigroupf:Morphism S1 S2a:S1.carrier⊢ f.mor (a * a) * f.mor a = f.mor a * f.mor a * f.mor a rw [resp_mul f]All goals completed! 🐙

有了强制类型转换后，我们可以写 f (a * a * a) 来代替 f.mor (a * a * a)。