型推論書いたった

　タイトルの通り、OCamlでOCamlのサブセットの型推論を書いたので、その事について纏めておこうと思います。
　対象とする型システムはプログラミング言語の基礎概念に載っているTypingML4ですが、プログラミング言語の基礎概念を持っていないものの型付け規則等を知りたい方はサポートページを探して下さい。

プログラミング言語の基礎概念 (ライブラリ情報学コア・テキスト)

ちなみに今回型推論を実装した型システムは単相なので

let s = fun x -> fun y -> fun z -> x z (y z) in
let k = fun x -> fun y -> x in
s k k

こういう式に型を付けられませんがあしからず。

　プログラミング言語の基礎概念に書かれていたML風擬似コードでは、型付けを行う関数が型環境と式を引数に取り型代入と式の型の組を返すように定義されていました。こういう関数はStateモナドを使いたい所ですが、OCamlにはモナドよりもっと手軽に扱えるものが有るはずです。そう、みんな大好き副作用！

型変数の表現

　型を表現する型の宣言を見ると、型変数が参照を用いて表されていることが分かります。

type t =
  | Int
  | Bool
  (* 型変数 *)
  | Var of t option ref
  | Fun of t * t
  | List of t

関数の引数のようにすぐには決定できない型が出現した場合には一旦Var (ref None)を返しておいて、型が確定した時点でSome (確定した型)を代入します。ただし、等価な型が物理的にも等価になるように注意が必要です。

単一化

(* 方程式に解が存在するか確かめる *)
let rec occur var = function
  | Var (var') when var == var' -> true
  | Int | Bool | Var { contents = None } -> false
  | Fun (t1, t2) -> occur var t1 || occur var t2
  | Var { contents = Some (t) } | List (t) -> occur var t

(* 型を単一化する *)
let rec unify t1 t2 =
  match t1, t2 with
  | Int, Int | Bool, Bool -> ()
  | Var { contents = Some (t1) }, t2
  | t2, Var { contents = Some (t1) }
  | List (t1), List (t2) ->
      unify t1 t2
  | Fun (t11, t12), Fun (t21, t22) ->
      unify t11 t21;
      unify t12 t22
  | Var (var1), Var (var2) when var1 == var2 -> ()
  | Var ({ contents = None } as var), t2
  | t2, Var ({ contents = None } as var) ->
      assert (occur var t2);
      var := Some (t2)

　型変数を参照で表現しているので、単一化の結果を型代入の集合として返すようなまどろっこしいことをする必要はありません。関数型言語とは一体…うごご
注意が必要なのは解が存在するかのチェックで、同じ型変数であるかどうかは物理的等価性を比較する必要があります。要するに=じゃなくて==使えってことで。

型を文字列で表現する

(* 指定した番号の型変数における文字列表現 *)
let string_of_var id =
  "'" ^ String.make 1 (char_of_int (int_of_char 'a' + id mod 26)) ^
    if id < 26 then "" else string_of_int (id / 26)

let to_string t =
  let counter = ref 0 in
  let dic = ref [] in
  let rec to_string_aux = function
    | Int -> "int"
    | Bool -> "bool"
    | Var ({ contents = None } as var) ->
        begin try List.assq var (!dic) with
        | Not_found ->
            let label = string_of_var (!counter) in
            dic := (var, label) :: !dic;
            incr counter;
            label
        end
    | Var { contents = Some (t) } -> to_string_aux t
    | Fun (Fun _ as t1, t2) ->
        "(" ^ to_string_aux t1 ^ ") -> " ^ to_string_aux t2
    | Fun (t1, t2) -> to_string_aux t1 ^ " -> " ^ to_string_aux t2
    | List (Fun _ as t) -> "(" ^ to_string_aux t ^ ") list"
    | List (t) -> to_string_aux t ^ " list" in
  counter := 0;
  dic := [];
  to_string_aux t

　今回の実装では型変数を参照としているので、そのままでは文字列としてどう表現するか悩みどころです。結局のところ再帰でループを回しつつローカル変数のカウンタと変数の辞書を破壊的代入で更新する、Haskellerが見たらディスプレイを叩き割りそうな方法に落ち着きました。ここでも物理的等価性を比較する所に注意が必要で、型変数に与えられた文字列表現を検索する際にList.assocではなくList.assqを使っています。

ソースコードは

https://github.com/fetburner/TypingML4
に置いておくので、間違っている点等が有りましたらご指摘下さい。