簡単な型システムを実装していく３ STLC + Bool

前回のSTLCにBool型と関連する式を追加してみる：

gist.github.com

まずは型にTBoolを追加：

type ty =
...
| TBool

式にTrue, FalseとIf式を追加：

type exp =
...
| ETrue
| EFalse
| EIf of exp * exp * exp

If式はcondition式、if-true-branch式、if-false-branch式の三要素を持つ。

式に合わせてtypeof関数にケースを追加する。まずはTrue/False：

let rec typeof env = function
...
| ETrue | EFalse -> TBool

当然これら式はTBool型。

If式の型チェック：

| EIf(e1,e2,e3) ->
  if typeof env e1 != TBool
    then failwith "guard of conditional not boolean"
    else
      let t2 = typeof env e2 in
      if typeof env e3 != t2 then failwith "type mismatch in arms of conditional"
      else t2

まずcondition式を型チェックしTBoolであることを確認。もしそうならif-true-branchとif-false-branchの型が合うことを確認して、その結果をif式全体の型として返す。

そういえば前回書き忘れていたがif typeof env e3 != t2 then ...のように直接ty型の値同士を=で比較している。TaPLのサンプルコードなどでは別途比較関数を定義していたりするが、それは全称型の型変数などが出てきた場合に必要だからだと思われる（∀a. a->aという型と∀b. b->bという型が同じものだと判定できる比較関数が必要になる）。当面は=で比較しても良さそう。

今回のコードの全容としてはSTLCに12行追加で28行。

次回

次は自然数Natを追加する。