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

型推論

型推論とは、式の型を自動的に検出するプロセスです。

これにより、Rust では型注釈を少なく、またはまったく書かずに済むため、ユーザーにとって扱いやすくなります。

fn main() {
    let mut things = vec![];
    things.push("thing");
}

ここでは、things にプッシュしている値により、things の型は Vec<&str> であると推論されます。

型推論は標準的な Hindley-Milner（HM）型推論アルゴリズムに基づいていますが、サブタイピング、リージョン推論、高階ランク型に対応するために、さまざまな方法で拡張されています。

用語に関する注記

推論変数を指すために ?T という表記を使用します。これは存在変数とも呼ばれます。

「リージョン」と「ライフタイム」という用語は同じ意味で使用します。どちらも &'a T における 'a を指します。

「束縛リージョン」という用語は、関数シグネチャ内で束縛されるリージョンを指します。たとえば、for<'a> fn(&'a u32) における 'a です。リージョンが束縛されていない場合、そのリージョンは「自由」です。

推論コンテキストの作成

推論コンテキストは、たとえば次のようにして作成します。

let infcx = tcx.infer_ctxt().build();
// ここで推論コンテキスト `infcx` を使用します。

infcx の型は InferCtxt<'tcx> であり、構築元の tcx と同じ 'tcx ライフタイムを持ちます。

tcx.infer_ctxt メソッドは実際にはビルダーを返します。つまり、infcx が作成される前に、いくつかの種類の設定を行うことができます。詳細については InferCtxtBuilder を参照してください。

推論変数

推論コンテキストの主な目的は、多数の推論変数を保持することです。これらは、正確な値がまだわかっていないものの、型チェックを実行するにつれて明らかになる型やリージョンを表します。

H-M 型システムにおける単一化の基本的な考え方や、Prolog のような論理型言語に詳しい場合、これは同じ概念です。そうでない場合は、H-M 型推論がどのように機能するかについてのチュートリアル、あるいは Chalk プロジェクトにおけるunification in the Chalk projectに関するこのブログ記事を読むとよいかもしれません。

全体として、推論コンテキストは 5 種類の推論変数を格納します（ 2023 年 3 月時点）。

  • 型変数。これには 3 種類があります。
    • 一般型変数（最も一般的なもの）。これは任意の型と単一化できます。
    • 整数型変数。これは整数型とのみ単一化でき、22 のような整数リテラル式から生じます。
    • 浮動小数点型変数。これは浮動小数点型とのみ単一化でき、22.0 のような浮動小数点リテラル式から生じます。
  • リージョン変数。これはライフタイムを表し、至るところで生じます。
  • const 変数。これは定数を表します。

すべての型変数はほぼ同じように機能します。新しい型変数を作成すると、未解決の型 ?T を表す Ty<'tcx> が得られます。その後、等価性やサブタイピングなど、推論器がサポートするさまざまな操作を適用できます。その結果として、その ?T が特定の値にインスタンス化（または束縛）される可能性があります。

リージョン変数はやや異なる動作をし、別のセクションで後述します。

等価性 / サブタイピングの強制

型推論器で実行できる最も基本的な操作は等価性です。これは 2 つの型 T と U が同じであることを強制します。等価制約を追加する推奨方法は、概ね次のように at メソッドを使用することです。

infcx.at(...).eq(t, u);

最初の at() 呼び出しは、多少のコンテキスト、つまりなぜこの単一化を行うのか、どの環境で行うのかを提供し、eq メソッドが実際の等価制約を実行します。

もの同士を等価にすると、それらが厳密に等しいことを強制します。等価化は InferResult を返します。Err(err) を返した場合、等価化は失敗しており、内包される TypeError が何が問題だったのかを示します。

成功の場合は、もう少し興味深いものです。eq の「主要な」戻り値の型は () です。つまり、成功した場合、特に関心のある値は返しません。むしろ、型変数を制約するなどの副作用のために実行されます。ただし、実際の戻り値の型は () ではなく、InferOk<()> です。InferOk 型は追加のトレイト義務を運ぶために使用されます。これらが満たされるようにするのはあなたの役割です（通常は、それらを充足コンテキストに登録します）。この点に関する背景については、trait chapterを参照してください。

同様に、infcx.at(..).sub(..) を通じてサブタイピングを強制できます。上記と同じ基本概念が適用されます。

等価性を「試す」

場合によっては、2 つの型をエラーなしで等価にすることが可能かどうかを知りたいことがあります。これは infcx.can_eq（サブタイピングの場合は infcx.can_sub）でテストできます。これが Ok を返す場合、等価性は可能です。ただし、いずれの場合も、副作用はすべて巻き戻されます。

ただし、これらのメソッドの成功または失敗は常にリージョンを法としていることに注意してください。つまり、2 つの型 &'a u32 と &'b u32 は、たとえ 'a != 'b であっても、can_eq に対して Ok を返します。これは、リージョン制約を解く方法の「2 フェーズ」の性質から生じます。

スナップショット

前のセクションの can_eq で説明したように、一連の操作を実行し、その後でそれらの副作用をロールバックできると便利なことがよくあります。これはさまざまな理由で行われます。その 1 つはバックトラックできるようにするためであり、どのパスを取るか決定する前に複数の可能性を試すことができます。もう 1 つは、一連の小さな変更がアトミックに行われるか、まったく行われないかを保証するためです。

これを可能にするため、推論コンテキストは snapshot メソッドをサポートしています。これを呼び出すと、実行する操作によって発生する変更の記録を開始します。完了したら、それらの変更を取り消す rollback_to を呼び出すか、変更を永続化する confirm を呼び出すことができます。スタックのような規律に従う限り、スナップショットはネストできます。

スナップショットを直接使用するよりも、より高レベルのパターンをカプセル化した commit_if_ok や probe のようなメソッドを使用すると役立つことがよくあります。

サブタイピング義務

議論する価値があるものの 1 つに、サブタイピング義務があります。?T <: i32 のように 2 つの型をサブタイプ関係に強制する場合、それらを等価制約に変換できることがよくあります。これは Rust のサブタイピングの概念がかなり限定的であることに由来します。したがって、上記の場合、?T <: i32 は ?T = i32 と等価です。

ただし、場合によってはより慎重になる必要があります。たとえば、リージョンが関与する場合です。したがって、?T <: &'a i32 がある場合、まず &'a i32 をリージョン変数を持つ型、つまり &'?b i32 に「一般化」し、その後 ?T をそれと単一化します（?T = &'?b i32）。次に、この新しい変数を元の境界と関連付けます。

&'?b i32 <: &'a i32

これにより、'?b: 'a というリージョン制約（後述）が生じます。 最後に興味深いケースとして、?T <: ?U のように、2 つの未束縛の型変数を関連付ける場合があります。この場合、処理を進めることができないため、Subtype(?T, ?U) というオブリゲーションをキューに入れ、InferOk メカニズムを通じてそれを返します。?T または ?U についてより多くの詳細が判明したときに、再度試す必要があります。

リージョン制約

リージョンは型とはやや異なる方法で推論されます。先行して統一を行うのではなく、処理の過程で制約を収集するだけで、リージョンを解決しようとすることは（ほとんど）ありません。これらの制約は「outlives」制約の形を取ります。

'a: 'b

実際には、コードはこれらをサブリージョン関係として扱う傾向がありますが、考え方は同じです。

'b <= 'a

（「verifys」など、他にもさまざまな種類の制約があります。詳細については、region_constraints モジュールを参照してください。）

あるケースでは、ある程度の先行した統一を行います。2 つのリージョンの間に等価制約がある場合、

'a = 'b

その事実を統一テーブルに記録します。その後、opportunistic_resolve_var を使用して 'b を 'a に変換できます（またはその逆も可能です）。これは、固定点アルゴリズムの停止性を保証するために必要になることがあります。

リージョン制約の解決

リージョン制約は、型検査の最後の最後、つまり他のすべての制約が判明し、他のすべてのオブリゲーションが証明された後にのみ解決されます。現在、リージョン制約を解決する方法は 2 つあります。レキシカルと非レキシカルです。最終的には 1 つだけになります。

ここでの例外は、トレイト解決中に使用され、高ランクリージョンを含むリージョン制約に依存するリークチェックです。ルートユニバース内のリージョン制約（つまり for<'a> から生じたものではない制約）は、トレイトシステムに影響を与えてはなりません。これらのリージョンはコード生成時にすべて消去されるためです。

レキシカルなリージョン制約を解決するには、resolve_regions_and_report_errors を呼び出します。これにより、リージョン制約プロセスが「クローズ」され、lexical_region_resolve コードが呼び出されます。これが完了すると、それ以降に等価関係を設定したり、サブタイピング関係を作成したりしようとすると ICE が発生します。

NLL ソルバー（実際には MIR 型チェッカー）は、少し異なる方法で処理します。トレイト解決には canonical query を使用し、その最後に take_and_reset_region_constraints を使用します。これにより、canonical query の間に追加されたすべての outlives 制約が抽出されます。これは、NLL ソルバーが、どのリージョンが互いに outlive するかだけでなく、どこでそうなるかも知る必要があるためです。最後に、NLL ソルバーは get_region_var_infos を呼び出し、すべてのリージョン変数をソルバーに提供します。

レキシカルリージョンの解決

レキシカルリージョンの解決は、最初に各リージョン変数に空の値を割り当てることで行われます。その後、各 outlives 制約を繰り返し処理し、固定点に到達するまでリージョン変数を拡張します。リージョン変数は、リージョン束上の最小上界関係を使用して、かなり素直な方法で拡張できます。