Chalk ベースのトレイト解決

Chalk は Rust 向けの実験的なトレイトソルバーであり、 ( 2022 年 5 月時点で) Types team によって開発中です。 その目標は、実装が難しい多くのトレイトシステム機能やバグ修正 (例: GAT や specialization) を可能にすることです。新しいソルバーの開発に 協力したい場合は、rust-lang Zulip の #t-types チャンネルに立ち寄って、 ぜひ声をかけてください！

新しいスタイルのトレイトソルバーは、chalk で行われた作業に基づいています。Chalk は Rust のトレイトシステムを、論理プログラミングの観点から明示的に捉え直します。これは、 Rust コードを一種の論理プログラムへ「低水準化」し、そのプログラムに対して クエリを実行できるようにすることで行われます。

ここで重要な観察は、Rust のトレイトシステムが基本的には一種の論理であり、 標準的な論理推論規則に対応付けられるということです。その後、たとえば Prolog ソルバーが動作する方法と非常によく似た形で、それらの推論規則の解を 探すことができます。実際には、Prolog の規則 (Horn 節とも呼ばれます) を そのまま 使用することはできず、もう少し表現力の高い変種が必要であることが わかっています。

Chalk 自体については、 Chalk book セクションでさらに詳しく読むことができます。

進行中の作業

新しいスタイルのトレイト解決の設計は、2 つの場所で行われています。

chalk。chalk リポジトリは、トレイトシステムの新しいアイデアや設計を 実験する場所です。

rustc。論理規則に満足したら、それらを rustc に実装する段階へ進みます。 struct、trait、impl 宣言を、rustc の lowering モジュール内で論理推論規則へ 対応付けます。