Edited at

圏論のモナドの法則からHaskellでよくみる形のモナド則を導き出す

More than 3 years have passed since last update.


関手

関手$F$は、次の法則を満たします。

F(f \circ g) = F(f) \circ F(g) \\

F(1_A) = 1_{F(A)}

fmapは関手です[追記]1[/追記]。つまり、次の法則が成り立ちます。

fmap (f . g) = fmap f . fmap g -- 合成の保存

fmap id = id -- 恒等射の保存

また、idfmap . fmapも関手です。


モナド

モナド$(T, \eta, \mu)$の自然変換$\eta$と$\mu$は、それぞれHaskellのreturnjoinに相当します。

\mu_A \circ \mu_{T(A)} = \mu_A \circ T(\mu_A) \\

\mu_A \circ \eta_{T(A)} = 1_{T(A)} = \mu_A \circ T(\eta_A)

という法則は、Haskellで言えば

join . join = join . fmap join

join . return = id = join . fmap return

です。

Haskellの>>=演算子は、joinfmapを使って次のように定義できます。

m >>= f = join (fmap f m)


自然変換

自然変換$\theta_A : F(A) \rightarrow G(A)$は、次の法則(自然性)を満たします。

\theta_B \circ F(f) = G(f) \circ \theta_A

returnjoinも自然変換なので、自然性が成り立ちます。

return . id f = fmap f . return

join . (fmap . fmap) f = fmap f . join


モナド則

以上のことから、次のモナド則を導いてみます。(出典: The monad laws)

1. return x >>= f = f x

2. m >>= return = m
3. (m >>= f) >>= g = m >>= (\x -> f x >>= g)


1. return x >>= f = f x

return x >>= f

= join (fmap f (return x)) -- (>>=)の定義を展開
= (join . fmap f . return) x -- 関数の合成を使った形に書き換え
= (join . return . id f) x -- returnの自然性
= (id . id f) x -- join . return = id
= f x


2. m >>= return = m

m >>= return

= join (fmap return m) -- (>>=)の定義を展開
= (join . fmap return) m -- 関数の合成を使った形に書き換え
= id m -- join . fmap return = id
= m


3. (m >>= f) >>= g = m >>= (\x -> f x >>= g)

(m >>= f) >>= g

= join (fmap g (join (fmap f m))) -- (>>=)の定義を展開
= (join . fmap g . join . fmap f) m -- 関数の合成を使った形に書き換え
= (join . join . fmap (fmap g) . fmap f) m -- joinの自然性
= (join . fmap join . fmap (fmap g) . fmap f) m -- join . join = join . fmap join
= (join . fmap (join . fmap g . f)) m -- 合成の保存
= join (fmap (join . fmap g . f) m) -- 関数の合成の展開
= m >>= (join . fmap g . f) -- (>>=)の定義を使った書き換え
= m >>= (\x -> (join . fmap g . f) x) -- η変換の逆
= m >>= (\x -> (join (fmap g (f x)))) -- 関数の合成の展開
= m >>= (\x -> f x >>= g) -- (>>=)の定義を使った書き換え

以上より、モナドについて、上記3つのモナド則が満たされることがわかりました。

TODO: その逆、モナド則を満たすならモナドであることを示す。

1. [追記]ここのところについて、関数で関手が表現できるって変でしょ、どういう仕掛けかな? - 檜山正幸のキマイラ飼育記が分かりやすく解説しています。[/追記]