类型类

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

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

#check @Add.add
-- Add.add : {a : Type} → Add a → a → a → a
end Ex

在上面 Lean 代码中，字段 add 的类型为 Add.add : {a : Type} → Add a → a → a → a 其中类型 a 周围的大括号表示它是一个隐式参数。我们可以通过以下方式实现 double：

namespace Ex
structure Add (a : Type) where
 add : a → a → a
def double (s : Add a) (x : a) : a :=
  s.add x x

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

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

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

注意，你可以用 double { add := Nat.add } n 使一个自然数 n 翻倍。当然，以这种方式让用户手动四处传递实现会非常繁琐。实际上，这会消除掉特设多态的大部分潜在好处。

类型类的主要思想是使诸如 Add a 之类的参数变为隐含的，并使用用户定义实例的数据库通过称为类型类解析的过程自动合成所需的实例。在 Lean 中，通过在以上示例中将 structure 更改为 class，Add.add 的类型会变为：

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

#check @Add.add
-- Add.add : {a : Type} → [self : Add a] → a → a → a
end Ex

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

namespace Ex
class Add (a : Type) where
 add : a → a → a
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 的实例。现在，我们可以通过隐式的实例重新实现 double 了：

namespace Ex
class Add (a : Type) where
  add : a → a → a
instance : Add Nat where
 add := Nat.add
instance : Add Int where
 add := Int.add
instance : Add Float where
 add := Float.add
def double [Add a] (x : a) : a :=
  Add.add x x

#check @double
-- @double : {a : Type} → [inst : Add a] → a → a

#eval double 10
-- 20

#eval double (10 : Int)
-- 100

#eval double (7 : Float)
-- 14.000000

#eval double (239.0 + 2)
-- 482.000000

end Ex

一般情况下，实例可能以复杂的方式依赖于其他实例。例如，你可以声明一个（匿名）实例，说明如果 a 存在加法，那么 Array a 也存在加法：

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

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

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

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

上述示例演示了类型类如何用于重载符号。现在，我们探索另一个应用程序。我们经常需要给定类型的任意元素。回想一下类型在 Lean 中可能没有任何元素。我们经常希望在一个「边界情况」下定义返回一个任意元素。例如，我们可能希望当 xs 为 List a 类型时 head xs 表达式的类型为 a。类似地，许多定理在类型不为空的附加假设下成立。例如，如果 a 是一个类型，则 exists x : a, x = x 仅在 a 不为空时为真。标准库定义了一个类型类 Inhabited，它能够让类型类推理来推断 可居（Inhabited） 类型类的「默认」元素。让我们从上述程序的第一步开始，声明一个适当的类：

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

#check @Inhabited.default
-- Inhabited.default : {a : Type u} → [self : Inhabited a] → a
end Ex

注意 Inhabited.default 没有任何显式参数。

类 Inhabited a 的某个元素只是形式为 Inhabited.mk x 的表达式，其中 x : a 为某个元素。投影 Inhabited.default 可让我们从 Inhabited a 的某个元素中「提取」出 a 的某个元素。现在我们用一些实例填充该类：

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

#eval (Inhabited.default : Nat)
-- 0

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

#eval (default : Nat)
-- 0

#eval (default : Bool)
-- true
end Ex

链接实例

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

-->

例如，以下定义展示了若两个类型 a 和 b 包含元素，则二者的积也包含元素：

instance [Inhabited a] [Inhabited b] : Inhabited (a × b) where
  default := (default, default)

将它添加到先前的实例声明后，类型类实例就能推导了，例如 Nat × Bool 的默认元素为：

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

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

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

instance [Inhabited b] : Inhabited (a → b) where
  default := fun _ => default

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

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

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

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

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

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

#print inferInstance

ToString 方法

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

structure Person where
  name : String
  age  : Nat

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

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

数值

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

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

instance : OfNat Rational n where
  ofNat := { num := n, den := 1, inv := by decide }

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

#eval (2 : Rational) -- 2/1

#check (2 : Rational) -- Rational
#check (2 : Nat)      -- Nat

Lean 会将项 (2 : Nat) 和 (2 : Rational) 分别繁饰（Elaborate）为： OfNat.ofNat Nat 2 (instOfNatNat 2) 和 OfNat.ofNat Rational 2 (instOfNatRational 2)。我们将繁饰的项中出现的数字 2 称为原始自然数。你可以使用宏 nat_lit 2 来输入原始自然数 2。

#check nat_lit 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

输出参数

默认情况下，Lean 仅当项 T 已知时且不包含缺失部分时，会尝试合成实例 Inhabited T。以下命令会产生错「typeclass instance problem is stuck, it is often due to metavariables ?m.7 （类型类实例问题卡住了，通常是由于元变量 ?m.7 引起的）」因为该类型有缺失的部分（即 _）。

#check_failure (inferInstance : Inhabited (Nat × _))

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

#eval hMul 4 3           -- 12
#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)

#eval hMul 4 3                    -- 12
#eval hMul 4 #[2, 3, 4]           -- #[8, 12, 16]
#eval hMul (-2) #[3, -1, 4]       -- #[-6, 2, -8]
#eval hMul 2 #[#[2, 3], #[0, 4]]  -- #[#[4, 6], #[0, 8]]
end Ex

当你拥有 HMul α β γ 的实例时，可以在类型为 Array β 的数组上将其使用标量类型 α 的新标量数组乘法实例。在最后的 #eval 中，请注意该实例曾在数组数组中使用了两次。

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, it is often due to metavariables HMul ?m.89 ?m.90 ?m.91"
#check_failure 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]

#check fun y => xs.map (fun x => hMul x y)  -- 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 := by decide }

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

#check 2 -- Rational

优先级也适用于控制不同默认实例之间的交互。例如，假设 xs 有类型 List α。在繁饰 xs.map (fun x => 2 * x) 时，我们希望乘法的同质实例比 OfNat 的默认实例具有更高的优先级。当我们仅实现了实例 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 类是仅实现了同质乘法的类型的简便记法。

局部实例

类型类是使用 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

-- def triple (p : Point) :=
--  p + p + p  -- Error: failed to synthesize instance

你也可使用 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

-- def triple (p : Point) :=
--  p + p + p  -- Error: failed to synthesize instance

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

作用于实例

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

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

-- #check fun (p : Point) => p + p + p  -- Error

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

end Point

open Point -- activates instance `Add Point`
#check fun (p : Point) => p + p + p

你可以使用 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`
#check fun (p : Point) => p + p + p

-- #check fun (p : Point) => double p -- Error: unknown identifier 'double'

可判定的命题

让我们考虑标准库中定义的另一个类型类，名为 Decidable 类型类。粗略地讲，对于 Prop 的一个元素，如果我们可以判定它是真或假，它就被称为可判定的。这种区别只有在构造性数学中才有用；在经典数学中，每个命题都是可判定的。但如果我们使用经典原则，比如通过情况来定义一个函数，那么这个函数将不可计算。从算法上来讲，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 : α) : α :=
  Decidable.casesOn (motive := fun _ => α) h (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 (λ h : c => t) (λ h : ¬ c => e)。

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

#check @instDecidableAnd
  -- {p q : Prop} → [Decidable p] → [Decidable q] → Decidable (And p q)

#check @instDecidableOr
#check @instDecidableNot

因此我们可以按照自然数上的可判定谓词的情况给出定义：

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

set_option pp.explicit true
#print step

打开隐式参数显示，繁饰器已经推断出了命题 x < a ∨ x > b 的可判定性，只需应用适当的实例即可。

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

open Classical

之后 Decidable p 就会拥有任何 p 的实例。因此，当你想进行经典推理时，库中的所有依赖于可判定假设的定理都会免费提供。在公理和计算一章中，我们将看到，使用排中律来定义函数会阻止它们被计算性地使用。因此，标准库将 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 类型类还为定理证明提供了一点小规模的自动化。标准库引入了使用 Decidable 实例解决简单目标的策略 decide。

example : 10 < 5 ∨ 1 > 0 := by
  decide

example : ¬ (True ∧ False) := by
  decide

example : 10 * 20 = 200 := by
  decide

theorem ex : True ∧ 2 = 1+1 := by
  decide

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

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

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

它们的工作方式如下：表达式 decide p 尝试推断 p 的决策过程，如果成功，则会求值为 true 或 false。特别是，如果 p 是一个为真的封闭表达式， decide p 将根据定义化简未为布尔值 true。在假设 decide p = true 成立的情况下，of_decide_eq_true 会生成 p 的证明。策略 decide 将所有这些组合在一起以证明目标 p。根据前面的观察，只要推断出的决策过程拥有足够的信息，可以根据定义将 c 求值为 isTrue 的情况，那么 decide 就会成功。

类型类推断的管理

如果你需要使用类型类推断来提供一个 Lean 可以推断的表达式，那么你可以使用 inferInstance 让 Lean 执行推断：

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

#check @inferInstance
-- {α : Sort u} → [α] → α

你可以使用 Lean 中的 (t : T) 语法指定你正在寻找的类的实例，这是一种很简洁的方式：

#check (inferInstance : Add Nat)

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

#check inferInstanceAs (Add Nat)

#check @inferInstanceAs
-- (α : Sort u) → [α] → α

有时 Lean 会找不到一个实例，因为该类被定义所掩盖。例如，Lean 无法找到 Inhabited (Set α) 的一个实例。我们可以显式地声明一个：

def Set (α : Type u) := α → Prop

-- fails
-- example : Inhabited (Set α) :=
--  inferInstance

instance : Inhabited (Set α) :=
  inferInstanceAs (Inhabited (α → Prop))

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

set_option trace.Meta.synthInstance true

如果你使用的是 VS Code，可以通过将鼠标悬停在相关的定理或定义上，或按 Ctrl-Shift-Enter 打开消息窗口来阅读结果。在 Emacs 中，你可以使用 C-c C-x 在你的文件中运行一个独立的 Lean 进程，并且在每次触发类型类解析过程时，输出缓冲区都会显示一个跟踪。

使用以下选项，你还可以限制搜索：

set_option synthInstance.maxHeartbeats 10000
set_option synthInstance.maxSize 400

选项 synthInstance.maxHeartbeats 指定每个类型类解析问题可能出现的心跳（Heartbeat）次数上限。心跳是（小）内存分配的次数（以千为单位），0 表示没有上限。选项 synthInstance.maxSize 是用于构建类型类实例合成过程中解的实例个数。

另外请记住，在 VS Code 和 Emacs 编辑器模式中，制表符补全也可用于 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

使用类型泛型进行强制转换

最基本的强制转换将一种类型的元素映射到另一种类型。例如，从 Nat 到 Int 的强制转换允许我们将任何元素 n : Nat 视作元素 Int。但一些强制转换依赖于参数；例如，对于任何类型 α，我们可以将任何元素 as : List α 视为 Set α 的元素，即，列表中出现的元素组成的集合。相应的强制转换被定义在 List α 的「类型族（Type Family）」上，由 α 参数化。

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

从一个类型族到另一个类型族
从一个类型族到种类（Sort）的类
从一个类型族到函数类型的类

第一种强制转换允许我们将源类型族任何成员的元素视为目标类型族中对应成员的元素。第二种强制转换允许我们将源类型族任何成员的元素视为类型。第三种强制转换允许我们将源类型族任何成员的元素视为函数。让我们逐一考虑这些。

在 Lean 中，强制转换在类型类解析框架的基础上实现。我们通过声明 Coe α β 的实例，定义从 α 到 β 的强制转换。例如，以下内容可以定义从 Bool 到 Prop 的强制转换：

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

这使得我们可以在 if-then-else 表达式中使用布尔项：

#eval if true then 5 else 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}
#check s ∪ [2, 3]
-- s ∪ List.toSet [2, 3] : 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}

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

Lean 还使用类型类 CoeDep 支持依值类型强制转换。例如，我们无法将任意命题强制转换到 Bool，只能转换实现了 Decidable 类型类的命题。

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

Lean 也会在有需要的时候构造链式（非依赖的）强制转换。事实上，类型类 CoeT 是 Coe 的传递闭包。

现在我们来考查第二种强制转换。 种类类（Class of Sort） 是指宇宙 Type u 的集合。第二种强制转换的形式如下：

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

其中 F 是如上所示的一族类型。这允许我们当 t 的类型为 F a1 ... an 时编写 s : t 。换言之，类型转换允许我们将 F a1 ... an 的元素视为类型。这在定义代数结构时非常有用，其中一个组成部分（即结构的载体）为 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

换句话说，一个半群包括一个类型「载体（carrier）」和一个乘法 mul，乘法满足结合性。 instance 命令允许我们用 a * b 代替 Semigroup.mul S a b 只要我们有 a b : S.carrier；注意，Lean 可以根据 a 和 b 的类型推断出参数 S。函数 Semigroup.carrier 将类 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
#check Semigroup.carrier

如果我们声明该函数是一个强制转换函数，那么无论何时我们都有半群 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)。

函数类型的类 ，是指 Π 类型集合 (z : B) → C。第三种强制转换形式为：

    c : (x1 : A1) → ... → (xn : An) → (y : F x1 ... xn) → (z : B) → C

其中 F 仍然是一个类型族，而 B 和 C 可以取决于 x1, ..., xn, y。这使得可以写 t s，只要 t 是 F a1 ... an 的元素。换句话说，转换使我们可以将 F a1 ... an 的元素视为函数。继续上面的示例，我们可以定义半群 S1 和 S2 之间的态射的概念。即，从 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)

#check @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)
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 := by rw [resp_mul f]
    _ = f a * f a * f a := by rw [resp_mul f]

有了强制类型转换，我们可以直接写 f (a * a * a) 而不必写 f.mor (a * a * a)。当 Morphism（态射）f 被用于原本期望函数的位置时， Lean 会自动插入强制转换。类似于 CoeSort，我们还有另一个类 CoeFun 用于这一类的强制转换。域 F 用于指定我们强制类型转换的目标函数类型。此类型可能依赖于我们强制转换的原类型。

Lean 4 定理证明