top page > computer > haskell > web_lecture > for_programmer > monad_to_monoidal_law.html
更新日:
文責: 重城良国

モナド則からモノイダル則を導く

(工事中 50%)

はじめに

モナドならアプリカティブファンクターである。それを示すためにはモナド則からモノイダル則を導く必要がある。

定義

モナド関数によるアプリカティブ関数の定義は

となる。モノイダル則は

として

となる。

展開

関数fmapとモノイダル関数をモナド関数まで展開する。

fmap f mx = pure f <*> mx
=> [ f' x | f' <- return f, x <- mx ]
=> [ f x | x <- mx ]
=> mx >>= return . f

unit = pure ()
=> return ()

u .** v = pure (,) <*> u <*> v
=> [ g y | g <- pure (,) <*> u, y <- v ]
=> [ g y | g <- [ f x | f <- return (,), x <- u ], y <- v ]
=> [ g y | g <- [ (x ,) | x <- u ], y <- v ]
=> [ g y | g <- fmap (,) [ x | x <- u ], y <- v ]
=> [ ((,) x) y | x <- [ x | x <- u ], y <- v ]
=> [ (x, y) | x <- u, y <- v ]

モノイダル則

モノイダル則を導く。

fmap snd (unit .** v)
=> fmap snd [ (x, y) | x <- return (), y <- v ]
=> [ snd ((), y) | y <- v ]
=> [ y | y <- v ]
=> v

fmap fst (u .** unit)
=> fmap fst [ (x, y) | x <- u, y <- return () ]
=> [ fst (x, ()) | x <- u ]
=> [ x | x <- u ]
=> u

fmap asl (u .** (v .** w))
=> fmap asl [ (x, (y, z)) | x <- u, (y, z) <- [ (y, z) | y <- v, z <- w ] ]
=> [ asl (x, (y, z)) | x <- u, y <- v, z <- w ]
=> [ ((x, y), z) | x <- u, y <- v, z <- w ]

(u .** v) .** w
=> [ ((x, y), z) | (x, y) <- [ (x, y) | x <- u, y <- v ], z <- w ]
=> [ ((x, y), z) | x <- u, y <- v, z <- w ]

まとめ

モナド則からモノイダル則を導くことができた。よってモナドならばアプリカティブファンクターだ。

「モナド則から導ける規則」へもどる 「モナド: 計算のログ」へ


メモ

以降はすべてメモだ。他で書いたものを保存してある。

モナドはすべてアプリカティブファンクター

(モナド則からモノイド則を導くのが煩雑だ。すこし考える必要がある)

関数appは関数bindで

u `app` v = u `bind` \f -> v `bind` \x -> ret (f x)

のように定義することができる。また、pure = retと定義できる。すると

unit = ret ()

であり

((m `bind` f) `bind` g == m `bind` \x -> f x `bind` g)

((m `bind` \x -> f x) `bind` g == m `bind` \x -> f x `bind` g)

u `tup` v
=> pure (,) `app` u `app` v
=> (ret (,) `bind` \f -> u `bind` \x -> ret (f x)) `app` v
=> (u `bind` \x -> ret (x ,)) `app` v
=> (u `bind` \x -> ret (x ,)) `bind` \f -> v `bind` \y -> ret (f y)
=> u `bind` \x -> ret (x ,) `bind` \f -> v `bind` \y -> ret (f y)
=> u `bind` \x -> v `bind` \y -> ret (x, y)

となる。

fmap snd (unit `tup` v)
=> fmap snd (ret () `tup` v)
=> fmap snd (ret () `bind` \x -> v `bind` \y -> ret (x, y))
=> fmap snd (v `bind` \y -> ret ((), y))
=> fmap snd $ v `bind` ret . (() ,)
=> fmap snd $ fmap (() ,) v
=> fmap (snd . (() ,)) v
=> fmap id v
=> v

fmap fst (u `tup` unit)
=> fmap fst (v `tup` ret ())
=> fmap fst (v `bind` \x -> ret () `bind` \y -> ret (x, y))
=> fmap fst (v `bind` \x -> ret (x, ()))
=> fmap fst (v `bind` ret . (, ()))
=> fmap fst $ (`bind` ret . (, ())) v
=> fmap fst $ fmap (, ()) v
=> fmap (fst . (, ())) v
=> fmap id v
=> v

(u `bind` \x -> v `bind` \y -> ret (x, y)) `bind` \(x, y) -> f x y
=> u `bind` \x -> (v `bind` \y -> ret (x, y)) `bind` \(x, y) -> f x y
=> u `bind` \x -> v `bind` \y -> (\y -> return (x, y)) y `bind` \(x, y) -> f x y
=> u `bind` \x -> v `bind` \y -> return (x, y) `bind` \(x, y) -> f x y
=> u `bind` \x -> v `bind` \y -> f x y

fmap asl (u `tup` (v `tup` w))
=> fmap asl (u `bind` \x -> (v `tup` w) `bind` \yz -> ret (x, yz))
=> fmap asl (u `bind` \x -> (v `bind` \y -> w `bind` \z -> ret (y, z)) `bind` \yz -> ret (x, yz)
=> fmap asl (u `bind` \x -> v `bind` \y -> w `bind` \z -> ret (x, (y, z)))
=> (u `bind` \x -> v `bind` \y -> w `bind` \z -> ret (x, (y, z))) `bind` ret . asl
=> u `bind` \x -> (v `bind` \y -> w `bind` \z -> ret (x, (y, z))) `bind` ret . asl
=> u `bind` \x -> v `bind` \y -> (w `bind` \z -> ret (x, (y, z))) `bind` ret . asl
=> u `bind` \x -> v `bind` \y -> w `bind` \z -> ret (x, (y, z)) `bind` ret . asl
=> u `bind` \x -> v `bind` \y -> w `bind` \z -> ret (asl (x, (y, z)))
=> u `bind` \x -> v `bind` \y -> w `bind` \z -> ret ((x, y), z)
=> u `bind` \x -> v `bind` \y -> ret (x, y) `bind` \(x, y) -> w `bind` \z -> ret ((x, y), z)
=> u `bind` \x -> (v `bind` \y -> ret (x, y)) `bind` \(x, y) -> w `bind` \z -> ret ((x, y), z)
=> (u `bind` \x -> v `bind` \y -> ret (x, y)) `bind` \(x, y) -> w `bind` \z -> ret ((x, y), z)
=> (u `tup` v) `tup` w

「モナド則から導ける規則」へもどる 「モナド: 計算のログ」へ

正当なCSSです! HTML5 Powered with CSS3 / styling, and Semantics