モナドは「変な結合」をしている
圏の射は、cod と dom が一致しているときに結合可能というのが公理にあるけれども、モナドの「結合」ではちょっとずれている。
タイトルの「変な結合」というのは、Haskell で言うと bind (>>=) のこと。どこが変かというと
cod と dom がモナド(関手)一個分ずれているとき「結合」可能*1
というところ。どっちに一個分ずれているかは省略。
こういう見方をすると、モナド則
1. (return x) >>= f == f x 2. m >>= return == m 3. (m >>= f) >>= g == m >>= (\x -> f x >>= g)最初の規則は return が >>= に関して左単位元になっていることを要請しています。二番目の規則は return が >>= に関して右単位元になっていることを要請しています。そして、三番目の規則は >>= に関する一種の結合法則です。三番目の規則に従えば、モナドをつかった do 記法のセマンティクスは一貫性をもちます。
The monad laws
がちゃんと単位元と結合法則に見えてくる。正直今までこれが単位元とか結合法則に見えたことはなかった。なんとなくそんな雰囲気はするけど、言いくるめられたように感じていた。
(ここ以下は全く確認せず書いてます。鵜呑み注意)
で、この「変な結合」は普通の結合になれないのか?でKleisli圏。
モナドを考えている圏からKleisli圏というものを構成すると、「変な結合」は普通の結合に、return は id (恒等射)に、「一種の結合法則」は普通の結合法則になる。
マックレーン本のKleisli圏のところは抽象的でよくわからなかったけれども、それを取っ掛かりにして構成できるか考えてみたら意外に簡単にできた。もちろん証明とかはしていないけど。
モナドを知って考え始めてから一番の進歩かもしれない。ウソ書いていたらご指摘お願いします > えらい人。
*1:こういう言い方が一番しっくりくるけど、見たことがない。間違ってるんだろうか。