型推論を実装する　その３　（型推論のある言語を作る）

型なしのLETREC、型検査のCHECKEDときて、ついに型推論ができるINFERREDの実装に移る。

言語仕様の変更

前回のCHECKEDでは

letrec int double(x : int)
  = if zero?(x) then 0 else -((double -(x, 1)), -(0, 2))
  in
  (double 6)

のように関数の仮引数の型と、再帰関数の戻り値の型を明示的に指定する必要があった。

INFERREDでは型注釈の部分に「?」を入れることで、型をプログラマが指定せずに言語側で推論するようにできる：

letrec ? double(x : ?)
  = if zero?(x) then 0 else -((double -(x, 1)), -(0, 2))
  in
  (double 6)

HaskellやMLのように型注釈を完全に省略するのではなく、C++のautoのように本来明示的に型を書くべきところに?と書くことで推論に回す、という構文だ。

型

今までType.tは：

type t = Int
       | Bool
       | Proc of t * t

のように、数値型、真偽型、そして関数型の三種が定義されていたのだが、今回そこに二つ追加する：

       | Unknown
       | Var of int

?で型注釈が省略されたところに、パースの時点でType.Unknownにしておいて、型検査の時にType.Var nとユニークな型変数を振っていく。

そのためにTypeモジュールに、新しい（ユニークな数字が振ってある）型変数を作成するnew_var関数と、それを使ってType.UnknownをType.Var nに変換するmake_concrete関数を定義する：

let n = ref 0
let init () = n := 0
let new_var () = let x = !n in (incr n; Var x)

let make_concrete = function
  | Unknown -> new_var ()
  | t -> t

Type.nがグローバルステートになっているが・・・　まあこういうところで限定的に副作用が使えるのもOCamlらしいということで・・・

最後に、ある型変数が別の型の中に出てくるかを調べるoccurs関数：

let rec occurs t1 = function
  | Int | Bool -> false
  | Var _ as t2 -> t1 = t2
  | Proc (t2, t3) ->
      occurs t1 t2 || occurs t1 t3
  | Unknown -> failwith "Invalid no occurrence check against Unknown type"

型推論

それではついに型推論の話に移る。

INFERREDでは型推論は型検査と同時に起きる。というか型検査の一部として、型注釈が?な部分に型変数を振った上で解決可能かをつどつど調べていく。

なのでTypecheckモジュールの中で型推論している。Const、Var、LetはCHECKEDと変わらず：

let rec check tenv = function
  | Exp.Const _ -> Type.Int
  | Exp.Var s -> (match Tenv.find tenv s with
      | Some t -> t
      | None -> failwith "Variable not typed")
  | Exp.Let (s1, e1, e2) ->
      let t1 = check tenv e1 in
      let tenv' = Tenv.extend tenv s1 t1 in
      check tenv' e2

ZeroP、Diff、Ifあたりから違いがで始める：

  | Exp.ZeroP e -> 
      let t = check tenv e in
      begin
        Unify.f t Type.Int;
        Type.Bool
      end
  | Exp.Diff (e1, e2) ->
      begin
        Unify.f (check tenv e1) Type.Int;
        Unify.f (check tenv e2) Type.Int;
        Type.Int
      end
  | Exp.If (e1, e2, e3) ->
      begin
        Unify.f (check tenv e1) Type.Bool;
        Unify.f (check tenv e2) (check tenv e3);
        check tenv e2
      end

大事なポイントはUnify.f関数を使っている点（Unify.fの実装については後述。論理プログラミングなどでいうところの「単一化」のための関数である）。CHECKEDと違ってINFERREDではcheck tenv eなどが型変数を返すことがあり得るので、「ZeroPの引数が数値型かどうか」などを直接調べることができない。Unify.fを使って「ZeroPの引数が数値型であると仮定して矛盾が起きないか」を調べることになる。

関数定義：

  | Exp.Proc (s, t, e) ->
      let t1 = Type.make_concrete t in
      let t2 = check (Tenv.extend tenv s t1) e in
      Type.Proc (t1, t2)

前述のType.make_concreteで型注釈が省略されている場合は引数に型変数を振る（明示的な型注釈がある場合はその型をそのまま使う）。Unify.fを使う必要はなし。

再帰関数定義：

  | Exp.LetRec (t1, fname, arg, t2, body, e) ->
      let rt = Type.make_concrete t1 in
      let at = Type.make_concrete t2 in
      let tenv' = Tenv.extend tenv fname (Type.Proc (at, rt)) in
      let tenv'' = Tenv.extend tenv' arg at in
      let bt = check tenv'' body in
      begin
        Unify.f bt rt;
        check tenv' e
      end

再帰関数は引数と戻り値両方に型注釈がつくので、Type.make_concreteも二回呼び出している。Unify.fは一回だけ（戻り値の型注釈と、再帰関数のbody部分の型に矛盾がないかを検査している）。

関数呼び出し：

  | Exp.Call (e1, e2) ->
      let rt = Type.new_var () in
      let t1 = check tenv e1 in
      let t2 = check tenv e2 in
      begin
        Unify.f t1 (Type.Proc (t2, rt));
        rt
      end

関数適用の結果の型は、型検査が進まないとわからない。なので結果に対して新たに型変数を振って、関数部分の型と（引数部分の型 -> 適用結果の型変数）に対してUnify.fを使って矛盾がないか確認した上で、式全体の型としては適用結果の型変数を返す。

これでTypecheckの主要部分は見終わった。次にUnify.fの実装。

まずは単一化したい二つの型の型変数を解決できるだけ解決しておいてからmatchする：

let rec f t1 t2 =
  match Subst.apply t1, Subst.apply t2 with
 ...

Subst.applyで型変数を解決する。この場合解決とは、出てくる型変数すべてを（わかっているだけ）固有の型に変換する、という意味。

もし二つの型が同一なら何もせずに単一化が成功する。

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

片方が型変数だった場合：

    | Type.Var _ as t1', t2' ->
      if Type.occurs t1' t2' then failwith "No occurrence condition violated"
      else Subst.extend t1' t2'
    | t1', (Type.Var _ as t2') ->
      if Type.occurs t2' t1' then failwith "No occurrence condition violated"
      else Subst.extend t2' t1'

片方が型変数だった場合、その型変数ともう片方の型との対応を追加する形でSubst内の状態を更新する（Subst.extend）。ただし、片方が型変数、もう片方に同じ型変数が使われていた場合、再帰的になってしまうがそれは許されていない。単一化は失敗し型エラーとなる。

どちらも関数型だった場合：

    | Type.Proc (atype1, rtype1), Type.Proc (atype2, rtype2) ->
      begin
        f atype1 atype2;
        f rtype1 rtype2
      end

引数の型どうし、戻り値の型どうしを単一化させて終わり。

上記以外はエラー：

    | _ -> failwith "Unification failed"

単一化する二つの対象が

型が完全に一致
片方が型変数
両方が関数型

以外の場合エラーだというのは考えてみれば納得できると思う。

最後に型変数の環境とも言えるSubstモジュール：

type t = (Type.t * Type.t) list ref

let subst : t = ref [] 
let init () = subst := []

let extend tv t = match tv with
  | Type.Var _ -> subst := (tv, t)::!subst 
  | _ -> failwith "Cannot extend substitution with a non-var LHS"

let rec apply = function
  | Type.Int -> Type.Int
  | Type.Bool -> Type.Bool
  | Type.Proc (t1, t2) ->
      Type.Proc (apply t1, apply t2)
  | Type.Var _ as t1 -> (match List.assoc_opt t1 !subst with
      | Some t2 -> t2
      | None -> t1)
  | Type.Unknown -> failwith "Invalid substitution application to Unknown type"

Substモジュールの中核にあるのは(型変数 * 型) list refのデータ構造で、それを初期化するinit、listに(型変数 * 型)を追加するextendと、型変数を解決する関数applyが定義されている。

これもグローバル変数的なものになっているのは気になる・・・　が、元々はTypecheck.checkがSubst.tを引数・戻り値両方に含むような形でコードを書いた（EoPLも同じようなコードになっていた）のだが、それをグローバル変数化したことでTypecheckのコードの見通しがものすごくよくなったという経緯があるので仕方ない。

使ってみる

非再帰関数：

>>> let f = proc (x:?) -(x, 1) in
let g = proc(h:?) (h 1) in
(g f)

0

再帰関数：

>>> letrec ? double(x : ?)
  = if zero?(x) then 0 else -((double -(x, 1)), -(0, 2))
  in
  (double 6)

12

型が合わないと：

>>> letrec ? double(x : ?)
  = if zero?(x) then 0 else -((double -(x, 1)), -(0, 2))
  in
  (double zero?(5))

Fatal error: exception Failure("Unification failed")

成功。

というわけでTypecheckでの型検査時に「この二つの型（変数）が同一だと考えて矛盾が生じるかどうか」をUnifyで調べ、矛盾が生じなければその対応関係を型変数環境ともいうべきSubstにどんどん入れていく、というおおまかな流れで型推論が実装できた。

Arantium Maestum

プログラミング、囲碁、読書の話題

型推論を実装する　その３　（型推論のある言語を作る）

言語仕様の変更

型

型推論

使ってみる