7-7. 一般的な型推論

関数を含む式に対する一般的な型推論のアルゴリズムは、 今までの考え方を踏襲するので、異なる点のみを説明する。 最終的な tinf2 の実装は、以下の通りである。 型代入の操作がかなり面倒なので、若干こみいったコードになっているが いろいろな例をあたえて試してみると、何をやっているかわかるであろう。
let theta0 = ([] : tysubst)

(* new_typevar : int -> ty * int ;; 型が間違っていたので修正 [2013/12/04] *)
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関数についての補足 [追加、2013/12/04] 上記の Fun のケースにある (remove te2 x) は、 型環境 te2 から、変数xに対応する型宣言を除去して得られる型環境を意味する。 たとえば te2 = [("x13",TInt); ("x20",TBool)] のとき、 (remove te2 "x13") = [("x20",TBool)] である。 また、関数remove の型は tyenv -> string -> tyenvである。

発展課題 7-7.


トップ, 前へ. 次へ.

亀山 幸義