Just $ A sandbox

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

Freer Monadじゃあないんですよ

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 MonadOpM = 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

おわり