クライスリ圏とMonadの対応

クライスリ圏とMonad型クラスの対応

以下の2つの関数の合成をしたい

code:hs

f :: A -> T B

g :: B -> T C

普通には合成できないのでbindを用いて以下のように合成する

code:hs

f a >>= g

f a :: T Bで、全体としてT Cになる

モナド型クラスのmethod

code:hs

(>>=) :: m a -> (a -> m b) -> m b

return :: a -> m a

このreturnは明らかに$ \etaなので、これは良いとして、

じゃあbindの方はクライスリ圏で言うと何なのか

https://gyazo.com/6718a89592567d6a53e2617ccc2e1f55

クライスリ圏の図

圏$ \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の役割を果たしている

上図のオレンジ色の太線

table:クライスリ圏との対応

クライスリ圏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

下図の青 = 赤 = 緑

https://gyazo.com/95ab5d98b06c03c92f9f1a9de18e9b66

モナドの単位律の一つ$ \mu\circ T\eta=1_Tに対応する

2つめ

上の対応表より、>>= returnが$ G((\eta_X)_T)に対応する

$ G((\eta_X)_T)=1_{T(X)}

https://gyazo.com/6017f76dca5bb13975c10e2a478534cd

モナドの単位律の一つ$ \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になる

これでモナド則を圏論表記に対応できたので、ここから左辺を導出する

https://gyazo.com/911c6c1a9540b743aa5b13da86485ecf

https://gyazo.com/82769c50428568758bdec303d29e2e2e

https://gyazo.com/b1fd99e16b49bf51e444e42a927cd066