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

前回のSTLC+Boolに自然数と関連する機能を追加していく。

gist.github.com

型

TNatという自然数を表す型を追加：

type ty =
...
| TNat

式

三種類の式を追加：

type exp =
...
| ENat of int
| EAdd of exp * exp
| EIsZero of exp

• 自然数リテラルを表すENat of int（実はintをとるので自然数じゃない・・・　ZeroとSuccにしてもよかったんだけどめんどくさいし実際こんな実装にしてる言語はほぼないに等しいので・・・）
• 自然数同士の足し算を表すEAdd of exp * exp
• 自然数がゼロかどうかを調べるEIsZero of exp

あれ、自然数って0も含むんだっけ？と心配になって調べたところ、定義に揺れのあるところらしい。とりあえずISO80000-2では0も含むと定義されている。

後者二つは今回はTaPL実装に従って独自のASTノードを定義しているが、別解としては組み込み関数としても用意するのもいい。その場合はtypeof関数に渡すenvにadd: TArrow(TNat, TArrow(TNat, TNat)), iszero: TArrow(TNat, TBool)といった初期設定を追加しておく必要が出る。

型検査

追加した三種の式のケースをtypeof関数にも追加していく。

まずはENat：

let rec typeof env = function
...
| ENat _ -> TNat

なんの数字かは関係なくTNatとなる。

EAdd：

| EAdd(e1,e2) ->
  if typeof env e1 = TNat && typeof env e2 = TNat then TNat
  else failwith "non-nat argument(s) to add"

まず引数が二つとも自然数であることを確認してから、全体の型を自然数だと返す。

EIsZero：

| EIsZero e ->
  if typeof env e = TNat then TBool
  else failwith "non-nat argument to iszero"

引数がTNatなら式全体の型はTBool。

次回

次はLet式による変数束縛を追加する。