プレースホルダーとユニバース
私たちは時折、具体的には知ることができない領域について推論しなければならないことがあります。たとえば、次のプログラムを考えてみましょう。
// static 参照を必要とする関数
fn foo(x: &'static u32) { }
fn bar(f: for<'a> fn(&'a u32)) {
// ^^^^^^^^^^^^^^^^^^^ **任意の**参照を受け取れる関数
let x = 22;
f(&x);
}
fn main() {
bar(foo);
}
このプログラムは型チェックに通るべきではありません。foo は引数に static 参照を必要とし、bar は 任意の参照を受け取る関数を渡されることを期待しているためです(たとえば、自身のスタック上の何かを使ってその関数を呼び出せるように)。しかし、これを どのように 拒否し、なぜ 拒否するのでしょうか。
サブタイピングとプレースホルダー
main を型チェックするとき、特に bar(foo) の呼び出しを型チェックするとき、最終的に次のようなサブタイピング関係に行き着きます。
fn(&'static u32) <: for<'a> fn(&'a u32)
---------------- -------------------
the type of `foo` the type `bar` expects
この種のサブタイピングは、スーパータイプで束縛されている変数を取り出し、それらを全称量化された代表で置き換えることで処理します。ここではそれを !1 のように表します。私たちはこれらの領域を「プレースホルダー領域」と呼びます。基本的には、「何らかの未知の領域」を表しています。
この置き換えを行うと、次の関係になります。
fn(&'static u32) <: fn(&'!1 u32)
ここでの重要な考え方は、この未知の領域 '!1 は他のどの領域とも関係していないということです。したがって、サブタイピング関係が '!1 について真であることを証明できれば、それは任意の領域について真であるはずであり、それこそが私たちの望んでいたことです。
では、次に何が起こるかを順に見ていきましょう。2 つの関数がサブタイプであるかどうかを確認するには、それらの引数が望ましい関係を持っているかを確認します(関数の引数は反変なので、ここでは左辺と右辺を入れ替えます)。
&'!1 u32 <: &'static u32
参照に関する基本的なサブタイピング規則によれば、これは '!1: 'static であれば真になります。つまり、「何らかの未知の領域 !1」が 'static より長生きする場合です。さて、これは真である 可能性はあります。結局のところ、'!1 は 'static かもしれません。しかし、それが真であるとは 分かりません。したがって、これは(最終的には)エラーを生成するべきです。
ユニバースとは何か?
前のセクションでは、プレースホルダー領域という考え方を導入し、それを !1 と表しました。私たちはこの数値 1 を ユニバースインデックス と呼びます。「ユニバース」という考え方は、ある型の中、またはある時点でスコープ内にある名前の集合である、というものです。ユニバースは木として形成され、各子は親にいくつかの新しい名前を追加します。したがって、ルートユニバース は概念的には、ライフタイム 'static や型 i32 のようなグローバルな名前を含みます。コンパイラでは、ジェネリック型パラメータもこのルートユニバースに入れます(この意味では、ルートユニバースは 1 つだけではなく、アイテムごとに 1 つあります)。そこで、この関数 bar を考えてみましょう。
struct Foo { }
fn bar<'a, T>(t: &'a T) {
...
}
ここで、ルートユニバースはライフタイム 'static と 'a で構成されます。実際には、ここではライフタイムに注目していますが、同じ概念を型にも適用できます。その場合、型 Foo と T が(i32 のような他のグローバル型とともに)ルートユニバースに含まれます。基本的に、ルートユニバースは bar の本体に自由に現れるすべての名前を含みます。
次に、変数 x を追加して bar を少し拡張してみましょう。
fn bar<'a, T>(t: &'a T) {
let x: for<'b> fn(&'b u32) = ...;
}
ここで、名前 'b はルートユニバースの一部ではありません。代わりに、この for<'b> の中に「入る」とき(たとえば、それをプレースホルダーで置き換えることによって)、ルートの子ユニバースを作成します。これを U1 と呼ぶことにしましょう。
U0 (root universe)
│
└─ U1 (child universe)
この考え方は、この子ユニバース U1 がルートユニバース U0 に新しい名前を追加する、というものです。その名前はユニバース番号 !1 によって識別しています。
次に、もう 1 つの変数 y を追加して bar を少し拡張してみましょう。
fn bar<'a, T>(t: &'a T) {
let x: for<'b> fn(&'b u32) = ...;
let y: for<'c> fn(&'c u32) = ...;
}
この 型に入るとき、再び新しいユニバースを作成し、それを U2 と呼びます。その親はルートユニバースになり、U1 はその兄弟になります。
U0 (root universe)
│
├─ U1 (child universe)
│
└─ U2 (child universe)
これは、U2 の中では U0 または U2 のものを名前で参照できますが、U1 のものは参照できないことを意味します。
存在変数にユニバースを与える。 ユニバースという概念を得たので、それを使って型チェッカーなどを拡張し、不正な名前が漏れ出すのを防ぐことができます。その考え方は、各推論(存在)変数に、型であれライフタイムであれ、ユニバースを与えるというものです。その変数の値は、そのユニバースから見える名前だけを参照できます。たとえば、あるライフタイム変数が U0 で作成された場合、その変数に !1 や !2 の値を割り当てることはできません。なぜなら、それらの名前はユニバース U0 から見えないからです。
単なるカウンタでユニバースを表す。 コンパイラがユニバースの完全な木を追跡していないことを知ると、驚くかもしれません。代わりに、単にカウンタを保持しています。そして、あるユニバースが別のユニバースを見ることができるかどうかを判定するには、単にインデックスがより大きいかどうかを確認します。たとえば、U2 は U0 を見ることができます。なぜなら 2 >= 0 だからです。しかし、U0 は U2 を見ることができません。なぜなら 0 >= 2 は偽だからです。
どうしてこれで済ませられるのでしょうか。これは、U2 が U1 も見ることを許してしまうことを意味しないのでしょうか。答えは、はい、もしその問いが発生することがあれば、そうなります。しかし、私たちの型チェッカーなどの構造上、それが起こる方法はありません。ユニバース U1 で起こっていることが U2 で起こっていることと「通信」するには、共通の共有推論変数 X を持つ必要があります。そして、U1 の中のすべてのものは U1 とその子にだけスコープされているため、その推論変数 X は U0 に存在しなければなりません。そして X は U0 にあるので、U1(または U2)のどのものも名前で参照できません。これは、ある種の汎用的な「論理」の例を使うと最も分かりやすいかもしれません。
exists<X> {
forall<Y> { ... /* Y は U1 にある ... */ }
forall<Z> { ... /* Z は U2 にある ... */ }
}
ここで、2 つの forall が相互作用する唯一の方法は X を介することですが、X が宣言された時点では Y も Z もスコープ内にないため、その値はそれらのどちらも参照できません。
ユニバースとプレースホルダー領域要素
しかし、そのエラーはどこから来るのでしょうか。それは次のようにして起こります。領域推論コンテキストを構築しているとき、型推論コンテキストから、存在するプレースホルダー変数の数を知ることができます(InferCtxt には内部カウンタがあります)。それらのそれぞれについて、対応する普遍領域変数 !n と「領域要素」placeholder(n) を作成します。これは「何らかの未知の他の要素の集合」に対応します。!n の値は {placeholder(n)} です。
同時に、各存在変数には ユニバース も与えます(これも InferCtxt から取得します)。このユニバースは、その値にどのプレースホルダー要素が現れてよいかを決定します。たとえば、ユニバース U3 の変数は placeholder(1)、placeholder(2)、placeholder(3) を参照できますが、placeholder(4) は参照できません。推論変数のユニバースは、その値にどのリージョン要素が現れることができるかを制御するものであり、リージョン要素が現れることになると言っているわけではない点に注意してください。
プレースホルダーと outlives 制約
リージョン推論エンジンでは、outlives 制約は次の形式を持ちます。
V1: V2 @ P
ここで V1 と V2 はリージョンインデックスであり、したがって何らかのリージョン変数(全称量化または存在量化されている可能性があります)に対応します。ここでの P は制御フローグラフ内の「点」です。このセクションでは重要ではありません。この変数にはユニバースがあるので、それぞれ U(V1) および U(V2) と呼ぶことにしましょう。(実際には、ここで気にするのは U(V1) だけです。)
この制約に遭遇したとき、通常の手順は P から DFS を開始することです。歩いているノードが value(V2) に存在する限り歩き続け、それらのノードを value(V1) に追加します。return の点に到達した場合は、任意の end(X) 要素を追加します。この部分は変更されません。
しかし、その後で、V2 内のプレースホルダー placeholder(x) 要素を反復処理したいとします(それらはそれぞれ U(V2) から見えていなければなりませんが、それが真であると仮定できるはずで、チェックする必要はありません)。value(V1) がそれらの各プレースホルダー要素よりも長く生きることを保証しなければなりません。
これが起こり得る方法は 2 つあります。まず、U(V1) がユニバース x を見ることができる場合(つまり x <= U(V1) の場合)、単に placeholder(x) を value(V1) に追加して完了できます。そうでない場合は、近似しなければなりません。placeholder(x) が表す要素の集合が何であるかは分からないかもしれませんが、それに対する何らかの上界 B、つまり placeholder(x) よりも長く生きるリージョン B は計算できるはずです。今のところ、それには単に 'static を使います(すべてよりも長く生きるためです)。将来的には、ここでもっと賢くできる場合があります(実際、他のコンテキストではこれを行うコードがすでにあります)。さらに、'static はルートユニバース U0 にあるため、すべての変数から見えることが分かっています。つまり基本的に、value(V2) が、V1 からは見えない何らかのユニバース x の placeholder(x) を含むことが分かった場合、V1 を 'static に強制します。
「全称リージョン」チェックの拡張
すべての制約が伝播された後、NLL リージョン推論には最後のチェックがあります。そこでは、各全称リージョンについて計算された最終的な値を調べ、それらが「大きくなりすぎて」いないことを確認します。今回の場合は、各プレースホルダーリージョンを調べ、それが outlive することが分かっている placeholder(u) 要素だけを含んでいることを確認します。(後で、fn シグネチャ由来の全称リージョンに対して行っているように、2 つのプレースホルダーリージョン間の関係を把握し、それを考慮に入れられるようになるかもしれません。)
別の言い方をすると、「全称リージョン」チェックは次のような制約をチェックしていると考えることができます。
{placeholder(1)}: V1
ここで {placeholder(1)} は定数集合のようなものであり、V1 は !1 リージョンを表すために作った変数です。
例に戻る
ここまでは順調です。では、最初の例で何が起こるかを見ていきましょう。
fn(&'static u32) <: fn(&'!1 u32) @ P // この点 P はここでは重要ではありません
リージョン推論エンジンは、次のようなリージョン要素ドメインを作成します。
{ CFG; end('static); placeholder(1) }
--- ------------ ------- ユニバース `!1` 由来
| 'static は常にスコープ内にあります
CFG 内のすべての点。ここでは特に関連しません
常に 2 つの全称変数を作成します。1 つは 'static を表し、もう 1 つは '!1 を表します。それらを Vs と V1 と呼ぶことにしましょう。これらは次のような初期値を持ちます。
Vs = { CFG; end('static) } // U0 にあるため、他のものを参照できません
V1 = { placeholder(1) }
上記のサブタイピング制約から、次のような outlives 制約が得られます。
'!1: 'static @ P
これを処理するために、V1 の値を拡張して Vs のすべてを含めます。
Vs = { CFG; end('static) }
V1 = { CFG; end('static), placeholder(1) }
この時点で、すべての outlives 関係が満たされているため、制約の伝播は完了します。次に、コードの「全称リージョンをチェックする」部分に進み、全称リージョンが大きくなりすぎていないことをテストします。
この場合、V1 は実際に大きくなりすぎています。end('static) よりも長く生きることは分かっておらず、CFG のどの点よりも長く生きることも分かっていないため、エラーを報告します。
別の例
このサブタイピング関係についてはどうでしょうか。
for<'a> fn(&'a u32, &'a u32)
<:
for<'b, 'c> fn(&'b u32, &'c u32)
ここでは、以前と同様に、スーパータイプ内の束縛リージョンをプレースホルダーで置き換え、次のようになります。
for<'a> fn(&'a u32, &'a u32)
<:
fn(&'!1 u32, &'!2 u32)
次に、左辺の変数をユニバース U2 の存在変数でインスタンス化し、次のようになります(?n は存在変数の記法です)。
fn(&'?3 u32, &'?3 u32)
<:
fn(&'!1 u32, &'!2 u32)
次に、これをさらに分解します。
&'!1 u32 <: &'?3 u32
&'!2 u32 <: &'?3 u32
さらに分解すると、リージョン制約が得られます。
'!1: '?3
'!2: '?3
この場合、'!1 と '!2 はどちらも変数 '?3 よりも長く生きる必要がありますが、変数 '?3 は他の何かよりも長く生きることを強制されていない点に注意してください。したがって、それは単に空の要素集合として始まり、空の要素集合として終わるため、ここでは型チェックが成功します。
(これは少し驚くはずです。私も最初に気づいたときは驚きました。私たちは、2 つの引数が同じリージョンを持つことを必要とする fn である場合に、2 つの異なるリージョンを持つ引数で呼び出されることを受け入れられる、と言っています。これは直感的には健全でないように思えます。しかし実際には問題ありません。これはずっと前に Rust の issue トラッカーの この issue で説明しようとしたとおりです。理由は、たとえ 2 つの異なるライフタイムを持つ引数で呼び出されたとしても、その 2 つのライフタイムには何らかの共通部分(呼び出し自体)があり、その共通部分を、引数の共通ライフタイムとして使用する 'a の値にできるからです。-nmatsakis)
最後の例
最後にもう 1 つ例を見てみましょう。前の例を拡張して、戻り値の型を持たせます。
for<'a> fn(&'a u32, &'a u32) -> &'a u32
<:
for<'b, 'c> fn(&'b u32, &'c u32) -> &'b u32
前の例と非常によく似ているように見えますが、このケースではエラーになります。それでよいのです。問題は、2 つの引数のうちどちらかを返すことを約束する fn から、最初の引数を返すことを約束する fn へと変わってしまったことです。これは健全ではありません。どのように展開されるか見てみましょう。
まず、スーパータイプ内の束縛リージョンをプレースホルダーで置き換えます。
for<'a> fn(&'a u32, &'a u32) -> &'a u32
<:
fn(&'!1 u32, &'!2 u32) -> &'!1 u32
次に、サブタイプを存在変数(U2 内)でインスタンス化します。
```text
fn(&'?3 u32, &'?3 u32) -> &'?3 u32
<:
fn(&'!1 u32, &'!2 u32) -> &'!1 u32
そしてここで、サブタイプ関係を作成します。
&'!1 u32 <: &'?3 u32 // 引数 1
&'!2 u32 <: &'?3 u32 // 引数 2
&'?3 u32 <: &'!1 u32 // 戻り値の型
そして最後に outlives 関係です。ここで、V1、V2、V3 を、それぞれ
!1、!2、?3 に割り当てる変数とします。
V1: V3
V2: V3
V3: V1
これらの変数は、次の初期値を持ちます。
V1 in U1 = {placeholder(1)}
V2 in U2 = {placeholder(2)}
V3 in U2 = {}
ここで V3: V1 制約があるため、placeholder(1) を V3 に追加する必要があります(そして
実際にそれは V3 から可視です)。そのため、次のようになります。
V3 in U2 = {placeholder(1)}
次に V2: V3 という制約があるため、最終的に
V2 を拡大して placeholder(1) を含める必要があります(これも可視です)。
V2 in U2 = {placeholder(1), placeholder(2)}
これで制約伝播は完了ですが、outlives
関係を確認すると、V2 にこの新しい要素 placeholder(1) が含まれていることが分かるため、
エラーを報告します。