hs2bf - 謎の型推論
そろそろCoreに変換するのですが、このあたりで型のアノテーションの方法(全ての部分式? 型変数の扱い?)をしっかり考えておかないと後で悲惨なことになりそうです。
そこで型推論のやりかたを調べてみます。
前置き: Hindley-Milner 型システムとAlgorithm W?
Hindley-Milnerはよく耳にする言葉ですが「Sytemなんとか」も聞いたことがあるような気がします。
ちょっと調べてみると、lambda cubeというもので型システムを分類できるそうですが
Introduction to generalized type systems
残念なことに私にはさっぱり分かりません。正攻法は諦めて、情報の断片的から適当に考えるいつもの方法でいきましょう。
気を取り直して・・・
例えば
f x x
の型を調べたいとします(fとxについては何も分かっていないとします)。
部分式全てに別々の型変数を割り当てます。
x :: α0 f :: α1 e0=f x :: α2 e1=e0 x :: α3
関数の適用で型がどう変化するか考えると次のような関係が得られます。
α1=α0->α2 α2=α0->α3
問題はこれをどう機械的に解くかということです。
適当に代入を繰り返せばα1=α0->α0->α3などは分かりますが、α2と他のαとの関係などは簡単には分かりません。
ここで凄くエレガントな発想の転換をします。
- α0=なんとか
- α1=なんとか
というような答えを直接求めるのではなく、
x :: σ(α0) f :: σ(α1) e0=f x :: σ(α2) e1=e0 x :: σ(α3)
となるような変換σ::(型変数)->(型)を作って、α0...α3に適用すると考えるのです。
「余計に難しいんじゃないの?」と思うかもしれません。
確かにこのままではややこしいので、さらにU::(型の関係の連立方程式)->(変換σ)という高階の変換を考えます。
このようなUをunifierという・・・らしいです。
ちなみに先程のσはU({α1=α0->α2,α2=α0->α3})のように表せます。
さて、Uが満たす法則を考えてみましょう。
- U({})=id
- U({型変数α=型t)}+E)=U(E内のαをtで置き換える) . (αをtで置き換える)
- U({型s->型u = 型v->型w}+E)=U({s=u,v=w}+E)
1は明らかです。何の条件もないなら、それぞれの変数の型は完全に無関係です。
2は赤の部分で型変数を消去しています。消すだけでなく、青の部分で何を何で置き換えたかを覚えておきます。
3も明らかです。α->β->γ=α'->β'->γ'みたいなのはどうするのと思うかもしれませんが、実際にはα->(β->γ)=α'->(β'->γ')なので曖昧性はありません。
ようやく準備が整ったのでさっきの関係をどうにかできるか試してみましょう。
- σ=U({α1=α0->α2,α2=α0->α3})
- α1=α0->α2について2を適用: σ=U({α2=α0->α3}) . (α1をα0->α2で置き換える)
- α2=α0->α3について2を適用: σ=U({}) . (α2をα0->α3で置き換える) . (α1をα0->α2で置き換える)
- 1を適用: σ=(α2をα0->α3で置き換える) . (α1をα0->α2で置き換える)
2と3を入れ替えても同じ結果が得られます。
そしてα0...α3を代入すると
- σ(α0)=α0
- σ(α1)=α0->α0->α3
- σ(α2)=α0->α3
- σ(α3)=α0
つまり
x :: α0 f :: α0->α0->α3 f x :: α0->α3 f x x :: α3
見事に当たっています!
拡張
思いのほか長くなったので簡潔に書きます。
data
コンストラクタは関数として扱います(例 Cons::α->List α->List α)。
List αなどは
- U({List 型s = List 型t}+E)=U((s=t):E)
のようなルールを加えるだけです。
let/caseなど
(let x::α0=y::α1 in e::α2) :: α3 (case x::α0 of y ::α1 -> z ::α2 y'::α3 -> z'::α4 ) :: α5
からはそれぞれ
- [α0=α1,α2=α3]
- [α1=α3,α2=α4,α4=α5]
が得られます。
Cons x xs -> ...のようなパターンマッチも単にCons x xsという式とみなせます。
結論
とりあえず型推論の実装の目処が立ちました。これで最初の山は越えたと言えるのではないでしょうか。
