Just $ A sandbox

プログラミングと計算機科学とかわいさ

トップ > Haskell

Freer Monadじゃあないんですよ

Haskell Coq 圏論

Extensible Effectsという、大変有名なモナドの合成方法があって、まぁこれはいいんだけど、関連する話でFreer monads, more extensible effectsという論文があり、これまた界隈では有名なんだけどなんやねんって話。

とりあえずext effはモナドを直和していい感じにするってことと、freerはOperational Monadを使ったんやなってことがわかっていればひとまずクリアという感じ。

よく知らない人はこれ読んで めっちゃわかりやすいから👇

www.slideshare.net

さて、まぁ上のような説明も上にあげた論文もHaskellのコードしか書いてなくてさっぱり分からないのでもっとちゃんと定式化しようねということを簡単にまとめます。

というか主にOperational monadの話な気がする。

Free Monad

今更言うまでもないけどFree monadはforgetful U : Mon{C} -> [C,C]のleft adjointである。

Old Eff

Freerじゃない方のExt Effは次で定まるものである。

Eff <Ti> := Free((+)Ti)

(+)TiはTiたちの直和のことで、TiたちがfunctorであればEff <Ti>はモナドになるし、(+)Ti -> (+)SjなるnatはEffの間のmonad morphismを誘導する。

Operational Monad

Operational MonadはOpM = Free . Coyoneda : [Ob(C),Ob(C)] -> Mon{C}っていう形のやつで、
CのObjectの間のmap familyがあればそこからモナドが作れるというなかなか面白いやつです。

ちなみにCoyonedaというのは次のようなもの:

Coyoneda f = Lan f 1 = 1†f = ∃b. (hom(b,-),Fb)

一番最後の形はKan拡張をcoendでかいたやつで、右のタプルをbに渡って直和を取ったものと思えばいい。

coend形を見れば、なぜOb(C)の間のmap familyがFunctorに拡張できるのかはすぐにわかると思う。

Freer Monad

これを使って次のようにしよう:

Eff <Ti> := Free(Coyoneda((+)Ti)) = OpM (+)Ti

すると、map family(+)Tiからモナドが得られる。

つまり、ただのmap familyたちTiがあると、(これは例えばGADTとかで1変数データ型を適当に作ってやればいい)
それらの作用をすべて含むモナドができて嬉しいねという話である。

さらにこれはいくつかの便利operationがあって、

send : Ti --> Eff<Ti> (injectionみたいなやつ)や
run : (T --> Ti) -> (Eff (T : <Ti>) --> Eff <Ti>) (injectionのMonad morphismへの持ち上げ)みたいなやつが得られるので

まぁ便利ねということである。

とかいうことを真面目にpdfにしようかなと思ったんだけど
需要があるのかよくわからないしやめました

でもせっかくなのでformalizeとかしたいねという気持ちはたしかにあります
ところで以下のようなcategory theory formalize projectがありますので(唐突な宣伝)
協力してくれる人、困ったときに相談に乗ってくれる人なんかがいましたらぜひに。

ちなみに現在の進捗は非常に辛かったコンマ圏のuniversalityを示し、そろそろ各点Kan拡張を定義するあたりです。

github.com

おわり

Recursive Typeの実装

λ-caluculus Haskell

前回は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とか書くのめんどくさくなってきた気もするし…)

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

参考文献

*1:任意のデータ型はinitial F-algebraでかける

λμのTypeCheckerの実装

λ-caluculus Haskell

λμの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でやるなりしたいなーと思いつつやってない。

とりあえず良い練習にはなったので他の型システムも随時実装していきたい。

参考文献