型推論器を作る(2) 単相の型推論①型取得と単一化

環境変数を保存する為のマップ用モジュールを作ります。

module M = Map.Make(String)

型取得(typeof)
型推論の基本は、式をトラバースして、型を取得する計算を行う事です。

  let rec typeof env e =
    match e with
    | Var x -> M.find x env
    | Lam(x,e) ->
      let tx = newvar() in
      let te = typeof (M.add x tx env) e in
      TArrow(tx,te)
    | App(e1,e2) ->
      let te1 = typeof env e1 in
      let te2 = typeof env e2 in
      let t = newvar() in
      t
    | Let(x,e1,e2) ->
      let te1 = typeof env e1 in
      typeof (M.add x te1 env) e2

この計算をする場合に、Appの関数呼び出しの箇所がありますが、
このApp(e1,e2)のe1の型をte1,e2の型をte2とすると、e1の型は関数の型のはずで、
e1が例えばintを文字列に変換する関数でe2の型がintならe1の型はint->stringでe2の型はintです。
そして、e1にe2を適用した型はstringになります。

te1 = int -> string
te2 = int
t = string

です。

te2 -> t = te1

という方程式が作れる事に注目しましょう。
te2 -> tは TArrow(te2, t)と書けるので、仮にTArrow(te2, t)とte1の型は同じにしてくれる関数unifyというものがあったとすれば、

    | App(e1,e2) ->
      let te1 = typeof env e1 in
      let te2 = typeof env e2 in
      let t = newvar() in
      unify t (TArrow(te2, t));
      t

と書く事ができます。

このunifyは日本語では単一化といって、以下のように実装出来ます。

  let rec unify t1 t2 =
    match (t1, t2) with
    | (t1,t2) when t1 == t2 -> ()
    | (TVar({contents=Unbound _} as tv), t)
    | (t, TVar({contents=Unbound _} as tv)) ->
      tv := Link t
    | (TVar({contents=Link t1}), t2)
    | (t1, TVar({contents=Link t2})) ->
      unify t1 t2
    | (TArrow(l1,l2),TArrow(r1,r2)) ->
      unify l1 r1;
      unify l2 r2

t1とt2が同じなら何もしません。

    | (t1,t2) when t1 == t2 -> ()

どちらかがまだ型が割り当てられていなければ、片方に、もう片方をコピーします。

    | (TVar({contents=Unbound _} as tv), t)
    | (t, TVar({contents=Unbound _} as tv)) ->
      tv := Link t

コピーした結果がどちらかに入っていたら、その中身を単一化します。

    | (TVar({contents=Link t1}), t2)
    | (t1, TVar({contents=Link t2})) ->
      unify t1 t2

共に関数の型なら、 その中身をチェックします。

    | (TArrow(l1,l2),TArrow(r1,r2)) ->
      unify l1 r1;
      unify l2 r2

最も簡単な単一化はこれだけで行う事が出来ます。