10.1. 类声明🔗

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

syntaxType Class Declarations

command ::= ...
    | `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers
      class `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` bracketedBinder* (: term)?
        (extends (ident : )?term,*)?
        where
        (`declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. 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 命令的结果几乎相同，并且两者中可以以相同的方式使用默认值等功能。有关结构体的默认值、继承和其他功能的更多信息，请参阅结构体文档。结构声明和类声明之间的区别是：

方法而不是字段: 创建 methods，而不是创建将结构类型的值作为显式参数的字段投影。每个方法都将相应的实例作为实例隐式参数。
实例隐式父类: 扩展其他类的类的构造函数将其父类的实例作为实例隐式参数，而不是显式参数。当定义此类的实例时，实例综合用于查找继承字段的值。不是类的父级仍然是底层构造函数的显式参数。
通过实例合成进行父投影: 结构字段投影利用继承信息从子结构值投影父结构字段。相反，类使用实例合成：给定一个子类实例，合成将构造父类；因此，方法不会以与将投影添加到子结构相同的方式添加到子类中。
注册为班级: 生成的归纳类型被注册为类型类，可以为其定义实例，并且可以用作实例隐式参数的类型。
考虑 Out 和 semi-out 参数: outParam 和 semiOutParam gadgets 在结构定义中没有任何意义，但它们在类定义中用于控制实例搜索。

虽然类定义允许使用 Lean.Parser.Command.declaration : commandderiving 子句来维护类和结构精化之间的并行性，但它们并不经常使用，应被视为高级功能。

No Instances of Non-Classes

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

Class vs Structure Constructors

非常小的代数层次结构可以表示为结构（下面的 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 α

Live ↪

类型类的参数可以用 gadgets 标记，它们是恒等函数的特殊版本，导致精化器以不同方式处理值。小工具永远不会改变术语的含义，但它们可能会导致在精化时间搜索过程中以不同方式对待该术语。小工具 outParam 和 semiOutParam 影响实例综合，因此它们记录在该部分中。

类型是否是类对定义等价没有影响。具有相同参数的同一类的两个实例不一定相同，实际上可能非常不同。

Instances are Not Unique

这种二进制堆插入的实现是有缺陷的：

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 仍然会选择指定的实例，但它确实为读者带来了正确性不变的前沿和中心。

Live ↪

10.1.1. 将类型求和为类🔗

大多数类型类遵循一组重载方法的范例，客户端可以从中自由选择。这自然是通过产品类型建模的，重载方法是该产品类型的投影。然而，有些类是求和类型：它们要求合成实例的接收者首先检查提供了可用实例构造函数。为了说明这些类，类声明可以包含任意归纳类型，而不仅仅是结构声明的扩展形式。

syntaxClass Inductive Type Declarations

command ::= ...
    | `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers
      class inductive `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` optDeclSig where
        (| `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers ident `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` optDeclSig)*
      (deriving ident,*)?

归纳类型类与其他归纳类型类一样，只是它们可以参与实例合成。类归纳的典型示例是 Decidable：在具有自由变量的上下文中合成实例相当于合成决策过程，但如果没有自由变量，则可以仅通过实例合成来确定命题的真实性（如 decide策略所做的那样）。

10.1.2. 类别缩写🔗

在某些情况下，许多相关的类型类可能在整个代码库中同时出现。不必重复编写所有名称，而是可以定义一个扩展所有相关类的类，而本身不提供新方法。然而，这个新类有一个缺点：它的实例必须显式声明。

Lean.Parser.Command.classAbbrev : commandExpands ``` class abbrev C <params> := D_1, ..., D_n ``` into ``` class C <params> extends D_1, ..., D_n attribute [instance] C.mk ```class abbrev 命令允许创建 class abbreviations，其中一个名称是许多其他类参数的缩写。在幕后，类缩写由扩展所有其他类的类来表示。它的构造函数还被声明为一个实例，因此可以仅通过实例合成来构造新类。

Class Abbreviations

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 : commandExpands ``` class abbrev C <params> := D_1, ..., D_n ``` into ``` class C <params> extends D_1, ..., D_n attribute [instance] C.mk ```class abbrev，因此无需附加声明即可将 plusTimes1 与 Nat 一起使用：

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

Live ↪