リストモナド \(L\) と任意のモナド \(M\) を合成してモナド \(ML\) を作れることを示す.
次はいわゆるリストモナド
map :: (a -> b) -> [a] -> [b]
map f [x, y, ...] = [f x, f y, ...]
unit :: a -> [a]
unit x = [x]
join :: [[a]] -> [a]
join = concatモナドはこれを一般化したもので、[a] を M a と書く. モナドには次の3つの関数があって、
map :: (a -> b) -> M a -> M b
unit :: a -> M a
join :: M (M a) -> M a更に次の7つの制約が成立することを要請する.
-- M-1
map id == id
-- M-2
map (f . g) == map f . map g
-- M-3
map f . unit == unit . f
-- M-4
map f . join == join . map (map f)
-- M-5
join . unit == id
-- M-6
join . map unit == id
-- M-7
join . map join == join . join型 (a や M a) を対象とし、(1変数の) 関数を射とするような所謂 Hask 圏を考える (恒等写像 id が恒等射). M-1 と M-2 は map が Hask 圏から Hask 圏への関手であることを言っている (関手としての定義を満たす; 恒等射を恒等射に写してかつ準同型).
対象 (型) a について map a という対象 (型) を M a と書いてると思う. (この M のことを単にモナドという.) つまり、
map は f: a -> b を map f: M a -> M b に写すM-4 は unit が恒等関手から関手 map への自然変換であることを言っている.
M-5 M-6 は unit と map unit とが join の右単位元であること. M-7 は 一種の結合則.
リストにはリスト内包があるのだからモナドにもモナド内包が考えられる. リスト内包表記と全く同様の表記法と定義を与える.
-- mc-1
[ t ] == [ t | Empty ] == unit t
-- mc-2
[ t | x <- u ] == map (\x -> t) u
-- mc-3
[ t | p, q ] == join [ [ t | q ] | p ]ここで Empty は空を表現するシンボル.
mc-3 で [ t | p, q, r ] みたいに3つ以上ある場合を網羅してないように見えるが、 適当に [ t | p, (q, r) ] みたいに２つにグルーピングする. グルーピングに関して (p, q), r としても p, (q, r) としても同じであるという、 一種の結合則が成立するがこれについては後述.
特に最後の mc-3 だが、順序故に
[(x, y) | x <- [1, 2], y <- [3, 4]]
== join [[(x, y) | y <- [3, 4]] | x <- [1, 2]]
== join [[(x, 3), (x, 4)] | x <- [1, 2]]
== join [[(1, 3), (1, 4)], [(2, 3), (2, 4)]]
== [(1, 3), (1, 4), (2, 3), (2, 4)]とか
[x | xs <- ls, x <- xs]
== join [[x | x <- xs] | xs <- ls]
== join [(map (\x -> x) xs) | xs <- ls]
== join [xs | xs <- ls]
== join (map (\xs -> xs) ls)
== join lsていう感じになる.
さてモナド内表表記を用いると初めのモナドに関する記述を書き直せる. 例えば M-5 M-6 M-7 は
-- M-5
[ t | Empty, q ] == [ t | q ]
-- M-6
[ t | q, Empty ] == [ t | q ]
-- M-7
[ t | (p, q), r ] == [ t | p, (q, r) ]と同じ. M-7 だけやってみる. join . join == join . map join を仮定したとき
[ t | (p, q), r ]
== join [[ t | r ] | p, q ]
== join . join [[[ t | r ] | q ] | p ]
== join . map join [[[ t | r ] | q ] | p ] -- !!
== join [join [[ t | r ] | q ] | p ]
== join [[ t | (q, r) ] | p ]
== [ t | p, (q, r) ]!! のとこで開けば逆も示せて結局、2つの M-7 は同値であることが分かる.
次の3つは mc-1 から mc-3 を使って示せるが有用な命題
-- mc-4
[ f t | p ] == map f [ t | p ]
-- mc-5
[ x | x <- u ] == u
-- mc-6
[ t | p, x <- [ u | q ], r ] == [ t' | p, q, r' ]ここで t' 及び r' は出現する自由変数から x を全て u に置き換えたもの.
-- 結合
++ :: [a] -> [a] -> [a]
[x, ...] ++ [y, ...] = [x, ..., y, ...]
-- 畳み込み
fold :: (a -> a -> a) a -> [a] -> a
fold _ e [] = e
fold _ e [x] = x
fold * e [x, y...] = x * y * ...関数 h が準同型であるとは、次のような形で定められること.
h = fold (*) e (map g)
where
(*) :: b -> b -> b
e :: b
g :: a -> bリスト (L) をモナド (M) で包んで出来る ML を考える.
ML a == M [a]次の * は直積のある種の一般化である.
(*) :: ML a -> ML a -> ML a
a * b = [ x ++ y | x <- a, y <- b ]unit [] が (*) の単位元となっている. というわけで 集合 A (型 a の値全体) に対して (ML(A), *) はモノイドである.
(unit a) * (unit b) == unit (a ++ b)
h (a ++ b) == h a ++ h b -- h is homomorphism
join (f a) * join (f b) == join (f (a * b))(*) による畳込みprod :: [M [a]] -> M [a]
prod = fold (*) e
where
e = unit []prod . unit == id
prod . map unit == unit . join
prod . map (map (map f)) == map (map f) . prod
prod . map (join . map prod) == join . map prod . prod
prod . map prod == prod . joinML はモナドである. すなわち次の3つの関数が定義できる.
右上の添字はどのモナドに関するそれらであるかを示す. ただし \(L\) はリストモナドのこと.
直積 (Cartesian product) 相当の
を定める. これを用いると
\[\begin{align*} cp \cdot \text{unit}^L & = \text{map}^M \text{unit}^L & :: a \to [M a] \\ cp \cdot \text{map}^L \text{unit}^M & = \text{unit}^M & :: a \to M a \\ cp \cdot \text{map}^L (\text{map}^M f) & = \text{map}^M (\text{map}^L f) \cdot cp \\ cp \cdot \text{map}^L \text{join}^M & = \text{join}^M \cdot \text{map}^M cp \cdot cp \\ cp \cdot \text{join}^L & = \text{map}^M \text{join}^L \cdot cp \cdot \text{map}^L cp \\ \end{align*}\]
特にこの3つめは \(cp\) が \(map^L \circ map^M\) から \(map^M \circ map^L\) への自然変換であることを言っている.