型推論を実装・改善していく２ 純粋関数型な単相型推論（中編）

前回に続いて純粋関数型な単相型推論の実装を詳細に見ていく。コードの全容はこちら。

具体的には前回見たtypeof関数：

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)

ここに出てくるnew_tvar、infer、unify、applysubstなどやそれらの中で使われているヘルパ関数などの実装を解説する、予定だったが長くなったので今回はnew_tvarとinferのみ。

new_tvar

まずはユニークな型変数を作成するために使うnew_tvar関数について。

完全に純粋な形でnew_tvarを実装するために、新しい型変数とともに「更新された自分自身を返す」再帰的な関数を定義する：

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

new_tvar内で定義されているfがTVar nと共にf (n+1)を返している。しかしこれを実現するためにはただのタプルだとOCamlの型検査を通らないのでtype new_tvar = NewTVar ...と新しい型とコンストラクタを定義している。

infer

次は特定の式の型を推論するinfer関数。

実引数として与えられる式の外部からわかる制約（主に型変数と他の型が同値である、というマッピング）は与えられていないので、inferから返ってくる型は最終的な型推論の結果ではないことに注意。

let rec infer env new_tvar = function

「式に出てくる変数とその型」のマッピングであるenvが引数の一つになっている。前述のとおりユニークな型変数を振るためのnew_tvar関数も引数として受け取り、そして最後の引数である「型を調べたい対象」である式に対してパターンマッチをする。

返り値は「式の型、次に使うべきnew_tvar関数、型制約リスト」のタプルとなっている。

パターンマッチする式の種類はSTLCと同じで変数、ラムダ抽象、関数適用の三つ。

まず変数：

| EVar s -> (List.assoc s env, new_tvar, [])

環境を調べて対応する型を返す。正しい式には自由変数が存在せず、束縛された変数は必ず型変数が振られているのでList.assocがエラーするのは正しくない式の場合のみ。ちなみに環境に入っている型は必ず型変数である（詳細は次のラムダ抽象の処理を参照）。new_tvarは使っておらずそのまま返され、新しい型制約も作成されないので空リストが返される。

ラムダ抽象：

| 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)

新しい型変数を作成し、それをラムダ抽象の引数の型として環境に入れた上で再帰的に関数のbodyの型をinferする。それでわかる関数の返り値の型を引数の型変数と合わせて関数型を作成。その関数型、更新されたnew_tvar、そして再帰的なinferから返ってきた型制約の三つをタプルとして返している。

関数適用：

| 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])

まず関数部分の式に対して再帰的なinferをして関数型tfuncを得る。

次に引数部分の式に対しても再帰的なinferをして引数の型targも得る（new_tvarは更新されたものを渡すのを忘れないようにしないといけない（ただしOCamlなのでシャドーイングで非明示的にやれている））。

関数の戻り値の型tretを表す型変数を新たに作成する。

[tfunc,TArrow(targ,tret)]は少しわかりにくいが実際には[(tfunc,TArrow(targ,tret))]と同じで、「inferから返ってきた関数型と、targとtretを組み合わせて作る関数型が同値であるという制約一つを持つ制約リスト」となっている。

最終的に返すのは「関数の戻り値の型」tret、新しいnew_tvar関数、そして上記の型制約と二つのinferから返ってきた型制約をconcatenateした型制約リストである。

次回

次回は二つの型制約のリストを合わせるunify関数、型に型制約を適用して変換するapplysubstを見ていくことで純粋関数型な単相型推論の話を終わらせる。