
2026/03/14 16:25
**Rustc を苦しめる ― 高階型(HKT)の擬似実装で挑む**
RSS: https://news.ycombinator.com/rss
要約▶
日本語訳:
Summary
この記事では、Rust が高度な汎用抽象化(例:関数型スタイルのスクリプト言語や深く再帰的なデータ構造)をサポートする際に直面する困難について説明しています。主因は、高階型(HKTs)が欠如していることと、共帰性 trait 解決が限定的である点です。
-
Rust で HKTs を試みる
著者はまず
列挙型を使って FP スクリプト言語を構築しようとしました。この列挙型はラッパー型(Ast
,Spanned
)を受け入れます。しかし、Rust には HKTs がないため、ジェネリックパラメータを型コンストラクタにすることができません。回避策として、Simple
トレイトと関連型Wrap
を導入し、Wrapper<T>
のようなマーカー構造体で実装しました。VecAsTypeConstructor -
再帰的定義がソルバーを破壊
を用いてWrap
を書き直すと、リンクリストのAst
などの再帰型がコンパイル時に “overflow evaluating the requirement … PartialEq” のようなエラーを生成します。これはCons
のような trait に対して無限証明木が生じるためであり、Rust の帰納的ソルバーでは処理できません。PartialEq -
Lean 4 が真の共帰性を示す
共帰的推論がどのように機能するかを示すため、著者は Lean 4 を用いて「任意の数は 3 で割り切れる」ことを inductive 型
を使って証明しました。証明ではS
,obtain
のタクティックと存在量化子が使用され、Rust の trait システムに欠ける洗練された論理的アプローチを示しています。exists -
Rust のソルバー環境
Rust では Chalk が trait を論理推論へマッピングします。次世代ソルバーは
のような auto‑trait を共帰的に証明できるものの、非共帰性循環にはまだ失敗します。最小例(Send
とそのFoo<W>
実装)では、Wrap
実装が循環を作り、Rust はこれを不安全として拒否します。PartialEq -
ICE がソルバーバグを露呈
次世代ソルバーは
を比較するときに内部コンパイラエラー(ICE)を引き起こし、循環 trait バウンドの取り扱いに具体的なバグがあることを明らかにしました。Foo<Noop> -
広範な影響と変更への呼び掛け
著者は Rust に HKTs やモナド、および包括的な共帰性サポートが欠如していることに苛立ち、これらのギャップが高度な型システム機能を本格的に利用する妨げになると主張しています。Lean 4、論理学、帰納/共帰推論などの学習リソースは有用だと述べつつ、記事は言語変更―段階的修正ではなく―が Rust を複雑な抽象プログラミングに適合させるために必要であると結論付けています。
欠落要素:改善された概要にはリストからのすべての重要ポイントが含まれ、例やエラー、ソルバー挙動を明示的に命名しています。元のテキストが伝える内容以外に推測は加えられていません。
本文
読書時間: 32 分
目次
- 前奏
- Rust は実際には HKT を持っていない、ということ
- 「1 + 1 は何?」―当然 Trait 要件評価のオーバーフロー
- 数学的証明と論理への逸話
- 4.1 自然数を超えた帰納法
- 4.2 カリーとハワードが共同でヤオイを斬った瞬間…
- 4.3 記事の中の自己陶酔的 Lean 4 部分
- 今度はあなたが最も好きなプログラミング言語へ戻る
- 5.1 Discord の会話に戻り、帰納循環とは何かを説明する部分
- 5.2 共帰性の大災害
前奏
2026 年 2 月 28 日、私は FP スクリプト言語を書き始めました。
最初は計算機用に単純な
Ast 列挙型から始めました。
pub enum Ast { Binary { left: Box<Ast>, operator: Token, right: Box<Ast> }, Unary { operator: Token, right: Box<Ast> }, Value { value: Value }, }
ソースのスパン情報をオプションで付与したいと考えました。
最初の試みは次のように。
pub struct Spanned<T> { inner: T, span: std::range::Range } pub struct Simple<T> { inner: T }
後にこれを汎用ラッパーへ抽象化しました。
pub struct Wrapper<T, M> { inner: T, metadata: M } type Spanned<T> = Wrapper<T, std::range::Range>; type Simple<T> = Wrapper<T, ()>;
この
Wrapper を Ast に適用しようとすると、こうなります。
pub enum Ast<W: ???> { Binary { left: Box<W<Ast>>, operator: Token, right: Box<W<Ast>> }, Unary { operator: Token, right: Box<W<Ast>> }, Value { value: Value }, }
Rust は高階型(HKT)を持たないため、
W を「型コンストラクタ」として扱うことはできません。そこで GAT とトレイトソルバーの世界へ踏み込みました。
Rust は実際には HKT を持っていない、ということ
高階型を使えばジェネリックがさらに別のジェネリックを受け取れるようになります。
struct Foo<T>(T<i32>);
ここで
T は arity 1 の「型コンストラクタ」です。Rust では 単純 なジェネリックしかサポートされておらず、型コンストラクタは存在しません。
GAT を使ってラッパー・トレイトを定義してみました。
trait Wrap { type Wrapper<T>; } struct VecAsTypeConstructor; impl Wrap for VecAsTypeConstructor { type Wrapper<T> = Vec<T>; }
これで
Foo は次のように書けます。
struct Foo<T: Wrap> { inner: T::Wrapper<i32>, } type Bar = Foo<VecAsTypeConstructor>;
動作しますが、あくまで一時的な回避策です。
「1 + 1 は何?」―当然 Trait 要件評価のオーバーフロー
小さな計算機を作り、テストを書きました。
コンパイラは次のように報告します。
error[E0275]: overflow evaluating the requirement `Wrapper<Ast<SpannedMarker>, std::range::Range<usize>>: PartialEq`
PartialEq を手動で再実装しても改善しませんでした。最小再現例では、再帰型でも同じエラーが発生します。
#[derive(Debug, PartialEq)] struct Cons<W: Wrap> { inner: W::Wrapper<i32>, next : Option<Box<W::Wrapper<Cons<W>>>>, }
Discord で議論しデバッグを重ねた結果、これは 帰納循環 の問題だと理解しました。
数学的証明と論理への逸話
カスタム帰納集合
S のすべての要素が 3 の倍数であることを証明するために帰納法を探求しました。Lean 4 を使って次のように書きました。
inductive S where | six : S | fifteen : S | step : S → S → S def S.toNat (s : S) : Nat := match s with | six => 6 | fifteen => 15 | step a b => toNat a + toNat b def Threeven (i : Nat) : Prop := ∃ k, i = 3 * k theorem three_divides_six : Threeven 6 := by exists 2 theorem three_divides_fifteen : Threeven 15 := by exists 5 theorem three_divides_threeven_plus_threeven (a b : Nat) (ha : Threeven a) (hb : Threeven b) : Threeven (a + b) := by obtain ⟨a', ha⟩ := ha obtain ⟨b', hb⟩ := hb exists a' + b' rw [ha, hb, Nat.mul_add]
最終的に次を証明しました。
theorem S.is_threeven (s : S) : Threeven s.toNat := by induction s with | six => apply three_divides_six | fifteen => apply three_divides_fifteen | step a b ha hb => rw [S.toNat] apply three_divides_threeven_plus_threeven · exact ha · exact hb
今度はあなたが最も好きなプログラミング言語へ戻る
帰納循環 vs. 共帰性
Rust のトレイトソルバーは 帰納的 です。証明木は有限でなければならないため、
List<T> のような再帰型では無限になる可能性があります。その場合 Rust は自動トレイト(Send 等)に対してのみ 共帰的 とみなし、循環を許容します。
例:
Send
List<i32>: Send ├─ i32: Send (基底ケース) └─ Option<Box<List<i32>>>: Send └─ Box<List<i32>>: Send └─ List<i32>: Send ← 循環
Send が共帰的であるため、この循環は許容されます。
共帰性の大災害
汎用ラッパーを使った最小例です。
use std::marker::PhantomData; trait Wrap { type Wrapper<T>; } #[derive(Debug, PartialEq)] struct Noop; impl Wrap for Noop { type Wrapper<T> = T; } #[derive(Debug, PartialEq)] struct Foo<W: Wrap>(PhantomData<W::Wrapper<Foo<W>>>);
Foo<Noop> は帰納的に PartialEq を実装できません。証明木には循環が含まれるためです。
Foo<Noop>: PartialEq ├─ PhantomData<Noop::Wrapper<Foo<Noop>>> └─ Noop::Wrapper<Foo<Noop>>: PartialEq ← 循環
PartialEq は共帰的ではないので、Rust は実装を拒否します。次世代ソルバーを使うと内部コンパイラエラーに至ります。
結論
- Rust は真の HKT をサポートしていません;GAT は部分的なワークアラウンドです。
- トレイト解決はデフォルトで帰納的ですが、特定の自動トレイト(
など)では共帰性が許容されます。Send - 再帰的ジェネリック型は無限証明木を引き起こすため、共帰的トレイト以外では失敗します。
これらの制約にも関わらず、トレイトソルバーを掘り下げることでタイプ理論や帰納・共帰性について深い理解が得られました。日常的な Rust プログラミングを超えたテーマです。