7-4. 関数に対する型検査

type exp =
  ...
  | Fun of string * exp   (* fun x -> e *)
  | App of exp * exp      (* function application i.e. e e *)

  type ty = TInt | TBool | TArrow of ty * ty

関数の型の検査

• 関数 (fun x -> e) に対して: 関数の引数であるx の型が何であるかわからないが，ここでは簡単のため， このx の型も型環境で与えられるとする(この制限は後に取り除く予定である)． この型を t1 とし，関数本体 e の型を t2 とすれば， (fun x -> e) の型は t1 -> t2 である． この型検査は(x と e の型検査が正常終了する限り)常に正常終了する (エラーにはならない．)
• 関数適用 (e1 e2) に対して: e1 と e2 をそれぞれ型検査して， それぞれの型が t1, t2 であることがわかったとする． このとき (e1 e2) という式の型が整合的であるためには， ある型t3 に対して，t1 = t2 -> t3 という等式が成立しなければならない． (t1 は関数の型であり，t2 は，その引数の型であるので， このような等式が成立しなければならない． たとえば，int -> bool 型の関数に int型の引数を適用することはできるが， bool型の引数を適用することはできない．) そこで，t1=t2->t3の形になるかどうかをチェックし，なれば， (e1 e2) の型として，t3 を返して終了する． この形にならない場合は，型エラーなので，エラーを発生して終了する．

(* tcheck3 : tyenv -> exp -> ty *)
let rec tcheck3 te e =
  match e with
  ...
  | Fun(x, e1) ->
        let t1 = lookup x te in
        let t2 = tcheck3 te e1 in 
           TArrow(t1,t2)
  | App(e1,e2) ->
        let t1 = tcheck3 te e1 in
        let t2 = tcheck3 te e2 in 
          begin
           match t1 with
	   | TArrow(t10,t11) -> if t2=t10 then t11
                             else failwith "type error in App"
	   | _ -> failwith "type error in App"
          end
  | _ -> failwith "unknown expression"

課題 7-4.

• 関数tcheck3 に，いくつかの式を与え，正しく型推論できていることを確かめよ． このための例題としては、以下のものを使うとよい。
  • 式(fun x -> if true then x else 100) と型環境 [("x",TInt)]
  • 式(fun x -> if true then x else 100) と型環境 [("x",TBool)]
  • 式((fun x -> if true then x else 100) (if true then y else 200)) と型環境[("x",TInt);("y",TInt)]
  • 式(fun f -> (fun x -> f (f (f x + 10)))) と適当な型環境
  • 式(fun f -> (fun g -> (fun x -> f (g x)))) と適当な型環境
  [Hint: 「適当な型環境」が何かわからないときは、まず、上記の式を OCaml に入力して、全体としてどのような型になるかを考えるとよい。 (fun f -> e) の形の式の型が (α->β)であれば、変数x はα型で、 関数の本体e はβ型である。]

• これまでに実装した型検査器では、(if e1 then e2 else e3) の形の式は e2とe3 がともに bool型かint型でなければならなかった。一方、実際の OCaml では e2とe3 の型が等しければ何でもよい(何らかの関数の型でもよい)。 たとえば、(if true then (fun x -> x+1) else (fun y -> y*2)) という式も 型が整合する。 そこで、そのような場合も型検査 に通るよう、tcheck3 における if文の処理を拡張せよ。

発展課題 (オプショナル)

• (発展課題: オプショナル) tcheck3を拡張して、let式に対応させよ。

  [Hint] この実験の範囲では、(let x = e1 in e2)という式は、 ((fun x -> e2) e1) という式と同じである。 そこで、既に実装した Fun と App の型付けを利用すればよい。

  例題としては、以下のものを使うとよい。

  • 式(fun x -> let y = x + 10 in y * 10) と 型環境[("x",TInt); ("y",TInt)]
  • 式(let x = fun y -> y in let z = fun w -> w in (x z) 10) と適当な型環境[("x",TInt); ("y",TInt)]
• 型検査のまとめとして、tcheck3 を拡張して、 ミニOCaml言語のなるべく多くの構文に対応するようにせよ。 まだ対応していないものは、(e1 > e2) の形の式など、 簡単に拡張できるものが多いので、 是非試みてほしい。 また、さらに余力があれば let-rec 式にも対応させてみよ。

補足: tcheck3 では，関数の引数となる変数の型も， 型環境で与えなければいけない．そのため，異なる関数の引数がx という同じ 名前であったとき，それらの型も同じでなければいけない，という(OCamlにはない) 制約がある． たとえば (fun x-> x) (fun x -> x + 1) という式は、OCaml では型がつく が、tcheck3 では型がつかない。なぜなら、2つの束縛変数x は OCaml では 異なるものであるのに、tcheck3 は区別せずに同じ型を持つ変数と見なしている からである。

この問題を克服するには、 型環境をつかうのではなく，関数の仮引数(変数)ごとに型を記述するスタイルにすれば よい．この場合，「式」の構文の中に，「型」を含む表記を許すよう 拡張しなければいけないので，本実験では，この方向は深追いしないが、 もし興味がある人がいたら、拡張してみるとよい。 たとえば、以下のようにするとよい。

type exp = 
    ...
  | Fun of string * ty * exp   (* fun (x:t) -> e *)
  | ...

亀山 幸義