10.1. 类声明🔗

类型类使用 Lean.Parser.Command.declaration : commandclass 关键字进行声明。

语法类型类声明

command ::= ...
    | `declModifiers` 是声明修饰符的集合，包括：

* 文档注释 `/-- ... -/`
* 属性列表 `@[attr1, attr2]`
* 可见性说明符 `private` 或 `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` 或 `nonrec`

所有修饰符都是可选的，并且必须按上述顺序出现。
`nestedDeclModifiers` 与 `declModifiers` 相同，但属性与声明打印在同一行；它用于嵌套在其他语法中的声明，例如结构体字段。declModifiers
      class `declId` 匹配 `foo` 或 `foo.{u,v}`：一个标识符，后面可以跟一个宇宙名称列表。declId `optDeclSig` 匹配类型可选的声明签名：先是一列绑定器，随后可以有 `: type`。bracketedBinder* (: term)?
        (extends (ident : )?term,*)?
        where
        (`declModifiers` 是声明修饰符的集合，包括：

* 文档注释 `/-- ... -/`
* 属性列表 `@[attr1, attr2]`
* 可见性说明符 `private` 或 `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` 或 `nonrec`

所有修饰符都是可选的，并且必须按上述顺序出现。
`nestedDeclModifiers` 与 `declModifiers` 相同，但属性与声明打印在同一行；它用于嵌套在其他语法中的声明，例如结构体字段。declModifiers ident ::)?
        structFields
      (deriving ident,*)?

声明一个新类型类。

Lean.Parser.Command.declaration : commandclass 声明创建了一个新的单构造器归纳类型，就好像使用了 Lean.Parser.Command.declaration : commandstructure 命令一样。实际上，Lean.Parser.Command.declaration : commandclass 和 Lean.Parser.Command.declaration : commandstructure 命令的结果几乎相同，并且诸如默认值之类的特性在两者中以相同的方式使用。请参考结构的文档以获取有关默认值、继承及结构的其他特性的更多信息。结构体声明和类声明之间的区别是：

方法而不是字段: 它不会创建以结构体类型的值作为显式参数的字段投影，而是创建方法。每个方法将对应的实例作为实例隐式参数。
实例隐式父类: 继承了其他类的类的构造器将其父类的实例作为实例隐式参数，而不是显式参数。当定义该类的实例时，实例合成被用于查找继承字段的值。不是类的父类仍然是底层构造器的显式参数。
借由实例合成得到的父投影: 结构体字段投影利用继承信息从子结构体值中投影出父结构体字段。类取而代之使用实例合成：给定一个子类实例，合成机制将构造父类；因此，方法不会像投影被添加到子结构体那样被添加到子类中。
注册为类: 得到的归纳类型被注册为类型类，可以为其定义实例，并且可以用作实例隐式参数的类型。
考虑输出参数与半输出参数: outParam 和 semiOutParam 小工具在结构体定义中没有意义，但它们在类定义中用于控制实例搜索。

虽然在类定义中允许 Lean.Parser.Command.declaration : commandderiving 子句，以保持类和结构体精译过程的平行，但它们并不常用，且应被视为高级特性。

非类的实例不存在

Lean 拒绝使用非类类型的实例隐式参数：

def f [n : invalid binder annotation, type is not a class instance
  Nat

Note: Use the command `set_option checkBinderAnnotations false` to disable the checkNat] : n = n := rfl

invalid binder annotation, type is not a class instance
  Nat

Note: Use the command `set_option checkBinderAnnotations false` to disable the check

类与结构体构造器对比

一个非常小的代数层次结构既可以表示为结构体（如下面的 S.Magma、S.Semigroup 和 S.Monoid），也可以表示为结构体与类的混合（C1.Monoid），或仅使用类（C2.Magma、C2.Semigroup 和 C2.Monoid）：

namespace S
structure Magma (α : Type u) where
  op : α → α → α

structure Semigroup (α : Type u) extends Magma α where
  op_assoc : ∀ x y z, op (op x y) z = op x (op y z)

structure Monoid (α : Type u) extends Semigroup α where
  ident : α
  ident_left : ∀ x, op ident x = x
  ident_right : ∀ x, op x ident = x
end S

namespace C1
class Monoid (α : Type u) extends S.Semigroup α where
  ident : α
  ident_left : ∀ x, op ident x = x
  ident_right : ∀ x, op x ident = x
end C1

namespace C2
class Magma (α : Type u) where
  op : α → α → α

class Semigroup (α : Type u) extends Magma α where
  op_assoc : ∀ x y z, op (op x y) z = op x (op y z)

class Monoid (α : Type u) extends Semigroup α where
  ident : α
  ident_left : ∀ x, op ident x = x
  ident_right : ∀ x, op x ident = x
end C2

S.Monoid.mk 和 C1.Monoid.mk 有着完全相同的签名，因为 C1.Monoid 类的父结构体本身并不是类：

S.Monoid.mk.{u} {α : Type u}
  (toSemigroup : S.Semigroup α)
  (ident : α)
  (ident_left : ∀ (x : α), toSemigroup.op ident x = x)
  (ident_right : ∀ (x : α), toSemigroup.op x ident = x) :
  S.Monoid α

C1.Monoid.mk.{u} {α : Type u}
  (toSemigroup : S.Semigroup α)
  (ident : α)
  (ident_left : ∀ (x : α), toSemigroup.op ident x = x)
  (ident_right : ∀ (x : α), toSemigroup.op x ident = x) :
  C1.Monoid α

类似地，因为 S.Magma 和 C2.Magma 都没有从其他结构体或类继承，所以它们的构造器是相同的：

S.Magma.mk.{u} {α : Type u} (op : α → α → α) : S.Magma αC2.Magma.mk.{u} {α : Type u} (op : α → α → α) : C2.Magma α

然而，S.Semigroup.mk 会将它的父级作为普通参数接受，而 C2.Semigroup.mk 会将其父级作为实例隐式参数接受：

S.Semigroup.mk.{u} {α : Type u}
  (toMagma : S.Magma α)
  (op_assoc : ∀ (x y z : α),
    toMagma.op (toMagma.op x y) z = toMagma.op x (toMagma.op y z)) :
  S.Semigroup α

C2.Semigroup.mk.{u} {α : Type u} [toMagma : C2.Magma α]
  (op_assoc : ∀ (x y z : α),
    toMagma.op (toMagma.op x y) z = toMagma.op x (toMagma.op y z)) :
  C2.Semigroup α

最后，C2.Monoid.mk 接受其半群父类作为实例隐式参数。对 op 的引用变为了对方法 C2.Magma.op 的引用，这依赖于实例合成通过其父级投影从 C2.Semigroup 实例隐式参数中恢复实现：

C2.Monoid.mk.{u} {α : Type u}
  [toSemigroup : C2.Semigroup α]
  (ident : α)
  (ident_left : ∀ (x : α), C2.Magma.op ident x = x)
  (ident_right : ∀ (x : α), C2.Magma.op x ident = x) :
  C2.Monoid α

在线查看 ↪

类型类的参数可以用小工具标记，小工具是恒等函数的特殊版本，会导致精译器对值的处理方式有所不同。小工具从不改变项的含义，但可能会让精译时的搜索过程对其采取不同的处理。小工具 outParam 和 semiOutParam 会影响实例合成，因此它们在对应小节记录。

某个类型是不是类对定义相等没有任何影响。参数相同的两个同类实例不一定相同，甚至在实际上可以有很大差别。

实例并不唯一

二叉堆插入的这个实现是有缺陷的：

structure Heap (α : Type u) where
  contents : Array α
deriving Repr

def Heap.bubbleUp [Ord α] (i : Nat) (xs : Heap α) : Heap α :=
  if h : i = 0 then xs
  else if h : i ≥ xs.contents.size then xs
  else
    let j := i / 2
    if Ord.compare xs.contents[i] xs.contents[j] == .lt then
      Heap.bubbleUp j { xs with contents := xs.contents.swap i j }
    else xs

def Heap.insert [Ord α] (x : α) (xs : Heap α) : Heap α :=
  let i := xs.contents.size
  {xs with contents := xs.contents.push x}.bubbleUp i

问题在于用一个 Ord 实例构造的堆可能在之后用到了另一个实例上，导致破坏堆的不变式。

修正该问题的一个方法是让堆类型依赖于选定的 Ord 实例：

structure Heap' (α : Type u) [Ord α] where
  contents : Array α

def Heap'.bubbleUp [inst : Ord α]
    (i : Nat) (xs : @Heap' α inst) :
    @Heap' α inst :=
  if h : i = 0 then xs
  else if h : i ≥ xs.contents.size then xs
  else
    let j := i / 2
    if inst.compare xs.contents[i] xs.contents[j] == .lt then
      Heap'.bubbleUp j {xs with contents := xs.contents.swap i j}
    else xs

def Heap'.insert [Ord α] (x : α) (xs : Heap' α) : Heap' α :=
  let i := xs.contents.size
  {xs with contents := xs.contents.push x}.bubbleUp i

在改进后的定义中，Heap'.bubbleUp 不必要地显式化；这里实例不需要被显式命名，因为即使不显式声明 Lean 也会选择所示的实例，但这确实向读者凸显了正确性不变式。

在线查看 ↪

10.1.1. 作为类的和类型🔗

大多数类型类遵循一组重载方法的范式，调用者可以从中自由选择。这自然可以用积类型来建模，其中被重载的方法即为其投影。然而，有些类是和类型：它们要求合成实例的接收者首先检查提供了哪个可用的实例构造器。为了将此类纳入考虑范围，类声明可以包含一个任意的归纳类型，而不仅是结构体声明的扩展形式。

语法类归纳类型声明

command ::= ...
    | `declModifiers` 是声明修饰符的集合，包括：

* 文档注释 `/-- ... -/`
* 属性列表 `@[attr1, attr2]`
* 可见性说明符 `private` 或 `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` 或 `nonrec`

所有修饰符都是可选的，并且必须按上述顺序出现。
`nestedDeclModifiers` 与 `declModifiers` 相同，但属性与声明打印在同一行；它用于嵌套在其他语法中的声明，例如结构体字段。declModifiers
      class inductive `declId` 匹配 `foo` 或 `foo.{u,v}`：一个标识符，后面可以跟一个宇宙名称列表。declId `optDeclSig` 匹配类型可选的声明签名：先是一列绑定器，随后可以有 `: type`。optDeclSig where
        (| `declModifiers` 是声明修饰符的集合，包括：

* 文档注释 `/-- ... -/`
* 属性列表 `@[attr1, attr2]`
* 可见性说明符 `private` 或 `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` 或 `nonrec`

所有修饰符都是可选的，并且必须按上述顺序出现。
`nestedDeclModifiers` 与 `declModifiers` 相同，但属性与声明打印在同一行；它用于嵌套在其他语法中的声明，例如结构体字段。declModifiers ident `optDeclSig` 匹配类型可选的声明签名：先是一列绑定器，随后可以有 `: type`。optDeclSig)*
      (deriving ident,*)?

类归纳类型就像其他归纳类型一样，唯一的区别是它们可能参与实例合成。类归纳类型的一个典型例子是 Decidable：在有自由变量的上下文中合成一个实例就等价于合成一个判定过程，但如果没有自由变量，那么就可以仅通过实例合成来确立命题的真值（就像 decide 策略所做的那样）。

10.1.2. 类缩写🔗

在某些情况下，代码库中可能到处会出现许多相关的类型类。与其重复写出所有名称，不如定义一个继承了所有相关类的类，而该类本身不提供任何新方法。但是，这个新类有一个缺点：必须显式地声明它的实例。

Lean.Parser.Command.classAbbrev : command将 ``` class abbrev C <params> := D_1, ..., D_n ``` 展开为 ``` class C <params> extends D_1, ..., D_n attribute [instance] C.mk ```class abbrev 命令允许创建类缩写，其中一个名称就是许多其他类参数的简写。在幕后，类缩写是用一个继承了其他类的类来表示的。其构造器还被额外声明为实例，这样新类就可以仅通过实例合成来构造了。

类缩写

plusTimes1 和 plusTimes2 都要求其参数的类型具有 Add 和 Mul 实例：

class abbrev AddMul (α : Type u) := Add α, Mul α

def plusTimes1 [AddMul α] (x y z : α) := x + y * z

class AddMul' (α : Type u) extends Add α, Mul α

def plusTimes2 [AddMul' α] (x y z : α) := x + y * z

由于 AddMul 是一个 Lean.Parser.Command.classAbbrev : command将 ``` class abbrev C <params> := D_1, ..., D_n ``` 展开为 ``` class C <params> extends D_1, ..., D_n attribute [instance] C.mk ```class abbrev，因此无需任何额外声明就能以 Nat 使用 plusTimes1：

37#eval plusTimes1 2 5 7

然而，plusTimes2 会失败，因为不存在 AddMul' Nat 的实例——目前还未声明任何实例：

#eval failed to synthesize instance of type class
  AddMul' ?m.8

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.plusTimes2 2 5 7

failed to synthesize instance of type class
  AddMul' ?m.8

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

声明一个非常通用的实例就能解决 Nat 和其他每种类型的问题：

instance [Add α] [Mul α] : AddMul' α where

37#eval plusTimes2 2 5 7

在线查看 ↪