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

前回Simple Boolからはじめると書いたのだが、よく考えると単純型付きラムダ計算（STLC）ではじめるのが当然な筋な気がしてきた。

ので急遽Simple BoolからBoolを取っ払ってSTLCだけをまずみてみる：

gist.github.com

定義されるものとしては

• 「型」を表す型type ty
• 「式」を表す型type exp
• 「型検査」の関数typeof

の三つだけ。TaPLの公式実装はもちろん、Simple TaPLのレポジトリにも入っていたパーサも文字列化関数も評価器もすべて消して、あくまで型システムに必要な部分だけ残してある。モジュールも分けずに１ファイルにベタ書き。機能が増えてくると追いにくくなる可能性もあるが、STLCだとたった18行なので問題ない。

type ty

STLCは型は関数の型であるArrow(* -> *)だけ：

type ty =
| TArrow of ty * ty

STLCだと型推論がなく、関数の引数に型注釈が必要。なので式の一部に型が現れる。というわけでtype tyがtype expの前に定義される必要がある。

type exp

ラムダ計算なので式は変数、ラムダ抽象、関数適用の三つ：

type exp =
| EVar of string
| EAbs of string * ty * exp
| EApp of exp * exp

前述のとおりラムダ抽象に型注釈が含まれている。

let typeof env = function ...

式の型を調べ、型検査が失敗した場合はエラーを投げるtypeof関数：

let rec typeof env = function
...

「式変数と型の対応を保持するenv」と「型を調べたい対象の式」を引数にとる。envは(string * ty) listな実装が剥き出しになっていてまったく抽象化されていない。Association Listくらいなら隠蔽せずそのまま提示してしまった方がコードを目で追う分には楽な気がする。

式の三種のケースに対してパターンマッチしていく。まずは変数：

| EVar var -> List.assoc var env

Association Listであるenvに対してList.assocで変数名を検索している。envに変数が入っていない場合はエラーを投げる。ちゃんとした言語処理系であればここでしっかりエラーメッセージをなるべく役に立つようカスタム化するところだが省略。大まかに何が起きてるかがわかりやすいことを優先。

ラムダ抽象：

| EAbs(var, t1, e1) -> TArrow(t1, typeof ((var,t1)::env) e1)

前述のとおり、STLCだとラムダ抽象に明示的な引数に対する型注釈が入るので、引数の型は調べる必要がない。返り値に関してはtypeof ((var,t1)::env) e1で調べている。((var,t1)::env)のような形でenvをそのままAssociation Listとして拡張している。

関数適用：

| EApp(e1, e2) ->
  let t2 = typeof env e2 in
  (match typeof env e1 with
   | TArrow(t11, t12) ->
     if t11 = t2 then t12
     else failwith "parameter type mismatch"
   | _ -> failwith "non-arrow type in function position")

関数部分の型がちゃんとTArrowであることを確認し、その引数の型が実引数の型と合うことを確認している。

今気づいたのだけど、typeof env e2はletで束縛するよりもパターンマッチの中に入れておいたほうがわかりやすい気がする：

| EApp(e1, e2) ->
  (match typeof env e1 with
   | TArrow(t11, t12) ->
     if t11 = typeof env e2 then t12
     else failwith "parameter type mismatch"
   | _ -> failwith "non-arrow type in function position")

あるいはガードも使って：

| EApp(e1, e2) ->
  (match typeof env e1 with
   | TArrow(t11, t12) when t11 = typeof env e2 -> t12
   | TArrow _ -> failwith "parameter type mismatch"
   | _ -> failwith "non-arrow type in function position")

こうしたほうがいいかもしれない。

次回

次はSTLCにBoolと関連機能を追加してみる。