型推論を実装・改善していく１０ レベルによるLet多相の効率化（後編）

前回に続いてLet多相にレベルを導入した実装の詳細を見ていく。

具体的にはinstantiate、match_fun_ty、unify、occursinがレベルの導入でどう影響を受けるかという点と、unifyで新しく使われるadjustlevelの理屈と実装を解説する。

instantiate

汎化された型のGenericな型変数に新しいUnboundな型変数を振って具体的な型を返すinstantiate関数。

新しく型変数を作る必要があるので当然levelが引数として必要：

let instantiate level ty =
  let id_var_hash = Hashtbl.create 10 in
  let rec f ty = match ty with
  | TVar{contents=Generic id} ->
    (try Hashtbl.find id_var_hash id
     with Not_found ->
       let var = new_tvar level in
        Hashtbl.add id_var_hash id var;
        var)
  | TVar{contents=Unbound _} -> ty
  | TVar{contents=Link ty} -> f ty
  | TArrow(tparam, tret) -> TArrow(f tparam, f tret)
  in f ty

そのレベルをnew_tvarに引数として渡す。instantiateに関しての変更はそれだけ。

match_fun_ty

関数適用の型推論のヘルパ関数であるmatch_fun_tyは引数にレベルは取らず、ほとんどのケースはレベルの導入の影響を受けない：

let rec match_fun_ty tfunc targ = match tfunc with
| TArrow(tparam,tret) -> unify tparam targ; tret
| TVar {contents=Link ty} -> match_fun_ty ty targ
...
| TVar {contents=Generic _} -> failwith "Generic type encountered, expecting arrow or instantiated variable"

唯一影響を受けるケースは「関数部分」の型がUnboundな型変数だった場合：

| TVar ({contents=Unbound(_,level)} as tvar) ->
  let tparam = new_tvar level in
  let tret = new_tvar level in
  tvar := Link(TArrow(tparam,tret));
  unify tparam targ;
  tret

型変数自体にlevelが含まれているので、それをnew_tvarに引数として渡している。なので関数型を構成する仮引数・返り値部分の型変数が、関数部分の型変数のレベルをそのまま継承することになる。それ以外の処理は変更なし。

unify

単一化処理のunifyもmatch_fun_tyと同じく、引数にレベルを取らず、ほとんどのケースは影響もない：

let rec unify t1 t2 = match t1, t2 with
| _, _ when t1 = t2 -> ()
| TArrow(tparam1, tret1), TArrow(tparam2, tret2) ->
  unify tparam1 tparam2;
  unify tret1 tret2
| TVar{contents=Link t1}, t2 | t1, TVar{contents=Link t2} -> unify t1 t2
...
| _ -> failwith "Cannot unify types"

変更があるのは片方がUnboundな型変数なケース：

| TVar({contents=Unbound(id,level)} as tvar), ty | ty, TVar({contents=Unbound(id,level)} as tvar) ->
  if occursin id ty then failwith "Unification failed due to occurs check";
  adjustlevel level ty;
  tvar := Link ty

adjustlevel level ty;の1行が追加されている。occursinがfalseで型変数の単一化が行われることになった場合、単一化する先の型に含まれる型変数のレベルが高すぎる場合は修正する必要がある。そのためにadjustlevelという関数を呼んでいる。この関数については後述するが、破壊的変更によって型変数のレベルを修正するもので、adjustlevelの返り値はunitとなる。

occursin

occursinはまったく変更なし：

let rec occursin id = function
| TVar({contents=Unbound(id1, _)} as tvar) -> id = id1
| TVar{contents=Link t} -> occursin id t
| TVar{contents=Generic _} -> false
| TArrow(tparam, tret) ->
  occursin id tparam || occursin id tret

実はGrow Your Own Type Systemの実装では次に見るadjustlevelがoccursinと混ざってoccursin_adjustlevelという関数になっていた。どちらも型の木構造を再帰的に辿っていくので、２回別々にやるより合わせてやったほうが効率がいいというのは事実。ただしたかだか定数倍。今回は実装のわかりやすさを優先した。

adjustlevel

unifyで片方がUnboundな型変数なケースでoccurs checkが通った場合に呼ばれるadjustlevel関数。

そのもっとも重要なTVar{contents=(Unbound ...)}のケース：

let rec adjustlevel level = function
| TVar({contents=Unbound(id1, level1)} as tvar) -> 
  if level < level1 then tvar := Unbound(id1, level)

「単一化する先の型に含まれている型変数」のレベルが「単一化でLinkとなる型変数」のレベルよりも高い場合、低い方のレベルに合わせる必要がある（レベルの高い方の型変数が作成されたLetの外側がその型変数に依存しているため、そのLetの箇所で汎化してはいけない）。

if level < level1 then tvar := Unbound(id1, level)というのがそのロジックの実装。level >= level1の場合は何もしない。

関数全体の返り値はunit。

それ以外のケース：

| TVar{contents=Link t} -> adjustlevel level t
| TVar{contents=Generic _} -> ()
| TArrow(tparam, tret) ->
  adjustlevel level tparam; adjustlevel level tret

型の木構造をtree walkしているだけ。前述のとおり、occursinと同じような流れでtree walkするので、定数倍効率を重視するなら二つの関数を合わせてしまうのがベスト。

まとめ

これでレベルを使った効率的なgeneralizeのあるLet多相が実装できた。

そしてひとまずHindley Milner型推論の実用に耐える＆比較的メジャーな？実装ができた。気持ちとしては「勝ったッ!第1部完!」である。

ここから追加したいのは

• unit, bool, int型
• record, variant型
• 再帰関数
• ref型
• 再帰型
• 型コンストラクタ

あたりで、つまり以前STLCに追加していったものをHM型推論にもつけていきたい。

その上で発展的なトピックとして型クラス、モジュール、bidirectional typingの実装をやっていく。