Monad の例

最近、はまってた Agda の例をまとめているんですが、(何回目の清書だよ) そういえば、Monad の例がない。例がなくても証明がどんどん進むところが圏論っぽいところなんだけど。

Higher order categorical logic に載っている例が、

T : A -> M x A ( M は monoid )
η : a -> (1,a)
μ : (m, (m', a ) -> (m*m', a)

っていう例でなかなか良くできてます。これを Haskell で、そのまま Monad として動かすのもできた。

なんだが、Agda で全然書けない。Agda こういうの多いんだよな。どう書けば良いのかさっぱり。本来、T ってのは、圏A に対して、

T : A -> A

だったよね? T : A -> M x A を Sets -> Sets と考えると本には書いてある。それって、Agda では、どうするんですか?

(1) Sets と直積を使って T という Functor を作る
(2) M x ( M x ... A )) っていう圏を作って、その上にTを定義する

の二種類の方法を考えて、どっちも、そなりに途中まで書けたんですが、なんかだめ。だめだ。これじゃない感です。なにか思い違いしているんだろうな〜

例がないってのもあんまりだし、実際の Monad と結びつかないってのもまずいからなぁ。

土曜日は xhago に顔出して懇親会にも寄って来ました。アプリ作りましたみたいなのが多い。良いね。次はハッカーズチャンプルーが8/24。その後から東京かな。ソフトウェア科学会まで、しばらく東京の予定です。