10. 类型类🔗

类型类（Type Class）作为一种原则性方法引入，是为了在函数式编程语言中支持特设多态（Ad-hoc Polymorphism）。我们首先观察到，如果函数简单地接受特定类型的实现作为参数，然后在其余参数上调用该实现，则很容易实现特设多态函数（如加法）。例如，假设我们在 Lean 中声明一个结构体来保存加法的实现：

namespace Ex

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

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

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

end Ex

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

namespace Ex

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

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

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

end Ex

其中方括号表示类型为 Add α 的参数是 实例隐式的 ，即，它应该使用类型类解析合成。这个版本的 add 是 Haskell 项 add :: Add a => a -> a -> a 的 Lean 类比。同样，我们可以通过以下方式注册实例：

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

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

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 的记法。

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

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. 链接实例🔗

以类型类推断的层面来看，它并不那么令人印象深刻；它不过是一种为精细器存储实例列表的机制，用于在查询表中查找。类型类推断变得强大的原因在于，它能够“链接（Chain）”实例。也就是说，实例声明本身可以依赖类型类的隐式实例。这导致类推断递归地通过实例进行链接，并在必要时回溯，就像 Prolog 中的搜索一样。

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

与此类似，我们可以使用合适的常量函数使其居留到类型函数中：

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

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

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

inferInstance : Inhabited Nat

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

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

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

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

10.2. 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. 数值🔗

数值在 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

2 : Nat#check nat_lit 2

2 : Nat

原始自然数不是多态的。

OfNat 实例对数值进行了参数化，因此你可以定义特定数字的实例。第二个参数通常是变量，如上例所示，或者是一个原始自然数。

                class Monoid (α : Type u) where
  unit : α
  op   : α → α → α

instance [s : Monoid α] : OfNat α (nat_lit 1) where
  ofNat := s.unit

def getUnit [Monoid α] : α :=
  1

10.4. 输出参数🔗

/--
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 的参数视为类型类合成器的输入值。当类型类有多个参数时，可以将其中一些标记为 输出参数 （Output Parameter）。即使这些参数有缺失部分，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

参数 α 和 β 会被视为输入参数，γ 被视为输出参数。如果给定一个应用 hMul a b，那么在知道 a 和 b 的类型后，将调用类型类合成器，并且可以从输出参数 γ 中获得最终的类型。在上文中的示例中，我们定义了两个实例。第一个实例是针对自然数的同质乘法。第二个实例是针对数组的标量乘法。请注意，你可以链接实例，并推广第二个实例。

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 中，请注意该实例曾在数组数组中使用了两次。

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

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

10.5. 默认实例🔗

在类 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

实例 HMul 没有被 Lean 合成，因为没有提供 y 的类型。然而，在这种情况下，自然应该认为 y 和 x 的类型应该相同。我们可以使用 默认实例 来实现这一点。

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

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

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. 局部实例🔗

类型类是使用 Lean 中的属性（Attribute）来实现的。因此，你可以使用 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. 作用域实例🔗

你可以在命名空间中声明作用域实例。这种类型的实例只在你进入命名空间或打开命名空间时激活。

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 类型类。粗略地讲，对于 Prop 的一个元素，如果我们可以判定它是真或假，它就被称为可判定的。这种区别只有在构造性数学中才有用；在经典数学中，每个命题都是可判定的。但如果我们使用经典原则，比如通过情况来定义一个函数，那么这个函数将不可计算。从算法上来讲，Decidable 类型类可以用来推导出一个过程，它能有效判定命题是否为真。因此，该类型类支持这样的计算性定义（如果它们是可能的），同时还允许平滑地过渡到经典定义和经典推理的使用。

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

namespace Hidden

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

end Hidden

namespace Hidden

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

end Hidden

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

如果没有经典逻辑，我们就不能证明每个命题都是可判定的。但我们可以证明某些命题是可判定的。例如，我们可以证明基本运算（比如自然数和整数上的等式和比较）的可判定性。此外，命题连词下的可判定性被保留了下来：

@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)))

打开隐式参数显示，阐释器（Elaborator）已经通过应用适当的实例推导出了命题 x < a ∨ x > b 的可判定性。

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

open Classical

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 类型类还为证明定理提供了一些小规模的自动化。标准库引入了 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

10.9. 管理类型类推导🔗

如果你遇到需要提供一个 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 : α] → α

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 : α] → α

                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 的程序，它会引起回溯搜索。程序的效率和找到的解决方案都取决于系统尝试实例的顺序。最后声明的实例最先被尝试。此外，如果实例是在其他模块中声明的，则尝试它们的顺序取决于打开命名空间的顺序。在较晚打开的命名空间中声明的实例会较早被尝试。

你可以通过为类型类实例分配 优先级 来更改尝试它们的顺序。声明实例时，会为其分配默认优先级值。定义实例时，你可以分配其他优先级。以下示例说明了如何执行此操作：

                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. 使用类型类的强制转换🔗

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

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 类，我们指的是宇宙集合 Type u。第二种强制转换的形式如下：

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

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

                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

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

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

所谓 函数类型类，我们指的是 Pi 类型 (z : B) → C 的集合。第三种强制转换的形式如下：

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

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)。当在需要函数的地方使用 Morphism f 时，Lean 会插入强制转换。与 CoeSort 类似，我们还有另一个类 CoeFun 用于此类强制转换。参数 γ 用于指定我们要强制转换到的函数类型。该类型可能取决于我们要强制转换的类型。