7.1. クラス定義（Class Declarations）🔗

型クラスは Lean.Parser.Command.declaration : commandclass キーワードを用いて宣言されます。

syntax
command ::= ...
    | `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `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 bracketedBinder*
          (extends term,*)? (: 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 `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 コマンドの結果はほとんど同じであり、デフォルト値のような機能はどちらも同じように使うことができます。構造体のデフォルト値や継承、その他の機能については 構造体についてのドキュメント を参照してください。構造体選言とクラス宣言の違いは以下の通りです：

フィールドの代わりにメソッド

構造体型の値を明示的なパラメータとして受け取るフィールドの射影を作成する代わりに メソッド が作成されます。各メソッドは対応するインスタンスをインスタンス暗黙のパラメータとして取ります。

インスタンス暗黙としての親クラス

他のクラスを継承するクラスのコンストラクタは、明示的なパラメータではなくそのクラスの親のインスタンスをインスタンス暗黙のパラメータとして受け取ります。このクラスのインスタンスが定義されると、継承されたフィールドの値を見つけるためにインスタンス統合が使用されます。クラスでない親は依然として基礎となるコンストラクタの明示的なパラメータになります。

インスタンス統合経由の親の射影

構造体のフィールドの射影では 継承情報 を使用して、子の構造体の値から親の構造体フィールドを射影します。クラスでは代わりにインスタンス統合を使用します：子のクラスのインスタンスに対して、統合によって親が構成されます；したがって、子の構造体に射影が追加されるのに対して、子クラスにメソッドが追加されることはありません。

クラスとして登録される

宣言の結果出来る帰納型は型クラスとして登録され、インスタンスの定義およびインスタンス暗黙の引数の型のために使用されます。

out と semi-out パラメータの考慮

outParam と semiOutParam ガジェット は構造体定義では意味を持ちませんが、クラス定義ではインスタンス検索を制御するために使用されます。

Lean.Parser.Command.declaration : commandderiving 句は、クラスと構造体のエラボレーションの間の並列性を維持するためにクラス定義で許可されていますが、頻繁に使用されるものではなく、高度な機能と見なされるべきです。

クラス以外ではインスタンスは存在しない

Lean はクラスでない型のインスタンス暗黙のパラメータを拒否します：

def f [n : invalid binder annotation, type is not a class instance Nat use the command `set_option checkBinderAnnotations false` to disable the checkNat] : n = n := rfl 
invalid binder annotation, type is not a class instance
  Nat
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 α

型クラスへ渡すパラメータは ガジェット （gadget）としてマークすることができます。ガジェットはエラボレータに値を異なるように扱わせる恒等関数の特別なバージョンです。ガジェットは項の 意味 を変更することはありませんが、エラボレーション時の検索手続きで異なる扱いをさせることができます。ガジェット outParam と semiOutParam については インスタンス統合 に影響するため、その節で記述されています。

型がクラスであるかどうかは definitional equality には影響しません。同じパラメータを持つ同じクラスの2つのインスタンスは必ずしも同一ではなく、実際には大きく異なる可能性があります。

インスタンスは一意ではない

この二分ヒープへの挿入の実装にはバグがあります：

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 := failed to prove index is valid, possible solutions: - Use `have`-expressions to prove the index is valid - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid - Use `a[i]?` notation instead, result is an `Option` type - Use `a[i]'h` notation instead, where `h` is a proof that index is valid α : Type ?u.798 inst✝ : Ord α i : Nat xs : Heap α h✝ : ¬i = 0 h : ¬i ≥ xs.contents.size j : Nat := i / 2 ⊢ sorry < xs.contents.sizecould not synthesize default value for parameter 'hi' using tacticscould not synthesize default value for parameter 'hj' using tacticsfailed to prove index is valid, possible solutions: - Use `have`-expressions to prove the index is valid - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid - Use `a[i]?` notation instead, result is an `Option` type - Use `a[i]'h` notation instead, where `h` is a proof that index is valid α : Type ?u.798 inst✝ : Ord α i : Nat xs : Heap α h✝ : ¬i = 0 h : ¬i ≥ xs.contents.size j : Nat := i / 2 ⊢ sorry < xs.contents.sizexs.contents.swap invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor Nat⟨i, by omega⟩ invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor Nat⟨j, by omega⟩} 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 インスタンスで構成されたヒープが後で別のインスタンスで使用される可能性があり、これによってヒープの不変性が破られることです。

これを修正する方法の1つとして、ヒープの型を選択された 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 := failed to prove index is valid, possible solutions: - Use `have`-expressions to prove the index is valid - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid - Use `a[i]?` notation instead, result is an `Option` type - Use `a[i]'h` notation instead, where `h` is a proof that index is valid α : Type ?u.327 inst : Ord α i : Nat xs : Heap' α h✝ : ¬i = 0 h : ¬i ≥ xs.contents.size j : Nat := i / 2 ⊢ sorry < xs.contents.sizecould not synthesize default value for parameter 'hi' using tacticscould not synthesize default value for parameter 'hj' using tacticsfailed to prove index is valid, possible solutions: - Use `have`-expressions to prove the index is valid - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid - Use `a[i]?` notation instead, result is an `Option` type - Use `a[i]'h` notation instead, where `h` is a proof that index is valid α : Type ?u.327 inst : Ord α i : Nat xs : Heap' α h✝ : ¬i = 0 h : ¬i ≥ xs.contents.size j : Nat := i / 2 ⊢ sorry < xs.contents.sizexs.contents.swap invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor Nat⟨i, by omega⟩ invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor Nat⟨j, by omega⟩} else xs def Heap'.insert [Ord α] (x : α) (xs : Heap' α) : Heap' α := let i := xs.contents.size {xs with contents := xs.contents.push x}.bubbleUp i invalid 'end', insufficient scopesend A

改良された定義では、 Heap'.bubbleUp は不必要に明示的です；Lean はどうであれ指示されたインスタンスを選択するため、ここで明示的にインスタンスを名付ける必要はありませんが、これによってコードを読む人に前と中間で不変性が保たれていることが提示されます。

7.1.1. クラスとしての直和型（Sum Types as Classes）🔗

ほとんどの型クラスはオーバーロードされたメソッドのセットからクライアントが自由に選択できるというパラダイムに従っています。これは自然に直積型によってモデル化され、そこからオーバーロードされたメソッドが射影されます。しかし、いくつかのクラスは直和型です：これらのクラスの統合されたインスタンスを受け取る方は利用可能なインスタンスのコンストラクタとして どれが 提供されたかを最初にチェックする必要があります。このようなクラスを考慮するために、クラス宣言は構造体選言の拡張形だけでなく、任意の 帰納型 で構成することができます。

syntax
command ::= ...
    | `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `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 `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 タクティクでできるように）インスタンス統合だけで確立することができます。

7.1.2. 省略クラス（Class Abbreviations）🔗

いくつかのケースでは、関連する型クラスがコードベース全体に同時に出現することがあります。それらのクラス名を繰り返し記述するよりも、該当するすべてのクラスを継承するクラスを定義した方が新しいメソッドを追加せずに済みます。しかし、この新しいクラスには欠点があります：そのインスタンスは明示的に宣言しなければなりません。

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 abbreviation）を作成することができます。裏側では、省略クラスは他のすべてのクラスを継承するクラスとして表されます。そのコンストラクタはさらにインスタンスであることが宣言されているため、新しいクラスはインスタンス統合だけで構成できます。

省略クラス

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 であるため、 Nat で plusTimes1 を使用するために追加の宣言は必要ありません：

37#eval plusTimes1 2 5 7 
37

しかし、 plusTimes2 では AddMul' Nat インスタンスが無い（インスタンスがまだ何も宣言されていない）ため失敗します：

#eval failed to synthesize AddMul' ?m.22 Additional diagnostic information may be available using the `set_option diagnostics true` command.plusTimes2 2 5 7 
failed to synthesize
  AddMul' ?m.22
Additional diagnostic information may be available using the `set_option diagnostics true` command.

この場合は非常に一般的なインスタンスを宣言することで Nat や他のすべての型の問題を解決できます：

instance [Add α] [Mul α] : AddMul' α where 37#eval plusTimes2 2 5 7 
37