Arantium Maestum

プログラミング、囲碁、読書の話題

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

前回のコードにLetによる変数束縛を追加する。

gist.github.com

コードの追加としては2行のみと非常に短い。

変更なし

追加するのはLetだけ:

type exp =
...
| ELet of string * exp * exp

ELet(変数、変数を束縛する式、本体の式)という構成になっている。

この型システムはSTLCの拡張で、HM型推論があるわけではないので実際にはラムダ抽象・関数適用の組み合わせで代用可能ではあるのだが

ELet("x",(ENat 1),(EVar "x"))

と、同等の

EApp(EAbs("x",TNat,(EVar "x")),(ENat 1))

を比較すると「ラムダ抽象・関数適用の組み合わせ」には明示的なTNatが出てくる。ラムダ抽象と関数適用にバラすと、ラムダ抽象の式単体では実引数の型情報にアクセスできないので、全体的な視点では不必要にも思える明示的な型注釈が必要になっているということだ。

確かHM型推論がLetのみ一般化できるというのもこれに似た話だったはず・・・。記憶があやふやなので実装するのを楽しみにしていよう。

typeof関数

ELet式のケースを書いていく:

let rec typeof env = function
...
| ELet(var,e1,e2) -> typeof ((var, typeof env e1)::env) e2

環境envを(「変数」:「束縛される式の型」)という情報で拡張して、その環境で「本体の式」の型を求めている。

余談だが、言語処理系の実装などをしているとtypeof ((var, typeof env e1)::env) e2のような「再帰的関数呼び出しで得た情報を引数に加えてもう一度再帰的呼び出し」といったコードが普通に出てきて自分も普通に書くようになるが、これは一般的なプログラミングではかなりレアなケースなことを忘れがちだと最近気がついた。昔は相互再帰的な関数なんて何に使うんだ?と自分が書けるような気がまったくしなかったものだが、今では「まあ問題が相互再帰的だったら普通にプログラムもそうなるよね」としか思わなくなっている。

学習時の言語機能・構文に対する直観というのは(少なくとも私個人では)あてにならないものだな、と改めて。

次回

次はレコードを追加する。