7-3. 変数の型付けを含む型検査

次に、変数を追加しよう。式の構文は、以下のように拡張する。
type exp =
  ...
  | Var of string         (* variable e.g. x *)
変数は、どのような型でも持てるので、(x + 10) や (if x then 10 else 20) は、型が整合する式である。 では、変数の型は一切無視すればいいかというと、そうではない。 たとえば、 (if x then x else 20) は、x がどのような型であるとしても、 型が整合しない。なぜなら、最初の x はbool型であるが、 2つ目の x は int型なので、一致しないからである。 後述する型推論では、 変数の型を自動的に計算(推論)するという作業を行う。 ここでは、それより簡単な型検査について述べる。

型検査は、C言語や Java言語のように、変数の型があらかじめすべて宣言さ れている言語で使われるものである。 一方、OCaml では、変数の型を宣言しない ので(宣言してもよいが、普通は宣言しない)、最終的には、型推論が必要となる。

型環境

前に作った tcheck1 は、「式」を与えて「その式の型」を返す(型が整合しな い場合はエラーを起こす)ものであった。ここでは、 式だけでなく、「その式に含まれる変数たちの型」も与えて その式の型を返す関数 tcheck2 を作成する。 この場合でも、型が整合しない場合はエラーとなる。

「式に含まれる変数たちの型」は、正式には型環境と呼ばれる。これは、 評価器における環境と似ている。環境は「変数と値」のリストであったが、 型環境は「変数と型」のリストとなる。型環境をあらわすデータの型は 以下のように定義される。

  type tyenv = (string * ty) list
たとえば、[("x", TInt); ("y", TBool)] は、 「変数xが int型で変数yが bool型」という型環境を表す。

型環境に対する lookup 関数が必要になるが、驚くべきことに 既に定義した(変数の値に対する)環境に対する lookup をそのまま使え るので、もう1度書く必要はない。これは、多相型をもつ OCaml の強みである (昔、1粒で2度おいしいというお菓子があったが、多相型を持つ式は、 1回定義すれば2回でも3回でも、相異なる型に具体化して使える。)

(* tcheck2 : tyenv -> exp -> ty *)
let rec tcheck2 te e =
  match e with
  | Var(s)    ->  lookup s te   (* 変数の型は、型環境 te から取ってくる *)
  | IntLit(_)    -> TInt
  | ...
  | Plus(e1,e2)  -> 
       begin
          match (tcheck2 te e1, tcheck2 te e2) with
          ...
この実装を見てわかるように、型環境 te は、tcheck2 の実行中には新しい要 素を追加されたり、削除されたりせず一定である。

課題 7-3.


トップ, 前へ. 次へ.

亀山 幸義