型推論を実装・改善していく８ Let多相型推論（後編）

前回に続いてLet多相の実装を見ていく。

generalize

前回書いたとおり、generalizeはLet式で「変数の型」を汎化する：

let rec typeof env = function
...
| ELet(svar, e, ebody) ->
  let tvar = typeof env e in
  let tgen = generalize (List.map snd env) tvar in
  typeof ((svar,tgen)::env) ebody

変数svarを束縛する対象であるe式の型tvarを汎化してtgenという新しい型にしている。(List.map snd env)で「環境に含まれているすべての変数の型のリスト」を引数の一つとして渡している。

というわけでgeneralizeの中身を見ていく：

let rec generalize env_tys ty = match ty with

例によって型に対するパターンマッチ。

まずはTVar{contents=Unbound id}なケース：

| TVar{contents=Unbound id} when not (List.exists (occursin id) env_tys) -> TVar (ref (Generic id))
| TVar{contents=Unbound _} -> ty
...

Unboundな型変数の場合、もし「環境に束縛されている型のリスト」の中に「出てこなければ」汎化。出てくるならそのまま同じ型変数として返す。

「出てこなければ」の定義が少し難しい。(List.mem ty env_tys)などと「その型変数そのものがリストに入っている」ことを検査すればいいのかとも思ったのだが、より広く探す(List.exists (occursin id) env_tys)にしてある。これだと「リストに入った型の構成要素としてこの型変数が出てくるか」も調べることになる。この処理だと環境に入っていた型すべてを一つ一つ調べていく必要があり、後述するが非常に重い処理となっている。

汎化の処理は「型変数のidはそのままで新しいGeneric idとして返す」というもの。前回の記事でも書いたとおりGenericな型変数はnew_tvarのような状態を持つ関数で作成する必要はない。

一つ考えるポイントとしては| TVar({contents=Unbound id} as tvar) ... -> tvar := Generic id; tyではない点。元の型に対して破壊的変更を加えるのか、それとも新しい型・型変数を作成するのか、気を付ける必要がある。ただしこのケースでは汎化される型変数はそもそも「ローカル」なものであることを確認しているので、どちらでも良さそう。こういう点をいちいち考える必要が出てくるのが状態と破壊的変更を導入することのデメリットである。

他のケースは簡単。

型変数がすでに他の型に単一化されていてリンクになっている場合は、そのリンク先の型を汎化する：

| TVar{contents=Link ty} -> generalize env_tys ty

すでにGenericな型変数はそのまま返す：

| TVar{contents=Generic _} -> ty

関数型は引数部分、返り値部分を個別に汎化してから新しいTArrow型として合わせて返す：

| TArrow(tparam, tret) -> TArrow(generalize env_tys tparam, generalize env_tys tret)

instantiate

typeof関数で変数式に型をつける場合、環境に入っている型をとってきてからinstantiateしている：

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

Letで導入された変数に汎化された型を対応させているのだが、その変数が実際にLetのbodyの中で使われている箇所では、使われる都度に「汎化された型」ではなく「新しく型変数が振られた具体的な型」としてその変数式を型付けする、というロジックになっている。

instantiateの内部実装を見ていく。

まずは外側：

let instantiate ty =
  let id_var_hash = Hashtbl.create 10 in
  let rec f ty = match ty with
  ...
  in f ty

instantiate自体は非再帰的な関数で、呼ばれるとまず状態をもつハッシュテーブルを作成し、それを使った再帰関数fを内部で定義して使う。fの中身は型に対するパターンマッチ。

fの中を見ていくと、一番処理が複雑なケースは当然Genericな型変数に対するもの：

  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 () in
        Hashtbl.add id_var_hash id var;
        var)

そのGeneric型変数のidに対して、すでに具体的なUnbound型変数が振られている場合はハッシュテーブルからその型変数を出してきて返す。もし振られていない場合（つまりハッシュテーブルのキーにそのGenericのidが入っていない場合）、新しい型変数をnew_tvarで作成しハッシュテーブルに追加した上で返す。

ここでうっかりハッシュテーブルをGenericなidからUnboundなidに対するものにして、try Hashtbl.find id_var_hash idをtry TVar(ref (Hashtbl.find id_var_hash id))などとしてしまうとバグる。というのも同じidを持つUnboundな型変数でも同一メモリ上になければ、後に片方が単一化でLinkに変更された時にもう片方はUnboundのまま、という状況が生じてしまう。generalizeの時も書いたが、効率化のために破壊的変更を利用することでこういうケースについて細心の注意を払う必要が出てきてしまう。

やはり他のケースは簡単。

すでにUnboundな型変数はそのまま：

  | TVar{contents=Unbound _} -> ty

リンクな場合はそのリンクを辿って再帰的にf適用：

  | TVar{contents=Link ty} -> f ty

関数型は引数部分、返り値部分を個別にf適用してから新しいTArrow型として合わせて返す：

  | TArrow(tparam, tret) -> TArrow(f tparam, f tret)

match_fun_ty、unify、occursin

単相な型推論でも出てきたヘルパ関数は、Let多相のためにほんの少しだけ変更が加わっている。

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=Unbound _} as tvar) ->
  let tparam = new_tvar () in
  let tret = new_tvar () in
  tvar := Link(TArrow(tparam,tret));
  unify tparam targ;
  tret
| TVar {contents=Generic _} -> failwith "Generic type encountered, expecting arrow or instantiated variable"

最後にTVar {contents=Generic _}のケースが加わっている。match_fun_tyに渡される型はgeneralizeされていないかinstantiateを通っているか、なはずなので、Genericな型変数に遭遇したらエラー。

unify：

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
| TVar({contents=Unbound id} as tvar), ty | ty, TVar({contents=Unbound id} as tvar) ->
  if occursin id ty then failwith "Unification failed due to occurs check"
  else tvar := Link ty
| _ -> failwith "cannot unify types"

同じく最後のケースが追加されている。少しわかりにくいがこれもGenericがどちらかに生じている場合で、これもmatch_fun_tyと同じ理屈でエラー（そもそもunifyがmatch_fun_tyからしか呼ばれない）。

occursin：

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

やはりGenericな型変数に対するケースが加わっている。occursinはgeneralizeからも呼ばれるようになっているのでmatch_fun_tyやunifyと違ってGenericに遭遇してもエラーにはならない。あくまでUnboundな型変数が型の中に出てくるかを確認する関数なのでGenericな型変数に対しては必ずfalseを返す。

改善点＆次回

これで今回の実装についてはすべての型定義・関数について解説した。

前述のとおり、このLet多相の実装で非効率さが目立つのはgeneralize関数である。型変数の汎化の時に(List.exists (occursin id) env_tys)で「現在の型環境に束縛されているすべて型の中にこの型変数が登場するか」を調べるというのは、一つの型の中に含まれるすべての型変数に関して、型環境の大きさnに対してO(n)の処理になる。この処理がLetで変数束縛するたびに走るというのは状況によっては型推論が非常に遅くなりかねない。

次回はこのgeneralizeの問題点を修正して効率化するために「型変数のレベル」という概念を導入する話。