λμのTypeCheckerの実装
λμのtypecheckerを実装したので
(ソースコードは参考文献[3]を参照)
λμ[1]はλ→に継続(callCC)を入れたもの(CCC + Continuation monad)。
syntax的にはμ-abstractionとnaming(termに名前をつける)が追加される。
型なしの項を受け取って、それにうまく型をつけることを考える。
アルゴリズム(合ってる保証はない):
typing : Context -> UntypedTerm -> Type (var) typing(G,x) = G(x) (lam) typing(G,λx.M) = ?n -> typing(G;x:?n, M) (app) typing(G,MN) = let U -> V = typing(G,M); W = typing(G,N) in unify(U -> V, W -> ?n); V (mu) typing(G,μα.M) = let U = typing(G,M) in unify(U,⊥); G(α) (name) typing(G,[α]M) = let U = typing(G;α:?n, M) in unify(U,G(α)); ⊥
ここで?n
はhole(まだ決定されていない型)を表していて、
unify
は与えられた型を合わせる作業をしてくれる。
厳密にはunifyは型の等式からなる集合({?0 = M, ?1 = ?2 -> ?3}
のようなもの)をより簡単な形に変えてかつ無駄を省いていく。途中で必要があれば型エラーを吐いてそれをユーザーに見せることもある。
unification algorithmは[2]をそのまま実装した。
で、肝心のコードについては、
必要なデータをState Environment
で引きずり回して随所でEitherを返すようにしたら最高にめんどくさくなったので、エラーメッセージのハンドリングはEitherTを使うなり(モナドトランスフォーマー重ねたくねぇ)MonadErrorでやるなりしたいなーと思いつつやってない。
とりあえず良い練習にはなったので他の型システムも随時実装していきたい。