型推論を実装・改善していく６ ミュータブルな型変数を使った単相型推論（後編）

前回に続いてミュータブルな型変数に対する破壊的代入で実装する効率的な単相型推論について見ていく。今回はtypeof関数の内部で使われているmatch_fun_ty、そしてunify, occursinの実装について。

match_fun_ty

前回見たとおり、型推論・型検査を行うtypeof関数の「関数適用」ケースでmatch_fun_tyというヘルパ関数が使われている：

let rec typeof env = function
...
| EApp(func, arg) ->
  let tfunc = typeof env func in
  let targ = typeof env arg in
  match_fun_ty tfunc targ

match_fun_tyが呼ばれる前にtfuncとtarg、つまり関数部分と引数部分それぞれの型を再帰的なtypeof呼び出しで算出した上で、それらを引数としてmatch_fun_tyに与えている。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=Unbound _} as tvar) ->
  let tparam = new_tvar () in
  let tret = new_tvar () in
  tvar := Link(TArrow(tparam,tret));
  unify tparam targ;
  tret

tfuncに対してパターンマッチしている。個別のケースを見ていく。

| TArrow(tparam,tret) -> unify tparam targ; tret

tfuncが関数型だった場合、その関数型の仮引数部分の型tparamと「実引数の型」targをunify関数で単一化し、それに成功したなら関数型の返り値部分の型を「関数適用の結果の型」として返す。（unifyについては後述）

| TVar {contents=Link ty} -> match_fun_ty ty targ

tfuncがすでに他の型に単一化されている型変数の場合、単一化された対象の型へのリンクを辿って、その型をtfuncだと考えて再帰的にmatch_fun_tyを呼び出す。

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

tfuncが単一化されていない型変数の場合、新しい型変数をそれぞれ仮引数と返り値の型として作成し、それらを組み合わせた関数型を作成。tfuncはその新しい関数型にリンクするように破壊的変更し、仮引数と実引数の型をunifyで単一化し、返り値の型であるtretを「関数適用の結果の型」として返す。

unify

単一化関数unifyは二つの型が同値であると扱えるかを調べ、扱えるなら正しく型変数をリンクに更新してunitを返す。扱えないならエラー。

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

片方の型が単一化されていない型変数であれば、まずその型変数がもう片方の型の中に出てこないかをoccursin関数で調べて（再帰的な型に対する型推論はサポートされていない）、大丈夫なら型変数の中身をもう片方の型へのリンクに更新する。

occursin

ある型変数が別の型の中に出てこないか確認するoccursin関数。「Grow Your Own Type System」の実装では（他にもいろいろ追加で処理をしているが根本的には）「型変数がある型に登場した場合はエラー、登場しない場合はunitを返す」という実装になっている。しかし関数の名前がoccursinなので「型変数がある型に登場した場合は真、登場しない場合は偽を返す」として、エラーを投げるのはoccursinが使われているunifyの中でのことにしたい。

実装は例によって型に対するパターンマッチ：

let rec occursin id = function
| TVar{contents=Unbound id1} -> id = id1

「別の型」が単一化されていない型変数ならidの比較。

| TVar{contents=Link t} -> occursin id t

単一化された型変数なら単一化された先の型に対して再帰的にoccursin適用。

| TArrow(tparam, tret) -> occursin id tparam || occursin id tret

関数型なら仮引数部分と返り値部分に対して別々にoccursin検査。どちらか片方でも含まれていれば全体も真なので||を使って組み合わせている。

まとめ＆Union Findについて

これで「ミュータブルな型変数による単一化の効率的実装」はおしまい。

この「ミュータブルな型変数に破壊的変更を加えて単一化する」というコードはアルゴリズム的にはdisjoint set forestに対するunion findだ。個別の型をノード、同値な型を集合と考えて、いかに効率的に同値な集合を算出していくか、という問題に落とし込んでいる。

その観点から言うとこの実装はまだ問題がある。一つの集合を表すtreeが非常に深くなる可能性がある点だ。型変数1が型変数2に単一化され、型変数2が型変数3に単一化され・・・と長い列ができた場合、型変数1の最終的な型を調べるのにはその長いリンクを一つ一つ辿っていく必要がある。union findだとそれをうまく処理して一つのtreeが浅く広くなるようにする（例えばリンクを辿っていく段階でそれまでの型変数をすべて保持しておいて、最終的なノードに到達したらすべての型変数のリンク先を更新する、など）。型推論でこれが実際に問題になるかはわからないが、もし今回の実装でも型推論の効率が悪かったらこのようなunion findの典型的な改善を考えるのもありだろう。

次回

次回からHindley Milner型推論のキモであるLet多相を実装する。