型推論バトル HM 型推論
Hindley-Milner型推論をクリックで進めて式に型を付ける
HM 型推論 — OCaml/Haskell の核技術。式から制約を生成し、
Robinson のユニフィケーションで解いて最一般型 (principal type) を得る。
本ゲームでは制約を1本ずつクリックで解き、置換の積み上げを観察します。Y Lab の OCaml 系処理系（rwhile/ROOPL/Jana）の理論基盤。
ステージ 1/8
残り制約 0
置換数 0
クリア 0
−
−
制約集合 C
置換 σ
操作
制約 (τ₁ = τ₂) をクリックすると Robinson 規則で分解／置換を行います。
α = τまたはτ = α→ 置換 σ に追加（α が τ に出現しないこと: occurs check）τ₁→τ₂ = σ₁→σ₂→τ₁=σ₁とτ₂=σ₂に分解- 同じ基本型 → 削除
- 不一致 → 型エラー