型推論器を作る(1) 構文木とテスト


## 目次

1. [構文木とテスト](http://qiita.com/h_sakurai/items/85d9efbfce19e2db31a2)
- [単相の型推論①型取得と単一化](http://qiita.com/h_sakurai/items/f16502e6f867b5e90b86)
- [単相の型推論②出現チェック](http://qiita.com/h_sakurai/items/a31c4ddc72cdbcd70bd0)
- [レミの多相型型推論①一般化とインスタンス化](http://qiita.com/h_sakurai/items/69cda3ce73ae6d4fda64)
- [レミの多相型型推論②レベルを追加する](http://qiita.com/h_sakurai/items/0058e90c7c1cf45ab54d)
- [レミの多相型型推論③Letに型の初期値を設定する](http://qiita.com/h_sakurai/items/5c0bf666a82e48a52fef)

## はじめに

OCamlの型推論がどのように出来ているかの文章を約してみたのですが、
自分なりにまとめてみました。

http://okmij.org/ftp/ML/generalization.html

https://github.com/hsk/generalization/wiki

## 構文木とテスト

第一回目ではテストを作ります。

まず、構文木は必要だし、テストは変えたくないので、Unboundにはレベルを最初から持たせましょう。

```ocaml:
type e =
| Var of string
| App of e * e
| Lam of string * e
| Let of string * e * e

type t =
| TVar of tv ref
| TArrow of t * t
and tv =
| Unbound of string * int
| Link of t
```

そして、スタブの型推論器と補助関数を作ります。

```ocaml:
module Typing = struct

  let count = ref 0

  let reset() =
    count := 0

  let gensym () =
    let n = !count in
    incr count;
    if n < 26 then
      String.make 1 (Char.chr (Char.code 'a' + n))
    else
      "t" ^ string_of_int n

  let newvar() =
    TVar(ref (Unbound(gensym(), 1)))

  let apply(e:e):t =
    newvar()
end
```

テストするコードを書いてみましょう。

```ocaml:
let print_assert = function
  | Assert_failure (_,l,_) ->
    Printf.printf "test error %d\n" l
  | _ -> assert false

let test(f,e, r) =
  try
    let r = Typing.apply r in
    if r = e then () else(
      try
        f ();
      with
      | Assert_failure _ as a -> print_assert a 
    )
  with
  | a ->
    try
      f ();
    with
    | Assert_failure _ as a -> print_assert a 


let _ =
  let id = Lam("x", Var"x") in
  let c1 = Lam("x", Lam("y",App (Var"x",Var"y"))) in
  test((fun () -> assert false),
    TArrow (TVar {contents = Unbound ("a", 1)},
            TVar {contents = Unbound ("a", 1)})
    ,
     id
  );
  test((fun () -> assert false),
    TArrow
      (TVar
        {contents =
          Link
            (TArrow (TVar {contents = Unbound ("b", 1)},
                     TVar {contents = Unbound ("c", 1)}))},
        TArrow (TVar {contents = Unbound ("b", 1)},
                TVar {contents = Unbound ("c", 1)}))
    ,
     c1
  );
  test((fun () -> assert false),
    TArrow (TVar {contents = Unbound ("b", 1)},
            TVar {contents = Unbound ("b", 1)})
    ,
    (Let ("y",Lam ("z",Var"z"), Var"y"))
  );
  test((fun () -> assert false),
    TArrow (TVar {contents = Unbound ("a", 1)},
            TArrow (TVar {contents = Unbound ("c", 1)},
                    TVar {contents = Unbound ("c", 1)}))
    ,
    (Lam ("x", Let ("y",Lam ("z",Var"z"), Var"y")))
  );
  test((fun () -> assert false),
    TArrow (
      TVar {contents = Unbound ("a", 1)},
      TVar {contents = Link (
        TVar {contents = Link (
          TVar {contents = Unbound ("a", 1)})})})
    ,
    (Lam ("x", Let ("y",Lam ("z",Var"z"), 
                                    App (Var"y",Var"x"))))
  );
  (try
    let _ = Typing.apply(Lam ("x",App (Var"x",Var"x"))) in
    assert false
  with
  	| Failure e -> print_endline e
  	| (Assert_failure _) as a -> print_assert a
  	| _ -> (try assert false with a -> print_assert a)
  );
  (try
    let _ = Typing.apply(Let ("x",Var"x",Var"x")) in
    assert false;
  with
  	| Not_found -> print_endline "unbound var"
  	| (Assert_failure _) as a -> print_assert a
  	| _ -> (try assert false with a -> print_assert a)
  );
  (* id can be `self-applied', on the surface of it *)
  test((fun () -> assert false),
    TVar {contents = Link(
      TVar {contents = Link(
        TArrow (TVar {contents = Unbound ("c", 1)},
                TVar {contents = Unbound ("c", 1)}))})}
    ,
    (Let ("id",id, App (Var"id",Var"id")))
  );
  test((fun () -> assert false),
    TArrow (
      TVar {contents = Unbound ("i", 1)},
      TVar {contents = Unbound ("i", 1)})
    ,
    (Let ("x",c1,
                    Let ("y",
                          Let ("z",App(Var"x",id), Var "z"),
                         Var"y")))
  );
  (*
  fun x -> fun y -> let x = x y in fun x -> y x
  - : (('a -> 'b) -> 'c) -> ('a -> 'b) -> 'a -> 'b = <fun>
  *)
  test((fun () -> assert false),
    TArrow (
      TVar {contents = Link (
        TArrow (
          TVar {contents = Link (
            TArrow (
              TVar {contents = Unbound ("d", 1)},
              TVar {contents = Unbound ("e", 1)}))},
          TVar {contents = Unbound ("c", 1)}))},
      TArrow (
        TVar {contents = Link (
          TArrow (
            TVar {contents = Unbound ("d", 1)},
            TVar {contents = Unbound ("e", 1)}))},
        TArrow (
          TVar {contents = Unbound ("d", 1)},
          TVar {contents = Unbound ("e", 1)})))
    ,
    (Lam ("x", Lam("y",Let ("x",App (Var"x",Var"y"),
                                   Lam ("x",App (Var"y",Var"x"))))))
  );
  print_string "start sound test\n";
  (* now sound generalization ! *)
  test((fun () -> assert false),
    TArrow (
      TVar {contents = Unbound ("a", 1)},
      TVar {contents = Unbound ("a", 1)})
    ,
    (Lam ("x", Let ("y",Var"x", Var"y")))
  );
  (* now sound generalization ! *)
  test((fun () -> assert false),
    TArrow (
      TVar {contents = Unbound ("a", 1)},
      TArrow (
        TVar {contents = Unbound ("c", 1)},
        TVar {contents = Unbound ("a", 1)}))
    ,
    (Lam ("x", Let ("y",Lam ("z",Var"x"), Var"y")))
  );
  (* now sound generalization ! *)
  test((fun () -> assert false),
    TArrow (
      TVar {contents = Link (
        TArrow (
          TVar {contents = Unbound ("b", 1)},
          TVar {contents = Unbound ("c", 1)}))},
      TArrow (
        TVar {contents = Unbound ("b", 1)},
        TVar {contents = Unbound ("c", 1)}))
    ,
    (Lam ("x", Let ("y",Lam ("z",App (Var"x",Var"z")), Var"y")))
  );
  (* now sound generalization ! *)
  test((fun () -> assert false),
    TArrow (
      TVar {contents = Link (
        TArrow (
          TVar {contents = Unbound ("b", 1)},
          TVar {contents = Link (
            TArrow (
              TVar {contents = Unbound ("b", 1)},
              TVar {contents = Unbound ("d", 1)}))}))},
      TArrow (
        TVar {contents = Unbound ("b", 1)},
        TVar {contents = Unbound ("d", 1)}))
    ,
    (Lam ("x", Lam("y",Let ("x",App (Var"x",Var"y"),
                                            App (Var"x",Var"y")))))
  );
  (* now sound generalization ! *)
  (try
    let _ = Typing.apply(Lam ("x",Let("y",Var"x", App (Var"y",Var"y")))) in
    assert false
  with
  	| Failure e -> print_endline e
  	| Assert_failure _ as a -> print_assert a;
  	| _ -> (try assert false with a -> print_assert a)
  );

  (* now sound generalization ! *)
  (* fun x -> let y = let z = x (fun x -> x) in z in y
     - : (('a -> 'a) -> 'b) -> 'b = <fun>
  *)
  test((fun () -> assert false),
    TArrow (
      TVar {contents = Link (
        TArrow (
          TArrow (
            TVar {contents = Unbound ("b", 1)},
            TVar {contents = Unbound ("b", 1)}),
          TVar {contents = Unbound ("c", 1)}))},
      TVar {contents = Unbound ("c", 1)})
    ,
    (Lam ("x",
      Let ("y",
      Let ("z",App(Var"x",id), Var "z"),
      Var"y")))
  );
  print_endline "\nAll Done\n"

```

殆ど、元のソースからのコピーなので、このテストを通れば多相な型推論がちゃんと動くと言えるであろう物です。

## 参照

http://okmij.org/ftp/ML/generalization.html

https://github.com/hsk/generalization/wiki