Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

正準化

注記: FIXME: この章の内容は 次世代トレイト解決の正準化の章と一部重複しています。 将来的にこれらの内容を再編成することが推奨されています。

正準化とは、推論値をそのコンテキストから分離するプロセスです。 これは正準クエリを実装するうえで重要な部分であり、より多くの背景を得るために親の章を読んでおくとよいでしょう。

正準化は、実際には非常に単純な概念に基づいています。すべての推論変数は常に 2 つの状態のいずれかにあります。つまり、まだそれがどの型であるかわからない未束縛の状態か、わかっている束縛済みの状態です。したがって、型/リージョンを含む何らかのデータ構造 T をその環境から分離するには、単に下へたどって T に現れる未束縛変数を見つけます。それらの変数は、0 から始まり固定された順序で番号付けされた「正準変数」に置き換えられます(ほとんどの場合は左から右ですが、実際には一貫している限り重要ではありません)。

たとえば、型 X = (?T, ?U) があり、?T?U が互いに異なる未束縛の推論変数である場合、X の正準形は (?0, ?1) になります。ここで ?0?1 はこれらの正準プレースホルダーを表します。型 Y = (?U, ?T)(?0, ?1) に正準化されることに注意してください。しかし、型 Z = (?T, ?T)(?0, ?0) に正準化されます((?U, ?U) も同様です)。言い換えると、推論変数の正確な同一性は重要ではありません。ただし、それらが繰り返される場合を除きます。

これを使って、キャッシュを改善したり、トレイト解決中にサイクルやその他のものを検出したりします。大まかに言えば、2 つのトレイトクエリが同じ正準形を持つ場合、それらは同じ答えを得るという考え方です。その答えは正準変数(?0, ?1)の形で表現され、それを元の変数(?T, ?U)へ対応付けて戻すことができます。

クエリの正準化

これがどのように機能するかを見るために、次のトレイトクエリを解決しようとしていると想像してください: ?A: Foo<'static, ?B>。ここで ?A?B は未束縛です。このクエリには 2 つの未束縛変数が含まれていますが、ライフタイム 'static も含まれています。トレイトシステムは一般にすべてのライフタイムを無視し、それらを等しく扱うため、正準化するときには、任意の自由ライフタイムも正準変数に置き換えます('static はここでは実際には_自由_ライフタイム変数であることに注意してください。私たちはそれをプログラム全体の型付けコンテキストではなく、このトレイト参照のコンテキストでのみ考慮しています。数学的には、プログラム全体にわたって量化しているのではなく、この義務についてのみ量化しています)。したがって、次の結果が得られます。

?0: Foo<'?1, ?2>

これを次のように別の形で書くこともあります。

for<T,L,T> { ?0: Foo<'?1, ?2> }

この for<> は、その中の各正準変数に関する情報を与えます。この場合、各 T は型変数を示すため、?0?2 は型です。L はライフタイム変数を示すため、?1 はライフタイムです。canonicalize メソッドは、各正準化された変数の「元の値」を持つ CanonicalVarValues 配列 OV も返します。

[?A, 'static, ?B]

クエリ応答を処理するときに、後でこのベクター OV が必要になります。

クエリの実行

正準クエリを構築したら、それを解決してみることができます。そのためには、最終的に新しい推論コンテキストを作成し、そのコンテキストで正準クエリをインスタンス化します。考え方としては、各正準変数に対応する新しい推論変数(適切な種類のもの)を含む、正準形からの置換 S を作成します。したがって、例のクエリでは次のようになります。

for<T,L,T> { ?0: Foo<'?1, ?2> }

置換 S は次のようになるかもしれません。

S = [?A, '?B, ?C]

その後、束縛された正準変数(?0 など)をこれらの推論変数に置き換えることで、次の完全にインスタンス化されたクエリが得られます。

?A: Foo<'?B, ?C>

ただし、置換 S を覚えておいてください。後でそれが必要になります。

さて、新しい推論コンテキストとインスタンス化されたクエリができたので、それを解決してみることができます。トレイトソルバー自体については別のセクションでより詳しく説明していますが、ここでは、それが確実性の値Proven または Ambiguous)を計算し、作成した推論変数に副作用を与えると言えば十分です。たとえば、Foo の impl が次のように 1 つだけだった場合:

impl<'a, X> Foo<'a, X> for Vec<X>
where X: 'a
{ ... }

その場合、確実性の値として Proven を得るとともに、新しい推論変数 '?D?E(impl 上のパラメータを表すため)を作成し、次のように単一化することになるかもしれません。

  • '?B = '?D
  • ?A = Vec<?E>
  • ?C = ?E

また、where 句により、リージョン制約 ?E: '?D も蓄積します。

最終的なクエリ結果を作成するには、これらの値をクエリの推論コンテキストから「持ち上げ」、元の推論コンテキストで再適用できるものにする必要があります。これは、正準化を再適用することによって行いますが、対象はクエリ結果です。

クエリ結果の正準化

親セクションで説明したように、ほとんどのトレイトクエリは、「確実性の値」certainty、結果の置換 var_values、およびいくつかのリージョン制約をまとめた結果になります。これを作成するために、最初にクエリをインスタンス化したときに作成した置換 S を再利用することになります。記憶を新たにすると、次のクエリがありました。

for<T,L,T> { ?0: Foo<'?1, ?2> }

これに対して置換 S を作成しました。

S = [?A, '?B, ?C]

その後、これらの変数のいくつかを他のものと単一化する作業を行いました。最新の結果で S を「更新」すると、次のようになります。

S = [Vec<?E>, '?D, ?E]

これらはまさに、元のクエリからの 3 つの入力変数に対する新しい値です。ただし、これらにはいくつかの新しい変数(?E など)が含まれていることに注意してください。もう一度正準化することで、それらを消すことができます。とはいえ、S だけを正準化するのではなく、クエリ応答 QR 全体を正準化します。

QR = {
    certainty: Proven,             // または任意のもの
    var_values: [Vec<?E>, '?D, ?E] // これは S
    region_constraints: [?E: '?D], // impl から
    value: (),                     // ここでの目的においては単に () だが、
                                   // 場合によっては型やその他の情報を
                                   // 持つことがある
}

結果は次のようになります。

Canonical(QR) = for<T, L> {
    certainty: Proven,
    var_values: [Vec<?0>, '?1, ?0]
    region_constraints: [?0: '?1],
    value: (),
}

(微妙な点が 1 つあります。クエリ結果を正準化するときには、自由ライフタイムに対して特別な扱いは行いません。たとえば、'?D への両方の参照は同じ正準変数(?1)に変換されています。これは、元のクエリで、すべての自由ライフタイムを新しい正準変数へ正準化していたこととは対照的です。)

この結果は、必要とされる各コンテキストで再適用されなければなりません。

正準化されたクエリ結果の処理

前のセクションでは、正準クエリ結果を生成しました。次に、その結果を元のコンテキストに適用する必要があります。思い出してみると、かなり最初のほうで、私たちは次のクエリを証明しようとしていました。

?A: Foo<'static, ?B>

これを次のように正準化しました。

for<T,L,T> { ?0: Foo<'?1, ?2> }

そして今、次の正準レスポンスが返ってきました。

for<T, L> {
    certainty: Proven,
    var_values: [Vec<?0>, '?1, ?0]
    region_constraints: [?0: '?1],
    value: (),
}

次に、このレスポンスを自分たちのコンテキストに適用したいと考えています。概念的には、そのために行うことは、(a) 結果内の各正準変数を新しい推論変数でインスタンス化し、(b) 結果内の値を元の値と単一化し、そして (c) リージョン制約を後で使うために記録する、というものです。ステップ (a) を実行すると、次のような結果になります。

{
      certainty: Proven,
      var_values: [Vec<?C>, '?D, ?C]
                       ^^   ^^^ fresh inference variables
      region_constraints: [?C: '?D],
      value: (),
}

ステップ (b) では、次を単一化します。

?A with Vec<?C>
'static with '?D
?B with ?C

そして最後に、リージョン制約 ?C: 'static が後で検証できるように記録されます。

(私たちが実際に行うのは、これを少し最適化した変種です。結果内の正準値をすべて変数で先行してインスタンス化するのではなく、値のベクターを走査し、その値が単なる正準変数であるケースを探します。この例では、values[2]?C なので、?C := ?B および '?D := 'static と推論できることを意味します。これにより、値の部分的な集合が得られます。値を見つけられなかったものについては、推論変数を作成します。)