クライスリ圏とMonadの対応
以下の2つの関数の合成をしたい
hsf :: A -> T B
g :: B -> T C普通には合成できないのでbindを用いて以下のように合成する
hsf a >>= g f a :: T B で、全体として T C になるモナド型クラスのmethod
hs(>>=) :: m a -> (a -> m b) -> m b
return :: a -> m aこのreturnは明らかに\etaなので、これは良いとして、
じゃあbindの方はクライスリ圏で言うと何なのか
クライスリ圏の図
圏\mathscr{A}_Tは圏\mathscr{A}のクライスリ圏
Haskellには出てこないがモナドの\mu: m a \to aがbindに含まれている
関手で包んだ射
T g は TB->TTC になるこれと
μ を合成することで、\mu\circ Tg::TB\to TCになるつまり対応としては、
(1) , (2) を未適用の引数として、以下のように書ける bind (1) (2) :: m a -> (a -> m b) -> m b (μ○T(2)) (1) :: m a -> (a -> m b) -> m b 引数の順番と場所の関係で変な記法になっているが
つまりbindの中に
μ :: m a -> a が含まれている関数
f :: X -> T Y に対して、 >>= f :: T X -> T Y になるので、bindは上図で言う関手Gの役割を果たしている上図のオレンジ色の太線
クライスリ圏との対応
| クライスリ圏A_T | 関手G | 圏A | Haskell |
| f_T | G(f_T) | μ○T(f) | >>= f |
| η_T | G(η_T) | η | return |
モナド則との対応
ポイントフリーにして考えると良い
1つめ
上の対応表より、
return . (>>= f) これが
f に等しくなる\mu_Y\circ Tf \circ \eta_X = \mu_Y\circ\eta_Y\circ f = f
下図の
青 = 赤 = 緑 
モナドの単位律の一つ\mu\circ T\eta=1_Tに対応する
2つめ
上の対応表より、
>>= return がG((\eta_X)_T)に対応するG((\eta_X)_T)=1_{T(X)}
モナドの単位律の一つ\mu\circ\eta T=1_Tに対応する
上の対応表より、
>>= g は\mu_Z\circ Tgなので \x -> f x >>= g は\mu_Z\circ Tg \circ fであり >>= (\x -> f x >>= g) は\mu_Z\circ T(\mu_Z)\circ Tg\circ fになるこれでモナド則を圏論表記に対応できたので、ここから左辺を導出する
