型推論を実装・改善していく３ 純粋関数型な単相型推論（後編）
前々回、前回に続いて純粋関数型な単相型推論の実装を詳細に見ていく。コードの全容はこちら。
型推論・型検査の関数であるtypeof：
let typeof env new_tvar constr e = let (t, new_tvar, constr1) = infer env new_tvar e in let constr = unify (constr @ constr1) in let t = applysubst constr t in (t, new_tvar, constr)
この後半で使われているunifyとapplysubstを見ていく。
unifyはinferから返ってくる型制約のリストを処理してapplysubstに渡せる形に変換する関数。（正確には型制約のリストはtypeofの引数としても渡されるが、こちらは基本的に空リスト（よりリッチな言語の場合はビルトイン関数の型制約があらかじめ渡される））
applysubstはある型に対して「unifyで処理された型制約のリスト」を順次に適用して変換する。その結果がtypeofに渡された式の型だと判定される。
unify
unify関数は型制約のリストに対する再帰的なパターンマッチでできている。型制約のリストはtype constr = (ty * ty) listである。
unifyの返り値もまた(ty * ty) listだが、タプルの最初のtyは必ず型変数となる。引数の(ty * ty)が双方向的な「この二つの型は同値である」という主張なのに対して、返り値の(ty * ty)は「最初の型変数は2番目の型に変換される」という方向性のあるマッピングである。
let rec unify = function | [] -> [] | (TVar s1, TVar s2)::rest when s1 = s2 -> unify rest
まったく同じ型変数同士に関する型制約は自明として無視される。
どちらか片方（あるいは両方）が型変数だが、まったく同一ではないケース：
| (t, TVar s)::rest | (TVar s, t)::rest -> if occursin s t then failwith "Unification failed due to occurs check" else List.append (unify (substinconstr s t rest)) [(TVar s, t)]
「型変数'aが型Bと同値である」という制約を考えるとき、型Bの中に型変数'aが出てくるような再帰性があった場合型推論がうまくいかない。なのでoccurs checkを行なって「型Bの中に型変数'aが出てこない」ということを確認する必要がある（occursin関数の実装は後で見ていく）。
再帰性がないことが確認できた場合、残っている型制約すべてに対してsubstinconstr関数（この関数についても後ほど詳細を見ていく）で「この型制約の型変数と型」の変換を行った上で再帰的にunifyを行い、その結果の最後に「この型制約の型変数と型」をappendしている。
この部分はかなり効率が悪い。残った型制約のリストに対してO(n)な処理を行なっているのでunifyがO(n**2)になる。また再帰的にunifyを使った結果に[(TVar s, t)]をappendしているというのも再度O(n)な処理で、さらに非末尾再帰的だ。この部分はaccumulatorを使えばO(1)な末尾再帰として解決できるはずだが、どうせsubstinconstrでO(n**2)になってるんだから、と開き直っているのだろうか・・・。
最後に関数型同士の型制約に関するケース：
| (TArrow(tparam1,tret1),TArrow(tparam2,tret2))::rest -> unify ((tparam1,tparam2)::(tret1,tret2)::rest)
引数の型同士、戻り値の型同士、と二つの型制約に分解した上で再帰的にunifyを呼び出す。
現在扱っている言語の型が型変数と関数型しかないので、以上ですべてのケースが網羅された。
unifyの返す結果は入力の順番にかなり左右される。
例えば
unify [(TVar "a", TVar "b); (TVar "c", TArrow(TVar"b", TVar "d"))] ---> [(TVar "c", TArrow(TVar"a", TVar "d")); (TVar "a", TVar "b)]
となる（関数型の中の型変数が"b"から"a"に変換されている）のだが、順番が逆の場合
unify [(TVar "c", TArrow(TVar"b", TVar "d")); (TVar "a", TVar "b)] ---> [(TVar "a", TVar "b); (TVar "c", TArrow(TVar"b", TVar "d"))]
変換が行われずに返ってくる。
実際には入力の順番によってunifyが失敗することはないのだが、そのかわり出力の順番を正しく扱う必要は出てくる。後で詳しく見ていくapplysubst関数で使われるわけだが、まずList.revをしてから型に対して順次に変換をしていかなくてはいけない。
ちなみに何故わざわざList.revしなくてはいけないような順番にしているのかがわからない（この部分はTaPL準拠）。unifyの| (t, TVar s)::rest | (TVar s, t)::rest ->のケースでわざわざList.append (unify (substinconstr s t rest)) [(TVar s, t)]などとしているからList.revが必要なのであって、素直に(TVar s, t)::(unify (substinconstr s t rest))を返していればいいのではないかと思うのだが・・・。
それではここまでで登場したヘルパ関数を見ていく。
occursin
ある型変数'aを別の型Bと同値だと見做すためには、'aがBの中に登場しないことを確認する必要がある（そうでないと型推論が壊れるため）。その検査をするoccursin関数：
let rec occursin s = function | TVar s2 -> s = s2 | TArrow(tparam,tret) -> occursin s tparam || occursin s tret
型の種類が二つしかないのでパターンマッチが非常に簡単。ちなみに第一引数は型ではなく型変数の中の文字列。
substinconstr
型制約のリストconstrに対して、ある型変数が起きる箇所をすべて別の型に入れ替えるsubstinconstr関数（Substitute inside Constraintsの略）：
let substinconstr s t constr = List.map (fun (t1,t2) -> (substinty s t t1, substinty s t t2)) constr
型制約ひとつひとつの右辺、左辺ともにsubstinty関数で型変数TVar sを型tに入れ替える。
substinty
ある型に出てくる特定の型変数を特定の型に入れ替えるsubstinty（Substitute inside Type）関数：
let rec substinty s t t1 = match t1 with | TVar(s1) -> if s = s1 then t else t1 | TArrow(tparam1,tret1) -> TArrow(substinty s t tparam1, substinty s t tret1)
やはり型の種類が二つしかないのでパターンマッチが非常に簡単。
applysubst
最後にinferから返ってきた型にunifyで用意した型制約を適用し、単一化された形の型を返すapplysubst関数：
let applysubst constr t = let f t = function | (TVar(s),t1) -> substinty s t1 t | _ -> assert false in List.fold_left f t (List.rev constr)
まず型に個別の型制約を適用する内部関数fを定義している。unifyを通した型制約はタプルのfstが型変数であるはずなので、パターンマッチで確認してエラーケースはassert falseになっている。fの正常系ではunifyの解説でも出てきたsubstinty関数で型の中の型変数を違う型に変換している。
その上でList.fold_leftで型制約のリストを次々とtに（fを使って）適用していく。前述のとおり、unifyから返ってきた型制約リストは逆順に適用する必要があるのでList.revしている。
まとめ＆次回
これでTaPL準拠（ほぼ）の純粋関数型な単相型推論の実装は完了。
コードを見てきて感じる問題点としては
などがあり、これらを改善していく。
次回は手始めにnew_tvarを破壊的に変更される状態を持つ関数にすることでコードを少しスッキリさせる。
