Yet Another List Monad ?
リストデータ型にのるモナド構造はいくつあるのでしょう。
「リストのモナドは
return x = [x]
xs >>= f = concatMap f xs
だけじゃないの。 他にあるの？」
と思った人も多いと思いますが実はそれだけじゃないんです。
モナドである条件
まず、モナドである条件を確認しておきましょう。
今回はリストのことだけを考えるので型はリストに限定して書きます。
リストにのるモナド構造とはモナド則を満たす2つの多相関数
return :: a -> [a]
(>>=) :: [a] -> (a -> [b]) -> [b]
-- モナド則
(return x) >>= f == f x
m >>= return == m
(m >>= f) >>= g == m >>= (\x -> f x >>= g)
return と (>>=) のことです。
join を使ったモナド則
ただしこの形のままだと扱いにくいので join xss = xss >>= id で定義される多相関数 join を導入して（fmap も使って）上記を同値な定義に書き換えると
リストにのるモナド構造とはモナド則を満たす2つの多相関数
return :: a -> [a]
join :: [[a]] -> [a]
-- モナド則
join (return xs) = xs
join (fmap return xs) = xs
join (join xss) = join (fmap join xss)
-- ポイントフリー形式で書くと
join . return = id
join . fmap return = id
join . join = join . fmap join
return と join のことです。
（ここら辺のことは join と (>>=) と、時々、fmap にもう少し詳しく書いています）
標準のリストモナドでは
return x = [x]
join xss = concat xss
{- 例えば join [[1], [2,3]] = [1,2,3] となる -}
となっています。
return と join を定義する
では、別のモナド構造の return と join を探していきましょう。
まず return ですが型が a -> [a] なので
return x = []
return x = [x]
return x = [x,x]
return x = [x,x,x]
...
return x = repeat x {- 要素が x の無限リスト -}
のうちのどれかしかありませんが今回は return x = [x] のケースについてだけ考えましょう。（標準のリストモナドの return と同じですね）
実は return x = [x] 以外はモナド構造としてはありえない（と思っている）のですが、その話はまたいつか。
モナド則のはじめの2つに出てくる return xs と fmap return xs がどんな形のリストになるか具体的に xs = [1,2,3] のケースで見てみましょう。
return [1,2,3] = [ [1,2,3] ]
fmap return [1,2,3] = [ [1], [2], [3] ]
長さが1であるリストと、すべての要素（これもリスト）が長さ1のリストであることがわかります。
これは xs = [1,2,3] だけでなく一般のリストでも成り立つことは明らかでしょう。
この条件でモナド則のはじめの2つを書き直すと
join xss
| single xss = concat xss -- return xs に対応するケース
| all single xss = concat xss -- fmap return xs に対応するケース
-- リストの長さが1かどうか
single [_] = True
single _ = False
となります。
この2つの条件にマッチしないときはどうしましょう。
標準のリストモナドではすべて concat していますが、ここでは一気にすべて空リストにしてみましょう。
join xss
| single xss || all single xss = concat xss
| otherwise = []
{- 例えば join [[1], [2,3]] = [] となる -}
QuickCheck でモナド則を検証
さて、join の定義はしたもののこの定義でモナド則の最後の条件
join (join xss) = join (fmap join xss)
を満たすでしょうか。
私の脳内ではこの条件を満たすことを証明できたつもりですが大ポカしているのではないかと不安です。
Coq や Agda などの定理証明器を使えばしっかりとした証明で確認することができるのでしょうが残念ながらマスターできていません。
そこで QuickCheck で確認することにしました。もちろん QuickCheck で全ケースを網羅することはできないので証明にはなりませんが多分大丈夫そうだという安心感は得られます。
リストの場合、形状、つまりリストの長さがまず大事になってきます。要素を比較する以前にリスト長が違えば異なることは明らかですからね。 そこで要素の型に値が一つしかない () 型の場合でまず確認してみましょう。 QuickCheck のデフォルトのテストケースは 100個ですが、それだけでは不安なので 1000000個でやってみます。
QuickCheckライブラリはすでにインストール済みとします。
$ stack ghci
Prelude> :{
Prelude| single [_] = True
Prelude| single _ = False
Prelude|
Prelude| join xss
Prelude| | single xss || all single xss = concat xss
Prelude| | otherwise = []
Prelude| :}
Prelude> import Test.QuickCheck
Prelude Test.QuickCheck> -- テストケースの個数を指定できるようにする。quickCheckWith を使う。
Prelude Test.QuickCheck> quickCheckN n = quickCheckWith stdArgs { maxSuccess = n }
Prelude Test.QuickCheck> -- join のモナド則を確認する prop。ルールではないが慣例として関数名に prop_ を付けるらしい。
Prelude Test.QuickCheck> prop_join xss = join (join xss) == join (fmap join xss)
Prelude Test.QuickCheck> quickCheckN 1000000 (prop_join :: [[[()]]] -> Bool)
+++ OK, passed 1000000 tests.
うまくいきました。形状の確認だけだとさすがに不安なので Int 型でもやってみましょう。
Prelude Test.QuickCheck> quickCheckN 1000000 (prop_join :: [[[Int]]] -> Bool)
+++ OK, passed 1000000 tests.
うまくいきました。今のところこの join のモナド則の反例は出てきていません。
この join の定義の残念なところは all single で全要素を走査してからでないと場合分けできないところで、特に無限リストに対しては有限時間で判定することができません。
さらにもう1つのリストモナド
他にもリストの別のモナド構造がないかと検索していたら見つかりました。
To what extent are Applicative/Monad instances uniquely determined? の Answer で見つけた
リストの要素に一つでも空リストのものがあれば join の結果は空リストにし、それ以外の場合は concat する、というものです。
return x = [x]
join xss
| any null xss = []
| otherwise = concat xss
{- 例えば join [[1], [], [2,3]] = [] となる -}
こちらの定義でも QuickCheck で join のモナド則の反例は出てきませんでした。
この join の定義も any null で全要素を走査してからでないと場合分けできません。
リストのモナドは3つだけか？
リストのモナド構造は標準のものを含めて少なくとも3つはあることが（ちゃんと証明を書いたわけではないけれど）わかりました。
他にもあるのでしょうか。
もし見つけたら、またはないことが証明されていたら是非教えてください。
May Monad be with you