Kleisli TripleとMonadの対応
Kleisli TripleとMonad型クラスの定義を同時に見ることで対応を見る
Kleisli Tripleの3つ組(T,\eta,(-)^*)が以下のような対応になる
対応
| クライスリトリプル | Haskell | |
| T | 型コンストラクタM | |
| η | return | |
| (-)^* | (=<<) | 反対向きのbind |
Monad型クラスの定義
hsclass Applicative m => Monad (m :: * -> *) where
(>>=) :: m a -> (a -> m b) -> m b
return :: a -> m aまた、
(=<<) は、 (>>=) の2つの引数を入れ替えたものなので、型は、
(a -> m b) -> m a -> m b Kleisli Tripleの満たすべき3条件と、モナド則の対応
クライスリトリプル
①f^*\circ\eta_A=f
②\eta_A^*=\mathrm{id}_{TA}
③g^*\circ f^*=(g^*\circ f)^*
モナド則
hsreturn x >>= f == f x -- ①
m >>= return == m -- ②
(m >>= f) >>= g == m >>= (\x -> f x >>= g) -- ③前提
hsreturn :: A -> M A
f :: A -> B
g :: B -> Cコツは、
Monad型クラスでよく定義される
(>>=) と向きが逆であることに注意することMonad型クラスの方を
(=<<) に変換してから考えるとわかりやすくなるまたKleisli Tripleの方は、写像の話しかしていない
ポイントフリーにしてる感じ
なので良い感じに引数を与えてあげるとHaskellとの対応が取りやすくなる
モナド則の
x とか m はどこから来たの？という感じなので、例えば①も \x -> return x >>= f のように、 x を引数として与えるように書き直せば扱いやすくなる①の対応
f^*\circ\eta_A=fの左辺をそのままHaskellで書くと、
(=<<) f . return になるこの型は、
A -> B であるこれのbindの向きを変えて、
>>= を使うように変更すると、 (\x -> x >>= f) . return と書ける合成
. の仕方を考えれば、これは (\x -> return x >>= f) と同じであることがわかるこれで、両者の左辺f^*\circ\eta_Aと
return x >>= f の対応が取れた右辺も同じで、ちゃんと書けば
\x -> f x なので、対応が取れている図で見るとわかりやすい
Kleisli Tripleの図と、Haskellの記号と一緒に描いてみた
②の対応
\eta_A^*=\mathrm{id}_{TA}の左辺をそのままHaskellで書くと、
(=<<) return になるこの型は、
M A -> M A これのbindの向きを変えて、
>>= を使うように変更すると、 \m -> (=<<) return m \m -> (>>=) m return \m -> m >>= return これは、モナド則の2つ目の左辺と同じである
右辺も
m を与えてあげるようにすれば、 \m -> id m であり、これはモナド則の右辺と同じKleisli Triple#615947c819827000003e424eをHaskellの記号と一緒に描くと
③の対応
g^*\circ f^*=(g^*\circ f)^*の左辺と右辺を別々に変換していって、モナド則と同じ形にする
まず左辺を見る
g^*\circ f^*をそのままHaskellで書くと
(=<<) g . (=<<) f (\m -> (=<<) g m) . (=<<) f g の方をポイントフリーでなくした (\m -> m >>= g) . (=<<) f g の方で >>= を使うように書き換えた \m -> (=<<) f m >>= g \m -> m >>= f >>= g これで、モナド則の左辺と同じになった
右辺
(g^*\circ f)^*をそのままHaskellで書くと、
(=<<) ((=<<) g . f) (=<<) ((\x -> (=<<) g x) . f) g の方をポイントフリーでなくした (=<<) ((\x -> x >>= g) . f) g の方で >>= を使うように書き換えた (=<<) (\x -> f x >>= g) \m -> (=<<) (\x -> f x >>= g) m \m -> m >>= (\x -> f x >>= g) これで、モナド則の右辺と同じになった