HM型推論
型変数の単一化を手で解いて多相型を推論する
背景： Hindley-Milner 型推論は 制約生成 → Robinson単一化 → let多相化 の3段階。各部分式に新しい型変数
α, β, ... を割り当て、関数適用 e₁ e₂ から type(e₁) = type(e₂) → α という制約を生成。Robinson のアルゴリズムで全制約を満たす最汎単一子 (mgu) を求める。
STAGE: 1/5
制約残: 0
解決: 0
失敗: 0
プログラム
期待される推論結果
制約 (Constraints)
代入 (Substitution σ)
操作
制約をクリック 選択 UNIFY 選択中の制約を1ステップ単一化 AUTO 残り全制約を自動解決 HINT 次に解くべき制約を点滅 RESET やり直し
Robinson 単一化規則：
α = α → 削除 α = τ (αが τ に出現しない) → α↦τ を σ に追加し、残り制約に適用
τ = α → 上と同様 c = c (基本型) → 削除 τ₁ → τ₂ = σ₁ → σ₂ → τ₁=σ₁, τ₂=σ₂ に分解
c = c' (異なる基本型) または α = τ with α ∈ FV(τ) → 失敗 (occurs check)
Y Lab tieup: ML系 (OCaml/Haskell) の型推論の根幹。横山研の関数型・可逆型システム研究 (R-WHILE/Janus) で型を扱う前提知識として頻出。