Posted at

具体的な値でモナド則を確認する - List編

モナド則に具体的な値をいれて理解を深めてみましょう。

今回はListを使ってみます。


モナド則

モナド則を確認しておきましょう。

return x >>= f == f x

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


Listの実装

Listの実装を確認しておきます。

return x = [x]

x >>= f = foldr (\y acc -> f y ++ acc) [] x


モナド則に具体的な値をいれてみよう


return x >>= f == f x


xが1 で fが \a -> [a+1] の場合


左辺

return x >>= f

-- xは1である
return 1 >>= f

-- return を適用
[1] >>= f

-- >>= を適用
foldr (\y acc -> f y ++ acc) [] [1]

-- foldrを適用
f 1 ++ []

-- fは \a -> [a+1]
(\a -> [a+1]) 1 ++ []

-- 無名関数を適用
[1+1] ++ []

-- 残りを計算
[2]


右辺

f x

-- xは1である
f 1

-- fを適用
[1+1]

-- 残りを計算
[2]

右辺と左辺が一致した


xが1 で fが \a -> [a, a+1] の場合


左辺

return x >>= f

-- xは1である
return 1 >>= f

-- return を適用
[1] >>= f

-- >>= を適用
foldr (\y acc -> f y ++ acc) [] [1]

-- foldrを適用
(\y acc -> f y ++ acc) 1 []

-- 無名関数を処理
f 1 ++ []

-- fを置き換えて、関数を適用
[1, 1+1] ++ []

-- 残りを計算
[1, 2]


右辺

f x

-- xは1である
f 1

-- fを適用
[1, 1+1]

-- 残りを計算
[1, 2]

右辺と左辺が一致した


m >>= return == m


m[]の場合


左辺

m >>= return

-- mは[]
[] >>= return

-- >>= を適用
foldr (\y acc -> f y ++ acc) [] []

-- foldrを適用
[]

mに一致する。


m[1]の場合


左辺

m >>= return

-- mは[]
[1] >>= return

-- >>= を適用
foldr (\y acc -> f y ++ acc) [] [1]

-- foldrを適用
(\y acc -> f y ++ acc) 1 []

-- 無名関数を処理
f 1 ++ []

-- fを適用
return 1 ++ []

-- returnを適用
[1] ++ []

-- 残りを処理
[1]

mに一致した。


m[1, 2]の場合


左辺

m >>= return

-- mは[]
[1, 2] >>= return

-- >>= を適用
foldr (\y acc -> f y ++ acc) [] [1, 2]

-- foldrを適用
(\y acc -> f y ++ acc) 1 $ (\y acc -> f y ++ acc) 2 []

-- $より後ろを処理
(\y acc -> f y ++ acc) 1 [2]

-- 無名関数を適用
f 1 ++ [2]

-- fを適用
return [2] ++ [2]

-- returnを適用
[1] ++ [2]

-- 残りを処理
[1, 2]

mに一致した。


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


m[1], fが \a -> [a+1]gが \b -> [b+2]` の場合


左辺

(m >>= f) >>= g

-- 疲れたので一気に処理(心の声)
[1 + 1] >>= g
[2] >>= g
[2+2]
[4]


右辺

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

foldr (\y acc -> (\x -> f x >>= g) y ++ acc) 1 []
((\x -> f x >>= g) 1) ++ []
(f 1 >>= g) ++ []
([1 + 1] >>= g) ++ []
[2 + 2] ++ []
[4]


m[1, 2], fが \a -> [a+1]gが \b -> [b+2]` の場合


左辺

(m >>= f) >>= g

([1, 2] >>= f) >>= g
[2, 3] >>= g
[4, 5]


右辺

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

foldr (\y acc -> (\x -> f x >>= g) y ++ acc) [1,2] []
([1+1] >>= g) ++ ([2+1] >>= g) ++ []
[2+2] ++ [3+2] ++ []
[4, 5]

左辺と右辺が一致した。

雰囲気がだけ察してほしい。


関連

https://qiita.com/eielh/items/cc4293ffefb1730f044b