6-2.単純な式に対する型検査 [2010/09/26 追加]

最初に、ミニOCaml言語の式の構文を(もう１度)限定して、整数定数，真理値定数，足し算，if-then-else だけを持つ式だけとし，これに対する型検査を考える。式をあらわす型 exp は次のように定義される．

(* 処理対象となる式の型の定義 *)
type exp =
    IntLit of int
  | BoolLit of bool
  | Plus of exp * exp 
  | If of exp * exp * exp

次に、これから作成する型検査システムでは、「ミニOCaml言語の式の型」をデータとして扱う必要があるので、そのためのデータ型 ty を以下のように定義する。

(* 「型」をあらわす型の定義 *)
type ty = TInt | TBool

ここで TInt と TBoll はそれぞれ「ミニOCaml言語の整数型」と「ミニOCaml 言語の真偽値型」をあらわす。これらは、データ構成子であり、 OCaml の型である int や bool をそのまま使ってはいけない。

ここまで準備ができたら、型検査器 tcheck1 を一気に書いてしまおう。 tcheck1 は exp型のデータ(式) を受けとり、ty型のデータ(「型」を意味するデータ)を返す関数である。

(* tcheck1 : exp -> ty *)
let rec tcheck1 e =
  match e with
  | IntLit(_)    -> TInt
(**************************
(* 2010/10/13 13:33 修正; 以下はミスタイプでした。
 *  | BooltLit(_)  -> TBool
 *)
  | BoolLit(_)   -> TBool
  | Plus(e1,e2)  -> 
       (match (tcheck1 e1, tcheck1 e2) with
          (TInt,TInt) -> TInt
        | _ -> failwith "type error in Plus")
  | If(e1,e2,e3) -> 
       (match (tcheck1 e1, tcheck1 e2, tcheck1 e3) with
          (TBool,TInt,TInt) -> TInt
        | (TBool,TBool,TBool) -> TBool
        | _ -> failwith "type error in IF")
  | _ -> failwith "unknown expression"

プログラムを見てわかるように、型が整合しない式を与えたときは、 failwith 関数を読んでエラーとしている。

課題 10.

関数tcheck1 に，いくつかの式を与え，正しく型検査できていることを確かめよ．(たとえば，If(BoolLit(true), IntLit(1), IntLit(100)) を与えたり，If(BoolLit(true), Plus(IntLit(1), BoolLit(false)), IntLit(100)) を与えたりして，どういう結果になるか確認せよ．)
上記の定義で扱っている式の範囲を拡張し，(e1 = e2) (等しさの比較) に対する型も推論できるようにせよ．ただし、(e1 = e2) が整合的な型を持つのは、 e1 と e2 が同じ型(両方とも整数型か、両方とも真理値型)のときであり、どちらのケースでも (e1=e2)全体は真理値型である。
```
type exp = ... | Eq of exp * exp   (* 上記の定義に、Eq を追加 *)
```

トップ, 前へ. 次へ.

亀山幸義