7-7. 一般的な型推論

関数を含む式に対する一般的な型推論のアルゴリズムは、今までの考え方を踏襲するので、異なる点のみを説明する。

以前のアルゴリズムでは、型変数を作成するために new_typevar という関数を使っていた。そこでは、「普通の変数1つに対して、型変数を1つ作ればよい」というものだったので、 new_typevar は「普通の変数 (の名前を表す文字列、たとえば "x")」を引数として与え、それに適当な文字を追加して、新しい型変数の名前とすれば良かった。これにより、普通の変数の名前が2か所以上で衝突しない限り、型変数の名前も衝突することはなく、「新しい型変数」であることを保証できた。
一方、今回の一般的な型推論で必要とする new_typevarはそうはいかない。なぜなら、普通の変数とは無関係な場所で型変数を作る必要があるから。そこで、今回は、自然数で表される「カウンタ」を使い、型変数の名前は、そのカウンタの値を含むようにした。 new_typevar は呼ばれるごとに、1ずつカウンタの値を増やすので、複数の型変数の名前が衝突することはない。
ちなみに、このような場合、通常は、大域変数にカウンタの値を格納して更新していくのであるが、この実験では、「徹頭徹尾純粋な関数型言語の機能だけを使う」というポリシーなので、ここで述べる実装も、それに従っている。
前回の(関数のない言語に対する)型推論では、plus や ifの処理で場合分けが非常にたくさんあって大変だった。今回は、その辺の処理はすべて unify がやってくれるので、型推論器本体では、その辺は気にしなくてよくなった。
型推論器 tinf2 は、型環境, 式、(上述の)カウンタをもらい、 (変更した後の)型環境、式の型、型代入、(更新した)カウンタを返す、という関数である。ここで、「型環境」に加えて「型代入」も返している。、一瞬無駄なような気もするが、これは必要である。

最終的な tinf2 の実装は、以下の通りである。型代入の操作がかなり面倒なので、若干こみいったコードになっているがいろいろな例をあたえて試してみると、何をやっているかわかるであろう。

let theta0 = ([] : tysubst)

(* new_typevar : int -> ty * int *)
let new_typevar n = 
  (TVar ("'a" ^ (string_of_int n)), n+1)

(* tinf2 : tyenv -> exp -> int -> tyenv * ty * tysubst * int *)
let rec tinf2 te e n =
  match e with
    | Var(s) -> 
	(try
	   let t1 = lookup s te in (te, t1, theta0, n)
	 with Failure(_) ->
	   let (tx,n1) = new_typevar n in
	   let te1 = ext te s tx in
	     (te1, tx, theta0, n1))
    | IntLit(_)   -> (te, TInt, theta0, n)
    | BoolLit(_)  -> ...
    | Plus(e1,e2) -> 
	let (te1, t1, theta1, n1) = tinf2 te e1 n in
	let (te2, t2, theta2, n2) = tinf2 te1 e2 n1 in
	let t11 = subst_ty theta2 t1 in
	let theta3 = unify [(t11,TInt); (t2,TInt)] in
	let te3 = subst_tyenv theta3 te2 in
	let theta4 = compose_subst theta3 
	              (compose_subst theta2 theta1) in
	  (te3, TInt, theta4, n2)
    | If(e1,e2,e3) ->  ...
    | Fun(x,e) -> 
	let (tx,n1) = new_typevar n in
	let te1 = ext te x tx in
	let (te2, t1, theta1, n2) = tinf2 te1 e n1 in
	let t2 = subst_ty theta1 tx in
	let te3 = remove te2 x in
	  (te3, TArrow(t2, t1), theta1, n2)
    | App(e1,e2) -> 
	let (te1, t1, theta1, n1) = tinf2 te e1 n in
	let (te2, t2, theta2, n2) = tinf2 te1 e2 n1 in
	let (tx,n3) = new_typevar n2 in
	let t11 = subst_ty theta2 t1 in
	let theta3 = unify [(t11,TArrow(t2,tx))] in
	let t3 = subst_ty theta3 tx in
	let te3 = subst_tyenv theta3 te2 in
	let theta4 = compose_subst theta3 
	              (compose_subst theta2 theta1) in

	  (te3, t3, theta4, n3)
    | _ -> failwith "unknown expression"

(* 以下は例題 *)
let tinf2top e = tinf2 [] e 0
let _ = tinf2top (If(BoolLit(true), IntLit(1), IntLit(100)))
let _ = tinf2top (If(Var("x"),Plus(Var("y"), IntLit(10)), IntLit(100)))
let _ = tinf2top (If(Var("x"),Plus(Var("y"), Var("z")), Var("z")))
let _ = tinf2top (Var("x"))

remove関数についての補足. 上記の Fun のケースにある (remove te2 x) は、型環境 te2 から、変数xに対応する型宣言を除去して得られる型環境を意味する。たとえば te2 = [("x13",TInt); ("x20",TBool)] のとき、 (remove te2 "x13") = [("x20",TBool)] である。また、関数remove の型は tyenv -> string -> tyenvである。

発展課題 7-7.

型推論器に、いくつかの式を与え、正しく型推論できていることを確かめよ。入力の例は、以下の通りだが、少なくとも5個以上の例題を与えなさい。
- tinf2top (Fun("f",Fun("x",App(Var("f"),App(Var("f"),Var("x"))))))
- tinf2top (Fun("x",Fun("y",Fun("z", App(App(Var("x"),Var("z")), App(Var("y"),Var("z")))))))
上記の実装では BoolLit と If のケースが落ちている。これらを実装して型推論器 tinf2 を完成させよ。
この型推論器を拡張して、ミニOCaml言語のすべての式に対応するようにせよ。(let などにも対応させよ。)

トップ, 前へ. 次へ.

亀山幸義