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

前回、前々回と見てきたLet多相はgeneralizeが非常に非効率で、環境に含まれている型すべてを調べる必要があった。

初期のML（少なくとも初期のCAML)ではこのような実装になっており、その頃の遅いコンピュータ上でも殊更HM型推論が遅いことが認識されていたようで、1988年にDidier Rémyが「レベルの導入」によって改善できることを発見したらしい。その経緯と内容についてはこちらのOleg Kiselyovの記事に非常に詳しい：

okmij.org

具体的にどういうことかというと、let x = a in bのaを型推論する時に新しく作成される型変数には、「その外側」の型推論で作成される型変数よりも高いレベルが与えられる。環境に入れるための式変数xの型を算出する場合、aの型を汎化するわけだが、その時に全称化される型変数は「外側」のレベルより高いレベルを持つ型変数のみ、となる。前回のコードだと「環境に入っているすべての型に対してoccursで調べる」という重い処理だったのが、レベルという整数の比較一回で済むようになる。

今回と次回で今まで実装してきたLet多相にレベルを導入してgeneralizeの効率を改善する。今回の実装はほぼGrow Your Own Type SystemのAlgorithm Wのコード準拠となっている（幾分か簡略化しているが）。

今回のコード：

gist.github.com

今回はtypeofとgeneralizeを見ていくところまで。instantiateやmatch_fun_tyへの変更や新しく使われているadjustlevelなどの解説は次回。

型

type ty =
| TVar of tvar ref
| TArrow of ty * ty
and tvar =
| Unbound of int * int (* intを追加 *)
| Link of ty
| Generic of int

型変数を表すtvar型のバリアントの一つUnboundが今までは| Unbound of intだった（intは型変数のidを表していた）のが| Unbound of int * intとレベルを表すintが追加された。

new_tvar

let new_tvar =
  let i = ref 0 in
  let f level = incr i; TVar(ref @@ Unbound(!i, level)) in
  f

新しい型変数を作る時には必ずlevelも引数として渡されなければいけない。

typeof

typeof関数は引数として整数型のlevelをとるように変更（トップレベルの式を型推論する場合は0を渡す）：

EVar：

let rec typeof env level = function
| EVar s -> instantiate level (List.assoc s env)

instantiateにlevelを渡す必要がある。

EAbs、EApp：

| EAbs(sparam, fbody) ->
  let tparam = new_tvar level in
  let tret = typeof ((sparam,tparam)::env) level fbody in
  TArrow(tparam,tret)
| EApp(func, arg) ->
  let tfunc = typeof env level func in
  let targ = typeof env level arg in
  match_fun_ty tfunc targ

new_tvarにも再帰的なtypeof呼び出しにもlevelを渡す。

ELet：

| ELet(svar, e, ebody) ->
  let tvar = typeof env (level+1) e in
  let tgen = generalize level tvar in
  typeof ((svar,tgen)::env) level ebody

ELet(svar, e, ebody)のeに対してtypeofをする時にtypeof env (level+1) eとレベルがインクリメントされる（levelはtypeofに引数として渡されたレベル）。なのでeを型付けする時に新たに振られる型変数はすべてlevel+1のレベルを持つ。

そのeの型を汎化する時generalizeに引数として渡すレベル、そしてLetのbodyをtypeofする時に渡すレベルは両方level（level+1ではなく）。

generalize

レベルの導入で処理が大きく変わるのはgeneralize関数、なのだが記述変更の量としては大したことがない。

まず当然levelが引数に加わる：

let rec generalize level ty = match ty with

TVar{contents=Unbound ...}のケース：

| TVar{contents=Unbound(id1,level1)} when level < level1 -> TVar(ref(Generic id1))
| TVar{contents=Unbound _} -> ty

when level < level1のケース、つまり型変数のレベルがgeneralizeの引数として渡されたレベルより高い場合のみ汎化してTVar(ref(Generic id1))を返している。それ以外は型変数をそのまま返す。

前回のコードだとここがwhen not (List.exists (occursin id) env_tys)となっていて、環境に含まれるすべての型を調べている（さらにはoccursinなので型の木構造に対して再帰的に調べていく）。これが整数二つの比較になってしまうのがこの変更のすごいところだ。

それ以外のケース：

| TVar{contents=Link ty} -> generalize level ty
| TVar{contents=Generic _} -> ty
| TArrow(tparam, tret) -> TArrow(generalize level tparam, generalize level tret)

これらに関しては再帰的なgeneralize呼び出しの時にlevelを引数として渡している以外は変更なし。

次回

今回でレベル導入の根本的な部分は解説できた。次回はinstantiate、match_fun_tyなど前回登場した関数がどう変わるかと、新しく追加された関数adjustlevelの詳細を解説する。