20
21

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 5 years have passed since last update.

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

Last updated at Posted at 2015-01-16

関手

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

20
21
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
20
21

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?