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

モナド則から導きだせる規則

(工事中 50%)

はじめに

モナド則から導かれる規則を示す。見やすさを考慮してモナド内包表記で表現する。モナド則から導かれる規則を見れば、それが直観的に「成り立っていてほしい」規則であることがわかるだろう。

モナド則の変換

モナド則として

(...演算子(>=>)を使ったモナド則...)

の3つを紹介した。直観的にわかりやすい規則だ。しかし

(...演算子(>>=)を使ったモナド則...)

のように変形したほうが使いやすい。これは

(...式変形...)

のようにして示すことができる。

そのまま

(以下を示すこと)

[ x | x <- u ] == u

returnは消せる

(以下を示すこと)

[ f x' | ..., x' <- return x, ... ] == [ f x | ..., ... ]

内側のfmap

(以下を示すこと)

[ f x' | ..., x' <- fmap g mx, ...] == [ f (g x) | ..., x <- mx, ...]

モナド則の連鎖

(m0 >>= \v0 -> m1 >>= \v1 -> ... mn >>= \vn -> return r) >>= f
=> m0 >>= \v0 -> (m1 >>= \v1 -> ... mn >>= \vn -> return r) >>= f
.
.
.
=> m0 >>= \v0 -> m1 >>= \v1 -> ... mn >>= \vn -> return r >>= f
=> m0 >>= \v0 -> m1 >>= \v1 -> ... mn >>= \vn -> f r

内包表現とfmap

fmap g [ r | v0 <- m0, ..., vn <- mn ]
=> (m0 >>= \v0 -> ... mn >>= \vn -> return r) >>= return . g
=> m0 >>= \v0 -> ... mn >>= \vn -> return (g r)
=> [ g r | v0 <- m0, ..., vn <- mn ]

内包表記の先頭のネスト

[ r | (w0, ..., wn) <- [ (w0, ..., wn) | w0 <- n0, ..., wn <- nn ], ..., vn <- mn ]
=> (n0 >>= \w0 -> ... nn >>= \wn -> return (w0, ..., wn)) >>= \(w0, ..., wn) -> ... mn >>= \vn -> return r
=> n0 >>= \w0 -> ... nn >>= \wn -> ... mn >>= \vn -> return r
=> [ r | w0 <- n0, ..., wn <- nn, ..., vn <- mn ]

内包表記の中間のネスト

[ r | v0 <- m0, ..., (w0, ..., wn) <- [ (w0, ..., wn) | w0 <- n0, ..., wn <- nn ], ..., vn <- mn ]
=> m0 >>= \v0 -> [ r | v1 <- m1, ..., (w0, ..., wn) <- [ (w0, ..., wn) | w0 <- n0, ..., wn <- nn ], ... vn <- mn ]
=> m0 >>= \v0 -> ... [ r | (w0, ..., wn) <- [ (w0, ..., wn) | w0 <- n0, ..., wn <- nn], ..., vn <- mn ]
=> m0 >>= \v0 -> ... [ r | w0 <- n0, ..., wn <- nn, ..., vn <- mn ]
=> [ r | v0 <- m0, ... w0 <- n0, ..., wn <- nn, ..., vn <- mn ]

まとめ

モナド則から以下の規則が導けた。

fmap f [ r | ... ] == [ f r | ... ]

[ r | ..., (v0, ..., vn) <- [ (v0, ..., vn) | v0 <- m0, ... vn <- mn ], ... ]
== [ r | ..., v0 <- m0, ... vn <- mn, ... ]

「拡張機能: MonadComprehensions」へもどる 「モナド則からモノイダル則を導く」へ

メモ

!!これはだめだ。Monadクラスを説明してない。しかし、Monadクラスを説明するには'Applicative m =>'がからんでくるし、難しいところだ。

モナド則からモノイダル則を導くのはMonadクラス等の紹介が終わったあとにしようかな。とりあえずは「モナド則からモノイダル則が導けます」とだけ言っておいて、あとで示すといった感じか。

モナド則からモノイダル則を導くのに以下の2つの規則が使えるとスムーズだ。

fmap f [ ret | ... ] == [ f ret | ... ]

[ ret | ..., (x, y) <- [ (x, y) | x <- u, y <- v ], ... ] == [ ret | ..., x <- u, y <- v, ... ]

これらをわかりやすく示したい。見やすさのためにMonadComprehensions拡張を紹介してしまおう。

途中に直観的にわかりやすい規則をはさむのがコツだと思う。

参考: リスト内包表記の変形

m >>= f >>= g

メモ2

(m >>= f) >>= g

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

[ z | y <- [ y | x <- m, y <- f x ], z <- g y ]
(m >>= f) >>= (\y -> g y >>= return)

[ z | x <- m, y <- f x, z <- g y ]
m >>= (\x -> f x >>= (\y -> g y >>= return))

f' x == fmap (x ,) (f x)とおくと

f' x
=> fmap (x ,) (f x)
=> f x >>= return . (x ,)
=> f x >>= \y -> return (x, y)

[ z | y <- [ y | x <- m, y <- f' x ], z <- g y ]
[ z | xy <- [ (x, y) | x <- m, y <- f x ], z <- g xy ]
[ z | (x, y) <- [ (x, y) | x <- m, y <- f x ], z <- g (x, y) ]

[ z | x <- m, y <- f' x, z <- g y ]
[ z | x <- m, y <- f x >>= \y -> return (x, y), z <- g y ]
[ z | x <- m, (x, y) <- f x >>= \y -> return (x, y), z <- g (x, y) ]
[ z | x <- m, z <- (f x >>= \y -> return (x, y)) >>= \(x, y) -> g (x, y) ]
[ z | x <- m, z <- f x >>= \y -> return (x, y) >>= \(x, y) -> g (x, y) ]
[ z | x <- m, z <- f x >>= \y -> g (x, y) ]
m >>= \x -> (f x >>= \y -> g (x, y)) >>= \z -> return z
m >>= \x -> f x >>= \y -> g (x, y)
m >>= \x -> f x >>= \y -> g (x, y) >>= \z -> return z
[ z | x <- m, y <- f x, z <- g (x, y) ]

do { y <- do { x <- m; f x }; g y }

do { x <- m; y <- f x; g y }

[ (x, (y, z)) | x <- u, (y, z) <- [ (y, z) | y <- v, z <- w ] ]
do { x <- u; (y, z) <- do { y <- v; z <- w; return (y, z) }; return (x, (y, z)) }
u >>= \x -> (v >>= \y -> w >>= \z -> return (y, z)) >>= \(y, z) -> return (x, (y, z))
u >>= \x -> v >>= \y -> (w >>= \z -> return (y, z)) >>= \(y, z) -> return (x, (y, z))
u >>= \x -> v >>= \y -> w >>= \z -> return (y, z) >>= \(y, z) -> return (x, (y, z))
u >>= \x -> v >>= \y -> w >>= \z -> return (x, (y, z))
[ (x, (y, z)) | x <- u, y <- v, z <- w ]

[ ((x, y), z) | (x, y) <- [ (x, y) | x <- u, y <- v ], z <- w ]
do { (x, y) <- do { x <- u; y <- v; return (x, y) }; z <- w; return ((x, y), z) }
(u >>= \x -> v >>= \y -> return (x, y)) >>= \(x, y) -> w >>= \z -> return ((x, y), z)
u >>= \x -> (v >>= \y -> return (x, y)) >>= \(x, y) -> w >>= \z -> return ((x, y), z)
u >>= \x -> v >>= \y -> return (x, y) >>= \(x, y) -> w >>= \z -> return ((x, y), z)
u >>= \x -> v >>= \y -> w >>= \z -> return ((x, y), z)
[ ((x, y), z) | x <- u, y <- v, z <- w ]

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

(f x >>= g) >>= h
(f >=> g) x >>= h
((f >=> g) >=> h) x

f x >>= (\y -> g y >>= h)
f x >>= (\y -> (g >=> h) y)
f x >>= (g >=> h)
(f >=> (g >=> h)) x

f = const u, g = const v, h = const w

[ (x, (y, z)) | x <- u, y <- v, z <- w ]
u >>= \x -> v >>= \y -> w >>= \z -> (x, (y, z))
f a >>= \x -> g x >>= \y -> h y >>= \z -> (x, (y, z))
(f >=> \x -> g x >>= \y -> h y >>= \z -> (x, (y, z))) a
(f >=> \x -> (g >=> \y -> h y >>= \z -> (x, (y, z))) x) a

メモ3

mf <*> mx
=> [ f x | f <- mf, x <- mx ]

pure (,) <*> mx <*> my
=> [ g y | g <- (pure (,) <*> mx), y <- my ]
=> [ g y | g <- [ f x | f <- return (,), x <- mx ], y <- my ]
=> [ g y | g <- [ (x ,) | x <- mx ], y <- my ]
=> (mx >>= \x -> return (x ,)) >>= \g -> my >>= \y -> return g y
=> mx >>= \x -> return (x ,) >>= \g -> my >>= \y -> return g y
=> mx >>= \x -> my >>= \y -> return (x, y)
=> [ (x, y) | x <- mx, y <- my ]

(exp0 >>= \v0 -> exp1 >>= \v1 -> exp2 >>= \v2 -> ... expn >>= \vn -> expr) >>= expk
=> exp0 >>= \v0 -> (exp1 >>= \v1 -> exp2 >>= \v2 -> ... expn >>= \vn -> expr) >>= expk
.
.
.
=> exp0 >>= \v0 -> exp1 >>= \v1 -> exp2 >>= \v2 -> ... expn >>= \vn -> expr >>= expk

[ r | v0 <- m0, v1 <- m1, ..., vn <- mn ]
m0 >>= \v0 -> m1 >>= \v1 -> ... mn >>= \vn -> return r
(m0 >>= \v0 -> m1) >>= \v1 -> ... mn >>= \vn -> return r
[ r | v1 <- [ v | v0 <- m0, v <- m1 ], ... vn <- mn ]

メモ4

(m0 >>= \v0 -> m1 >>= \v1 -> m2 >>= \v2 -> ... mn >>= \vn -> return r) >>= f
=> m0 >>= \v0 -> (m1 >>= \v1 -> m2 >>= \v2 -> ... mn >>= \vn -> return r) >>= f
.
.
.
=> m0 >>= \v0 -> m1 >>= \v1 -> m2 >>= \v2 -> ... mn >>= \vn -> return r >>= f
=> m0 >>= \v0 -> m1 >>= \v1 -> m2 >>= \v2 -> ... mn >>= \vn -> f r

[ r'' | r' <- [ r | v0 <- m0, ..., vn <- mn ], r'' <- f r' ]
=> [ r'' | r' <- [ (v0, ..., vn) | v0 <- m0, ..., vn <- mn ], r'' <- f r' ]
=> [ r'' | v0 <- m0, ..., vn <- mn, r'' <- f (v0, ..., vn) ]

[ r | v0 <- m0, ..., vn <- mn ]
m0 >>= \v0 -> [ r | v1 <- m1, ..., vn <- mn ]

メモ5

[ r | v0 <- m0, ... vk <- [ s | w0 <- n0, ..., wn <- nn ], ..., vn <- mn ]
m0 >>= \v0 -> ... m(k-1) >>= \v(k-1) -> [ r | vk <- [ s | w0 <- n0, ..., wn <- nn ], ..., vn <- mn ]
m0 >>= \v0 -> ... m(k-1) >>= \v(k-1) -> [ r | (w0, ..., wn) <- [ (w0, ..., wn) | w0 <- n0, ..., wn <- nn ], ..., vn <- mn ]
m0 >>= \v0 -> ... m(k-1) >>= \v(k-1) -> [ r | w0 <- n0, ..., wn <- nn, v(k+1) <- m(k+1), ..., vn <- mn ]
[ r | v0 <- m0, ..., v(k-1) <- m(k-1), w0 <- n0, ..., wn <- nn, v(k+1) <- m(k+1), ..., vn <- mn ]

「拡張機能: MonadComprehensions」へもどる 「モナド則からモノイダル則を導く」へ

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