7.3. インスタンス統合（Instance Synthesis）🔗

インスタンス統合は与えられた型クラスのインスタンスを見つけるか失敗するかのどちらかの結果となる再帰的な検索手順です。言い換えると、型クラスとして登録されている型が与えられたとき、インスタンス統合はその型を持つ項の構築を試みます。これは reducibility を尊重します： semi-reducible や irreducible の定義は展開されないため、 reducible でない限り、定義に対するインスタンスは自動的にその定義の展開に対するインスタンスとして扱われることはありません。与えられたクラスに対して、インスタンスは複数ある可能性があります；この場合、宣言された優先度と宣言の順番がタイブレーカとして使用されます。順番として、同じ優先度のインスタンス同士ではより新しいインスタンスがそれより古いものより優先されます。

この検索手続きはダイアモンドがあっても効率的であり、巡回があっても無限にループすることはありません。 ダイアモンド （diamond）は与えられたゴールへのルートが1つ以上ある場合に発生し、巡回（cycle）は2つのインスタンスがそれぞれもう1つを解決すれば解決できる状況です。ダイアモンドは実際に、型クラスを使用して数学的概念をエンコードする際に定期的に発生します。また Lean の強制機能は有限集合と有限多集合の間などで巡回を自然に導きます。

インスタンス統合は Lean.Parser.Command.synth : command#synth コマンドを使ってテストすることができます。

syntax

Lean.Parser.Command.synth : command#synth コマンドは指定されたクラスのインスタンスの統合を試みます。成功した場合、結果の項が出力されます。

command ::= ...
    | #synth term

さらに、 inferInstance と inferInstanceAs を使うことで、インスタンス自体が必要である位置においてインスタンスを統合することができます。

def

inferInstance.{u} {α : Sort u} [i : α] : α

inferInstance synthesizes a value of any target type by typeclass inference. This function has the same type signature as the identity function, but the square brackets on the [i : α] argument means that it will attempt to construct this argument by typeclass inference. (This will fail if α is not a class.) Example:

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

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

example : foo.default = (default, default) :=
  rfl

def

inferInstanceAs.{u} (α : Sort u) [i : α] : α

inferInstanceAs α synthesizes a value of any target type by typeclass inference. This is just like inferInstance except that α is given explicitly instead of being inferred from the target type. It is especially useful when the target type is some α' which is definitionally equal to α, but the instance we are looking for is only registered for α (because typeclass search does not unfold most definitions, but definitional equality does.) Example:

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

7.3.1. インスタンス検索の概要（Instance Search Summary）

一般的に言うと、インスタンス統合は再帰的な検索手順であり、一般的には任意にバックトラックすることができます。統合はインスタンスの項で成功することもあれば、そのような項が見つからなければ失敗することもあり、情報が不十分であれば 行き詰る こともあります。インスタンス統合アルゴリズムの詳細な説明は Selsam, Ullrich, and de Moura (2020)Daniel Selsam, Sebastian Ullrich, and Leonardo de Moura, 2020. “Tabled typeclass resolution”. arXiv:2001.04301 にあります。インスタンス検索問題は、具体的な引数に適用される型クラスによって与えられます；これらの引数の値は既知と未知の場合のどちらもあります。インスタンス検索は、登録された各インスタンスと同様に、型がクラスであるすべてのローカル束縛変数を優先度と定義の順に試行します。候補のインスタンス自体がインスタンスの暗黙のパラメータを持つ場合、統合のタスクが追加で課されます。

問題は型クラスへの入力パラメータがすべてわかっているときのみに試行されます。ある問題がまだ試行できない場合、その分岐は行き詰っています；他の部分問題の進行によってこの問題が解けるようになる場合があります。出力または半出力パラメータはインスタンス検索の開始時において既知と未知のどちらでもよいです。出力パラメータはインスタンスが問題にマッチするかどうかをチェックする際には無視されますが、半出力パラメータは考慮されます。

与えられた問題の解の各候補はテーブルに保存されます；これにより、巡回が存在する場合の無限後退やダイアモンド（つまり、同じゴールを達成できる複数の経路）が存在する場合の指数関数的な検索のオーバーヘッドを防ぐことができます。探索の分岐は以下のいずれが発生したときに失敗します：

すべてのインスタンス候補が試行され、検索空間が空になった場合。
オプション synthInstance.maxSize で指定されたインスタンスサイズの上限に達した場合。
出力パラメータの統合結果の値が検索問題で指定された値と一致しない場合。失敗した分岐は再試行されません。

検索が失敗か行き詰った場合、検索プロセスは優先度の高い順に一致するデフォルトインスタンスの使用を試みます。デフォルトインスタンスでは、入力パラメータを完全に知っている必要はなく、インスタンスパラメータの値によってインスタンス化することができます。デフォルトインスタンスはインスタンス暗黙のパラメータを取ることがあり、これによってさらなる再帰的な検索が引き起こされます。

成功した問題が完全に分かっている（つまり未解決のメタ変数がない）成功したブランチは刈り込まれ、それ以上成功する可能性のあるインスタンスは試みられません。なぜなら先に成功した分岐を失敗させる可能性のあるインスタンスはこの後には存在しないからです。

7.3.2. インスタンス検索問題（Instance Search Problems）

インスタンス検索は、（潜在的に引数が0個の可能性もあります）関数適用の作成中に発生します。暗黙のパラメータの値のうちいくつかはそれ以外から強制されます；例えば、暗黙の型パラメータは、それより後に明示的に提供された値引数の型を使用して解決されるかもしれません。暗黙のパラメータはプログラム中のその時点で期待される型の情報を使って解決することもできます。インスタンス暗黙の引数の検索は見つかった暗黙の引数の値を使用し、さらに他の値を解決することができます。

インスタンス統合はインスタンス暗黙のパラメータの型から始めます。この型は0個以上の引数に対する型クラスの適用でなければなりません；検索開始時にはこれらの引数の値は既知と未知の場合のどちらもあります。クラスの引数が未知の場合、対応するパラメータが出力パラメータとしてマークされ、明示的にインスタンス統合のルーチンの出力にならない限り、検索プロセスはそれをインスタンス化しません。

検索は成功することもあれば、失敗することも行き詰ることもあります；行き詰った検索は未知の引数の値がわかることで前進できるかもしれないような場合に発生する可能性があります。行き詰った検索はエラボレータがそこまでに未知だった暗黙の引数の1つを発見した場合に再度呼び出される場合があります。これが発生しない場合、行き詰った検索は失敗します。

7.3.3. 候補のインスタンス（Candidate Instances）

インスタンス統合では、ローカルインスタンスとグローバルインスタンスの両方を検索に使用します。 ローカルインスタンス （local instance）とは、ローカルコンテキストで利用可能なインスタンスのことです；これらは関数のパラメータであったり、let でローカルに定義されたりします。ローカルインスタンスは特別に示す必要はありません；型が型クラスである任意のローカル変数はインスタンス統合の候補となります。 グローバルインスタンス （global instance）はグローバル環境で利用可能なインスタンスです；すべてのグローバルインスタンスは instance 属性が適用された定義名です。 Lean.Parser.Command.declaration : commandinstance 宣言は自動的に instance 属性を適用します。

ローカルインスタンス

この例では、 addPairs はローカルに定義された Add NatPair インスタンスを含みます：

structure NatPair where
  x : Nat
  y : Nat

def addPairs (p1 p2 : NatPair) : NatPair :=
  let _ : Add NatPair :=
    ⟨fun ⟨x1, y1⟩ ⟨x2, y2⟩ => ⟨x1 + x2, y1 + y2⟩⟩
  p1 + p2

このローカルインスタンスはインスタンス統合によって発見され、加法に用いられます。

優先度を持つローカルインスタンス

ここで、 addPairs はグローバルインスタンスがあるにもかかわらず、ローカルで定義された Add NatPair インスタンスを含みます：

structure NatPair where
  x : Nat
  y : Nat

instance : Add NatPair where
  add
    | ⟨x1, y1⟩, ⟨x2, y2⟩ => ⟨x1 + x2, y1 + y2⟩

def addPairs (p1 p2 : NatPair) : NatPair :=
  let _ : Add NatPair :=
    ⟨fun _ _ => ⟨0, 0⟩⟩
  p1 + p2

このローカルインスタンスはグローバルのものの代わりに選択されます：

{ x := 0, y := 0 }#eval addPairs ⟨1, 2⟩ ⟨5, 2⟩

{ x := 0, y := 0 }

7.3.4. インスタンスパラメータと統合（Instance Parameters and Synthesis）🔗

インスタンスの検索プロセスはクラスのパラメータに大きく支配されています。型クラスは一定数のパラメータを取り、インスタンスはそのパラメータの選択がインスタンス統合を試みるクラスの型のパラメータと 互換性がある 場合において、検索が試行されます。

インスタンス自体もパラメータを取ることがありますが、インスタンス統合におけるインスタンスのパラメータの役割は大きく異なります。インスタンスのパラメータは、インスタンス統合によってインスタンス化される可能性のある変数か、インスタンスを使用する前に行うべきさらなる統合作用のいずれかを表します。特に、インスタンスに対するパラメータは明示的・暗黙的・インスタンス暗黙のいずれかです。インスタンス暗黙であれば、さらに再帰的なインスタンス検索を引き起こしますが、明示的・暗黙的なパラメータは単一化によって解決されなければなりません。

インスタンスの暗黙的・明示的なパラメータ

インスタンスは通常、暗黙的またはインスタンス暗黙のパラメータを取りますが、明示的なパラメータはインスタンス統合時に暗黙的であるかのように埋めることができます。この例では、 aNonemptySumInstance が統合によって見つかり、正しい型となるために必要な Nat に明示的に適用されます。

instance aNonemptySumInstance (α : Type) {β : Type} [inst : Nonempty α] : Nonempty (α ⊕ β) :=
  let ⟨x⟩ := inst
  ⟨.inl x⟩

set_option pp.explicit true in
@aNonemptySumInstance Nat Empty (@instNonemptyOfInhabited Nat instInhabitedNat)#synth Nonempty (Nat ⊕ Empty)

出力では、明示的な引数 Nat と暗黙的な引数 Empty の両方が検索ゴールによる単一化によって見つかり、 Nonempty Nat インスタンスは再帰的なインスタンス統合によって見つかっています。

@aNonemptySumInstance Nat Empty (@instNonemptyOfInhabited Nat instInhabitedNat)

7.3.5. 出力パラメータ（Output Parameters）🔗

デフォルトでは、型クラスのパラメータは検索プロセスへの入力とみなされます。パラメータが未知の場合、検索プロセスは行き詰ります。なぜならインスタンスを選択するにはパラメータがインスタンスの値と一致する必要がありますが、不完全な情報に基づいて決定することはできないからです。ほとんどの場合、インスタンスを推測することはインスタンスの統合を予測不可能にします。

しかし、あるパラメータを選択すると自動的に別のパラメータが選択されるような場合もあります。例えば、オーバーロードされたメンバシップ述語の型クラス Membership はデータ構造の要素の型を出力として扱うため、インスタンス統合を開始する前に両方の型を決定するのに十分な型注釈があることを要求する代わりに、要素の型は使用する側でデータ構造の型によって決定することができます。 List Nat の要素は単純にリスト内のメンバシップに基づいて Nat であると結論付けることができます。

型クラスのパラメータは outParam ガジェットでそれらの型をラップすることで出力として宣言することができます。クラスのパラメータが 出力パラメータ （output parameter）である場合、インスタンス統合はそれが既知であることを要求しません；実際、どんな値を渡しても完全に無視されます。入力パラメータがマッチする最初のインスタンスが選択され、そのインスタンスの出力パラメータの値には利用箇所で使用される値が割り当てられます。そのインスタンスの出力パラメータに値が存在していた場合、統合が完了した後にその値と割り当てられた値が比較され、一致しない場合はエラーとなります。

def

outParam.{u} (α : Sort u) : Sort u

Gadget for marking output parameters in type classes.

For example, the Membership class is defined as:

class Membership (α : outParam (Type u)) (γ : Type v)

This means that whenever a typeclass goal of the form Membership ?α ?γ comes up, Lean will wait to solve it until ?γ is known, but then it will run typeclass inference, and take the first solution it finds, for any value of ?α, which thereby determines what ?α should be.

This expresses that in a term like a ∈ s, s might be a Set α or List α or some other type with a membership operation, and in each case the "member" type α is determined by looking at the container type.

出力パラメータと行き詰った検索

このシリアライズ化のフレームワークは、値を基礎となるストレージ型に変換する方法を提供します：

class Serialize (input output : Type) where
  ser : input → output
export Serialize (ser)

instance : Serialize Nat String where
  ser n := toString n

instance [Serialize α γ] [Serialize β γ] [Append γ] :
    Serialize (α × β) γ where
  ser
    | (x, y) => ser x ++ ser y

この例では出力パラメータは不明です：

example := typeclass instance problem is stuck, it is often due to metavariables
  Serialize (Nat × Nat) ?m.16ser (2, 3)

インスタンス統合は Serialize Nat String インスタンスを選択することができず、したがって Append String インスタンスも選択することができません。なぜならこれは出力の型が String とインスタンス化されることを要求するからです。そのためこの検索は行き詰ります：

typeclass instance problem is stuck, it is often due to metavariables
  Serialize (Nat × Nat) ?m.16

この問題を解決する1つの方法は期待される型を与えることです：

example : String := ser (2, 3)

もう1つの方法は出力の型を出力パラメータにすることです：

class Serialize (input : Type) (output : outParam Type) where
  ser : input → output
export Serialize (ser)

instance : Serialize Nat String where
  ser n := toString n

instance [Serialize α γ] [Serialize β γ] [Append γ] :
    Serialize (α × β) γ where
  ser
    | (x, y) => ser x ++ ser y

これでインスタンス統合は Serialize Nat String インスタンスを自由に選択できるようになり、これによって ser の未知の暗黙の output パラメータを解決できるようになります：

example := ser (2, 3)

値がすでに与えられている出力パラメータ

クラス OneSmaller は、ある型の最大でない要素を要素が1つ少ない型に変換する方法を表現します。入力型 Option Bool にマッチするインスタンスが2つあり、出力が異なります：

class OneSmaller (α : Type) (β : outParam Type) where
  biggest : α
  shrink : (x : α) → x ≠ biggest → β

instance : OneSmaller (Option α) α where
  biggest := none
  shrink
    | some x, _ => x

instance : OneSmaller (Option Bool) (Option Unit) where
  biggest := some true
  shrink
    | none, _ => none
    | some false, _ => some ()

instance : OneSmaller Bool Unit where
  biggest := true
  shrink
    | false, _ => ()

インスタンス統合は最後に定義されたインスタンスを選択するため以下のコードはエラーになります：

#check failed to synthesize
  OneSmaller (Option Bool) Bool
Additional diagnostic information may be available using the `set_option diagnostics true` command.OneSmaller.shrink (β := Bool) (some false) sorry

failed to synthesize
  OneSmaller (Option Bool) Bool
Additional diagnostic information may be available using the `set_option diagnostics true` command.

与えられた β の値を考慮することなく、インスタンス統合によって OneSmaller (Option Bool) (Option Unit) インスタンスが選択されています。

半出力パラメータ （semi-output parameter）は統合を開始する前に知っている必要がないという点では出力パラメータと同じです；出力パラメータとは異なり、インスタンスを選択する際にその値が考慮されます。

def

semiOutParam.{u} (α : Sort u) : Sort u

Gadget for marking semi output parameters in type classes.

Semi-output parameters influence the order in which arguments to type class instances are processed. Lean determines an order where all non-(semi-)output parameters to the instance argument have to be figured out before attempting to synthesize an argument (that is, they do not contain assignable metavariables created during TC synthesis). This rules out instances such as [Mul β] : Add α (because β could be anything). Marking a parameter as semi-output is a promise that instances of the type class will always fill in a value for that parameter.

For example, the Coe class is defined as:

class Coe (α : semiOutParam (Sort u)) (β : Sort v)

This means that all Coe instances should provide a concrete value for α (i.e., not an assignable metavariable). An instance like Coe Nat Int or Coe α (Option α) is fine, but Coe α Nat is not since it does not provide a value for α.

半出力パラメータはインスタンスに要件を課します：半出力パラメータを持つ各インスタンスは、その半出力パラメータの値を決定しなければなりません。

値がすでに与えられている半出力パラメータ

クラス OneSmaller は、ある型の最大でない要素を要素が1つ少ない型に変換する方法を表現します。これは Option Bool という入力型にマッチする2つの別々のインスタンスを持っており、異なる出力をもちます：

class OneSmaller (α : Type) (β : semiOutParam Type) where
  biggest : α
  shrink : (x : α) → x ≠ biggest → β

instance : OneSmaller (Option α) α where
  biggest := none
  shrink
    | some x, _ => x

instance : OneSmaller (Option Bool) (Option Unit) where
  biggest := some true
  shrink
    | none, _ => none
    | some false, _ => some ()

instance : OneSmaller Bool Unit where
  biggest := true
  shrink
    | false, _ => ()

インスタンス統合は、インスタンスを選択する時に半出力パラメータを考慮するため、β として提供された値によって OneSmaller (Option Bool) (Option Unit) インスタンスが渡されます：

OneSmaller.shrink (some false) ⋯ : Bool#check OneSmaller.shrink (β := Bool) (some false) sorry

OneSmaller.shrink (some false) ⋯ : Bool

7.3.6. デフォルトインスタンス（Default Instances）🔗

インスタンスを選ばずにインスタンス統合が失敗した場合、 default_instance 属性を使用して指定された デフォルトインスタンス （default instance）が優先度の高い順に試行されます。優先度が等しい場合、より最近定義されたデフォルトインスタンスがそれ以前のものよりも先に選択されます。検索が成功した最初のデフォルトインスタンスが選択されます。

デフォルトインスタンスはデフォルトインスタンス自体がインスタンス暗黙のパラメータを持つ場合、さらに再帰的なインスタンス検索を引き起こす可能性があります。再帰検索が失敗した場合、検索プロセスはバックトラックし、次のデフォルトインスタンスが試行されます。

7.3.7. 「道徳的に標準的な」インスタンス（“Morally Canonical” Instances）

インスタンス統合中、ゴールが完全に既知（つまりメタ変数を含まない）であり、検索が成功した場合、同じゴールに対してそれ以上インスタンス検索が試行されることはありません。言い換えると、あるゴールに対して、その後の情報の増加によって反論できないような方法で検索が成功した場合、たとえ使用できた可能性のある他のインスタンスがあったとしてもそのゴールは再度試行されません。この最適化により、インスタンス統合の検索の後の分岐で失敗した場合に誤ったバックトラックが発生し、それより前の分岐で解が早く得られるはずだったことが、大規模な状態空間の低速な検索に置き換わってしまうことを防ぐことができます。

この最適化は、インスタンスが 道徳的に標準的 （morally canonical）であるという仮定に依存しています。与えられた型クラスのオーバーロードされた演算の潜在的な実装が1つ以上あったり、ダイアモンドによってインスタンスを統合する方法が1つ以上あったりしても、 発見されたインスタンスは他のインスタンスと同じように良いものである と考えるべきです。言い換えれば、そのうちの1つが動作することが保証されている限り、 すべての 潜在的なインスタンスを考慮する必要はありません。この最適化は後方互換なオプション backward.synthInstance.canonInstances で無効にすることができますが、これは今後の Lean で削除される可能性があります。

インスタンス暗黙のパラメータを使用するコードは、すべてのインスタンスを同等のものとみなすように準備すべきです。言い換えれば、統合されたインスタンスの違いにあたってもロバストでなければなりません。そのコードが 実際に インスタンスが同等である事実に依存する場合、インスタンスを明示的に操作するか（例えば、ローカル定義を介して構造体フィールドに保存するか、構造体を適切なクラスから継承させる）、インスタンスの異なる選択が互換性のない型につながるように型の中でこの依存関係を明示的にする必要があります。

7.3.8. オプション（Options）

option

backward.synthInstance.canonInstances

Default value: true

use optimization that relies on 'morally canonical' instances during type class resolution

option

synthInstance.maxHeartbeats

Default value: 20000

maximum amount of heartbeats per typeclass resolution problem. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit

option

synthInstance.maxSize

Default value: 128

maximum number of instances used to construct a solution in the type class instance synthesis procedure