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 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拡張を定義するあたりです。
おわり