正準化
正準化は、値をそのコンテキストから隔離するプロセスであり、推論変数を含むゴールをグローバルにキャッシュするために必要です。
考え方としては、ゴール u32: Trait<?x> と u32: Trait<?y> が与えられ、ここで ?x と ?y が現在は制約されていない 2 つの異なる推論変数である場合、両方のゴールに対して同じ結果を得るべきです。したがって、正準クエリ exists<T> u32: Trait<T> を一度証明し、その結果を再利用できます。
まず正準クエリがどのように動作するかを見てから、正準化がどのように機能するかの詳細に入ります。
正準クエリのウォークスルー
少しわかりやすくするため、トレイトゴール u32: Trait<?x> を例として使い、関連する impl は impl<T> Trait<Vec<T>> for u32 だけであると仮定します。
入力の正準化
まずゴールを正準化し、推論変数を存在束縛変数に、プレースホルダーを全称束縛変数に置き換えます。これにより、正準ゴール exists<T> u32: Trait<T> が得られます。
すべての束縛変数の元の値を、元のコンテキスト内で覚えておきます。ここでは、これは T を ?x に対応付けます。これらの元の値は、後でクエリ応答を扱うときに使用されます。
次に、正準ゴールを使って正準クエリを呼び出します。
クエリ内での正準ゴールのインスタンス化
実際に正準ゴールを証明しようとするために、束縛変数を再び推論変数とプレースホルダーでインスタンス化します。
これは、クエリ内の完全に別の InferCtxt の中で行われます。クエリ内では、ゴール u32: Trait<?0> があります。また、正準ゴール内の束縛変数をインスタンス化するために使った値も覚えておきます。これは T を ?0 に対応付けます。
次に、ゴール u32: Trait<?0> を計算し、これが成り立つことを突き止めますが、?0 は Vec<?1> に制約されています。最後に、この結果を呼び出し元にとって有用なものへ変換します。
クエリ応答の正準化
ゴールが成り立つかどうかと、クエリ内からの推論制約の両方を呼び出し元に返す必要があります。
推論結果を呼び出し元に返すために、束縛変数からクエリ内でインスタンス化された値へのマッピングを正準化します。つまり、クエリ応答は Certainty::Yes と、T から exists<U> Vec<U> へのマッピングになります。
クエリ応答のインスタンス化
呼び出し元は、クエリによって返された制約を適用する必要があります。そのために、まず正準応答の束縛変数を再び推論変数とプレースホルダーでインスタンス化します。そのため、応答内のマッピングは T から Vec<?z> へのものになります。
次に、T の元の値（?x）を、応答内の T に対する値（Vec<?z>）と等価にします。これにより、?x は正しく Vec<?z> に制約されます。
ExternalConstraints
トレイトゴールの計算は、推論変数を制約するだけでなく、リージョン義務を追加することもあります。たとえば、ゴール (): AOutlivesB<'a, 'b> が与えられた場合、'a: 'b が成り立たなければならないという事実を返したいとします。
これは、束縛変数からクエリ内でインスタンス化された値へのマッピングを返すだけでなく、応答を構築する際に InferCtxt コンテキストから追加の ExternalConstraints を抽出することで行われます。
正準化は正確にはどのように機能するか
TODO: PR がマージされたらコードへリンクして詳述する
- 型と const: ユニバースを考慮し、推論変数は存在束縛変数へ、プレースホルダーは全称束縛変数へ
- 入力内のジェネリックパラメーターは、ルートユニバース内のプレースホルダーとして扱われる
- 入力内のすべてのリージョンは、すべて存在束縛変数にマッピングされ、それらを「一意化」する。
&'a (): Trait<'a>はexists<'0, '1> &'0 (): Trait<'1>に正準化される。これらのユニバースについては気にせず、すべてのリージョンを入力の最も高いユニバースに単純に入れる。 - 出力では、呼び出し元のユニバース内のすべてのものがルートユニバースに入れられ、呼び出し元の元の値と変数値を単一化するときにのみ正しいユニバースを得る
- 応答内のリージョンは一意化せず、
'staticは正準化しない