Monad合成

Monad合成はできました。

http://www.ie.u-ryukyu.ac.jp/%7Ekono/lecture/software/s07/lecture.html

こんな感じでできるらしい。明日の授業のネタだけど。こんな自転車操業でいいのか? これにも一週間かかった。慣れもあると思うけど。自分で Monad を書く話は、あまりぐぐっても出てこない。あまり書かないものらしいです。

昨日はせっかく飲みに行ったのに、Monad 合成の話が抜けなくて、結局、途中で帰ってきてしまいました。酒よりも、面白いものはたくさんあるね。

論文の締め切りも過ぎたので一段落かも。なので、Adjoint と Universal mapping の証明の Agda 版にも手を付けて見ました。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/tip/universal-mapping.agda

これで半分行ってないかな。 これも楽しめるな〜