型推論を実装・改善していく４ 状態を持つ型変数生成

前回書いた通り、TaPL準拠の型推論が完全に純粋関数型なのに対して、「ユニークな型変数を作る」new_tvar関数に状態を持たせることでいちいち引数・返り値のタプルの一部として渡し回さなくてもいいようにする。

HaskellだったらStateモナドの出番なのだろうが、OCamlなので普通に破壊的代入でやってしまう。

今回のコード：

gist.github.com

変更を加えたのはnew_tvar関数そのもの、大元のtypeof関数、そしてinfer関数の三箇所。unifyやapplysubstなどは元々new_tvarを触っていなかったので変更なし。

new_tvar

before

type new_tvar = NewTVar of ty * (unit -> new_tvar)

let new_tvar =
  let rec f n () =
    NewTVar (TVar n, f (n+1))
  in f 0

after

let new_tvar =
  let i = ref 0 in
  let f () = incr i; TVar !i in
  f

元々はnew_tvarを実行すると新しい型変数と新しいnew_tvar関数が返ってくるようになっていた。次に型変数を作るときはこの新しいnew_tvarを使うことで作成される型変数のユニークさを担保していた。

新しいコードではただ単にミュータブルなrefを含むクロージャを作り、その関数をnew_tvarとして扱っている。new_tvarが呼ばれるたびにこのクロージャのrefが更新される形。

typeof

before

let typeof env new_tvar constr e =
  let (t, new_tvar, constr1) = infer env new_tvar e in
  let constr = unify (constr @ constr1) in
  let t = applysubst constr t in
  (t, new_tvar, constr)

after

let typeof env constr e =
  let (t, constr1) = infer env e in
  let constr = unify (constr @ constr1) in
  let t = applysubst constr t in
  (t, constr)

typeof関数の引数と返り値からnew_tvarが消えている。さらに関数内部の実装を見るとinferの引数と返り値も同じくnew_tvarが含まれていたのが消えている。

infer

inferは長めなのでパターンマッチのケースごとに見ていく。

EVarケース

before

let rec infer env new_tvar = function
| EVar s -> (List.assoc s env, new_tvar, [])

after

let rec infer env = function
| EVar s -> (List.assoc s env, [])

EVarのケースは単純なのであまり変わらない。返り値にnew_tvarが入っているかどうかの違いで、返り値自体の複雑さもないしnew_tvarが更新されるような場面もない。

EAbsケース

before

| EAbs(sparam, fbody) ->
  let NewTVar(tparam,new_tvar) = new_tvar () in
  let (tret, new_tvar, constr) = infer ((sparam,tparam)::env) new_tvar fbody in
  (TArrow(tparam,tret), new_tvar, constr)

after

| EAbs(sparam, fbody) ->
  let tparam = new_tvar () in
  let (tret, constr) = infer ((sparam,tparam)::env) fbody in
  (TArrow(tparam,tret), constr)

かなりスッキリしてきた。new_tvarを実行すると返ってくるのが新しい型変数のみだったり、再帰的なinferで式の型と制約を算出したり、と実際の型推論のロジックだけがコードに出てきている印象。やはり各行に１、２回new_tvarが出てくるのは処理の見通しをかなり悪化させる。

EAppケース

before

| EApp(func, arg) ->
  let (tfunc,new_tvar,constr1) = infer env new_tvar func in
  let (targ,new_tvar,constr2) = infer env new_tvar arg in
  let NewTVar(tret,new_tvar) = new_tvar () in
  let newconstr = [tfunc,TArrow(targ,tret)] in
  (tret, new_tvar, List.concat [newconstr; constr1; constr2])

after

| EApp(func, arg) ->
  let (tfunc,constr1) = infer env func in
  let (targ,constr2) = infer env arg in
  let tret = new_tvar () in
  let newconstr = [tfunc,TArrow(targ,tret)] in
  (tret, List.concat [newconstr; constr1; constr2])

私の脳のキャパシティの問題かもしれないが、各行に二回出ていたnew_tvarが消えると一気にコードのロジックがはっきりしてくる。各行を言葉で説明するのもいちいちnew_tvarに言及しなくてはいけないと非常にまどろっこしい。

この変更で効率化やロジックの大幅な簡略化などはできていないのだが、それでも「何が起きているか」がはっきり分かりやすくなったと感じる。

次回

今回の変更は少し前座的なところがあり（というかコメントも「スッキリしてきた」「はっきりしてきた」しか言ってない気がする）、段階的に破壊的代入の利用を導入していく過程の一部だ。その本丸は「型変数をミュータブルにすることでの単一化処理の効率化」である。次回はその変更を見ていく。