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

「型推論を実装・改善していく３　純粋関数型な単相型推論（後編）」で書いたとおり、型推論のTaPL実装は副作用を使わない純粋関数型なもので、型制約のリストを正しく変換するunify関数がリストの長さnに対してO(n**2)な処理になっている。

その非効率さを改善するよく知られた手法として「型変数をミュータブルにし、型同士の単一化を破壊的代入で行う」というやり方がある。型変数が登場するすべてのところを探していちいち変換するのではなく、型変数の持つrefを更新することですべての箇所から単一化が自動的に見えるようにするというもの。ちなみにこれはHM型推論の初出であるMilnerの論文でも「実際に使うとしたらこうだよね」とAlgorithm Jの名前で紹介されている手法なので、初期のMLでもこういった実装になっていたと思われる。

今回は前回までのコードをベースに、Grow your own type systemというレポジトリのAlgorithm W実装を参考にしながら「ミュータブルな型変数に対して破壊的変更を行う効率的な単相型推論」を実装していく。

今回のコード：

gist.github.com

例によって長くなったので２回にわける。今回は型（特に型変数）をどう表現するかと、大元のtypeof関数の全体的な流れを見ていく。unifyなどの実装は次回。

型

今までどおり型変数と関数型のみの型システムだが、型変数の実装が変わる：

type ty =
| TVar of tvar ref
| TArrow of ty * ty
and tvar =
| Unbound of int
| Link of ty

今まではTVar of intだったのがTVar of tvar refになっており、type tvar = Unbound of int | Link of tyだ。

Unboundが今までの型変数に相当していて、例えば型変数TVar 5はTVar (ref (Unbound 5))となる。OCamlだとrefはレコードで実装されているので実際にはTVar {contents=Unbound 5}のようにパターンマッチする。

Linkは型変数'aが他の型Bと同値であることがわかった場合、型変数がBを指し示すようにするためのもの。

match t with
...
| TVar tv -> ...; tv := Link new_t

のように使う。

new_tvar

新しい型変数を作るnew_tvar：

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

前回はTVar !iで型変数を作っていたのがTVar(ref @@ Unbound !i)になっている。

typeof

純粋関数型な実装と同様、型推論・型検査を行う大元の関数であるtypeof：

let rec typeof env = function
| EVar s -> List.assoc s env
| EAbs(sparam, fbody) ->
  let tparam = new_tvar () in
  let tret = typeof ((sparam,tparam)::env) fbody in
  TArrow(tparam,tret)
| EApp(func, arg) ->
  let tfunc = typeof env func in
  let targ = typeof env arg in
  match_fun_ty tfunc targ

実装の内容はかなり様相が変わっている。

まず「型制約」という概念がなくなっている。「型同士の同値関係を一旦データとして出力してから、そのデータをもとに特定の型を変換する」のではなく「同値関係がわかった時点で型変数を破壊的に変更する」というやり方に変わっているのが理由。（ただし「制約をすべて出力してから、そのデータをもとに破壊的変更を順次加えていく」という実装のやり方もあるとは思う）

型制約がなくなった結果、typeof関数の中でinfer、unify、applysubstと明示的にステップをわける必要もなくなった。なので純粋関数型な実装ではinferでやっていた式に対するパターンマッチを直接typeofでやるようになっている。

個別のケースを見ていく。

式としての変数EVar：

| EVar s -> List.assoc s env

環境の中で変数に対応する型を探す。純粋関数型版のinferと同じロジック。

ラムダ抽象のEAbs：

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

引数の型として新しい型変数tparamを作り、引数の変数とその型変数を環境に加えてbody式に対して再帰的なtypeof適用。それで返ってくる型をラムダ抽象の返り値の型tretとして、ラムダ抽象全体の型として関数型TArrow(tparam, tret)を返す。

関数適用のEApp：

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

関数部分の型tfuncと引数部分の型targをそれぞれtypeofの再帰的適用で算出。それらをヘルパ関数match_fun_tyに渡して返ってきた「関数適用の返り値の型」を返す。

次回

今回見てきたtypeof関数のコードでは型変数を単一化する箇所が出てこなかった。実はこの簡単な言語においては、単一化の処理はすべてmatch_fun_tyに隠蔽されている。次回はmatch_fun_tyとその中で使われているunify、occursin関数を見ていく。