Recursive Typeの実装 - Just $ A sandbox

前回はsimply-typedの拡張としてλμを実装したけれど、
今回はsimply-typedにrecursive typeを実装してみた。

recursive typeはいわゆる(G)ADT相当の機能だけど、型パラメータを持たないのでADTの真面目な実装に比べると楽だと思う。

recursive typeはType -> Typeなるmappingのleast fixed pointが取れるよってやつ。
あるいは任意のF-algebraに対してinitial objectが存在する*1ことなので、単なるCCCに比べれば相当強い構造が入ることになる。

さて、initial F-algebra Iが取れているとすると、定義より任意のF-alg f:FX -> Xに対して一意的な射I --> Xが存在してそれが誘導する図式が可換になるけれど、
このとき取れるI --> XがIのelimination rule(destructor, recursor, induction function, etc)になって、
図式の可換性がelim[f](intro[ConI] a) => f (ConI a)という、言葉で言えば「コンストラクタつけてデストラクタつけたら元に戻る」というcomputation ruleを生成する。

ちなみに、initial F-algebraの構造射fI: FI -> Iがコンストラクタ(の直和)になる。

で、少し考えればこのfIは同型になるので、その逆射はI -> FIという、いわば「データ型を定義に従って直和に分解する」射になる。

このときunfold: I -> FIおよびfold: FI -> Iの2つのruleと、上に書いたようなintro[-]: (A -> FI) -> A -> Iとelim[-] : (FI -> X) -> I -> Xなる2つのruleは同値になるので、結局recursive typeの実装はこのunfold, foldを実装すればよいことになる。

という前置きをしておいて実装の話。

型のleast fixpoint operatorをμでかく。

- fold rule:
f: F(μX.FX)
--------------
fold(f): μX.FX


- unfold rule:
f: μX.FX
-------------------
unfold(f): F(μX.FX)

- computation rule:
unfold (fold (f)) => f

で、typing functionは次のような感じ。
(例によって証明もしてないし何も見てないので合ってる保証はない)

typing(fold[F](e)) = unify(typing(e), F(μX.FX)); μX.FX
typing(unfold[F](e)) = F(unify(typing(e), μX.FX))

(fold, unfold以外のtypingについては前回のλμの記事参照)

あとはこれを気合で実装すれば動く。
コードは[2]を参照。

それと、inductive datatypeだけではあんまり遊べないので、ついでに1と直和(fin. colimit)も入れておいた。
これでめでたくNat = μX. 1 + Xが定義できて、ちゃんとrecursive typeで遊べるようになった👏👏👏

コードについて

exceptionsパッケージを始めて使ってみて、これはエラーを投げて別の場所でキャッチするだけならすごく簡単なんだけど、投げたエラーをきっちりデータとしてハンドリングするにはあんまり向いてなさそうだな(そもそも例外とはそういうものかもしれないけど)と思った。
CatchTやら何やらを使うとEitherに変換はできるけどエラーはSomeExceptionというexistに囲まれた謎の型が落ちてくるので、欲しいエラー型を持っているかどうかはこれだけではよくわからないし…。

一応、テストを書くときはMaybe型にして(うまく動くかどうかだけを気にする。エラーが発生するケースのテストも、どのエラーが出たかは気にしない)、実際に例のプログラムを動かすときはIO型にすることでエラーメッセージを表示、みたいな感じで使い分けている。
でも、こういう感じで「あるときはMaybeでエラーを握りつぶして、またある時はちゃんと画面に表示して」ってことが同じプログラムに対してどのrun関数を適用するかだけで変えられるのでそこはすごく便利。

次は真面目に型パラメータつきのGADTの実装でもやろうかなと思ってる。

ただ、それをやるならどうしてもカインド推論もしないといけないし色々めんどくさいからやだな〜という。
そもそも未だにパーサーすら用意してないのでそっちが先かも(流石にいちいちApp expr1 expr2とか書くのめんどくさくなってきた気もするし…)

まぁその時の気分で✌✌✌