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

関手

関手$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                   -- 恒等射の保存

また、idやfmap . fmapも関手です。

モナド

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

\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の>>=演算子は、joinとfmapを使って次のように定義できます。

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

自然変換

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

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

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

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