型システム実装幕間２ unifyとoccurs check、adjust levelについて

match_fun_tyなどのヘルパ関数をなくす是非を考えていて「型変数を新しく作成して使うコストは低いのだから（破壊的代入でリンクをアップデートしてるので管理する型変数の数が増えても処理が重くならない）、match_fun_tyなどでパターンマッチせずTArrow(tvar1, tvar2)を新しく作って単一化するのでもそこまで非効率ではないのでは？」と多少は楽観視していたのだが。

よく考えると「新しく作る」「管理する」のは低コストだが「単一化」が高コストだった。新しく作った型変数と他の型の単一化で何故コストがかかるかというと、単一化の内部で行われるoccurs checkとadjust levelでもう片方の型のすべてのノードを再帰的に辿るからだ。

「たった今作成した型変数なんだからoccurs checkいらないだろう」ということでoccurs check（とadjust level）を省略したunify_skipという関数を新たに定義してみた：

let rec unify_skip t1 t2 = match t1, t2 with
| _, _ when t1 = t2 -> ()
| TArrow(tparam1, tret1), TArrow(tparam2, tret2) ->
  unify_skip tparam1 tparam2; unify_skip tret1 tret2
| TVar{contents=Link t1}, t2 | t1, TVar{contents=Link t2} -> unify_skip t1 t2
| TVar{contents=Unbound(_,level1)}, TVar{contents=Unbound(_,level2)} ->
  if level1 < level2 then tvar2 := Link t1 else tvar1 := Link t2
| TVar({contents=Unbound(id,level)} as tvar), ty | ty, TVar({contents=Unbound(id,level)} as tvar) ->
  tvar := Link ty
| TTuple ts1, TTuple ts2 -> List.iter2 unify_skip ts1 ts2
| TRecord lts1, TRecord lts2 ->
  if List.map fst lts1 != List.map fst lts2 then failwith "Cannot unify records with mismatched labels";
  List.iter2 unify_skip (List.map snd lts1) (List.map snd lts2)
| TVariant lts1, TVariant lts2 ->
  if List.map fst lts1 != List.map fst lts2 then failwith "Cannot unify variants with mismatched labels";
  List.iter2 unify_skip (List.map snd lts1) (List.map snd lts2)
| TRef t1, TRef t2 -> unify_skip t1 t2
| TList t1, TList t2 -> unify_skip t1 t2
| _ -> failwith "Cannot unify types"

typeofで使ってみる：

let rec typeof env level = function
...
| EApp(func, arg) ->
  let tparam = new_tvar level in
  let tret = new_tvar level in
  unify_skip (typeof env level func) (TArrow(tparam, tret));
  unify (typeof env level arg) tparam;
  tret

しかしよく考えるとadjust levelしていないのは問題になる。今作った型変数だからoccursチェックは省略できるが、adjust levelしないといけないんだったらどっちみち型のノードをすべて確認する必要があり、大した効率化にはならない。

というかそもそもlet tparam = new_tvar levelで渡しているlevel自体が間違っている疑いが出てきた（match_fun_tyでは既存の型変数からlevelを取ってきている）。そうするとmatch_fun_tyといった関数の役割は「効率化」だけではなく「型変数作成時に正しいlevelを伝播する」という機能もあるということになり、軽々しく省略してはいけないものということになる。

なのでこの「単純化」は失敗だと言えそう。その代わりmatch_fun_tyなどの重要性がわかった。

今回のコードはここ