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

型検査の対象となる式の構文に関数を追加しよう。

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

これに対応して「式の型」をあらわす型も拡張する必要がある。関数の型は、(int -> bool) のように矢印を使って表現する。これを、TArrow(TInt, TBool) と表現することにしよう。ただ、関数の定義域や値域がさらに関数型であることもある。たとえば、(int -> (int -> bool)) や ((int -> bool) -> int) といったものも型である。(このような「高階関数」が使えることが、関数型言語の特徴の1つである。)そこで、拡張された ty型は以下のように定義される。

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

この定義を使えば、(int -> (int -> bool)) に対応する内部表現は、TArrow(TInt, TArrow(TInt, TBool)) となる。

関数の型の検査

上記の拡張に対する型検査は、以下のように行えばよい。

関数 (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 を実装する。

(* 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 x -> 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",TArrow(TArrow(TInt, TInt), TArrow(TInt, TInt))); ("y", TArrow(TInt, TInt)); ("z", TArrow(TInt, TInt)); ("w", 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 *)
  | ...
```
この場合、Fun の構文を変更するので、今まで実装した Fun を扱う部分も全て変更する必要がある。なお、後に述べる型推論の考え方を使えば、この問題点も自然に解消する。

トップ, 前へ. 次へ.

亀山幸義