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