リストのモナドは1つだけか？

# Yet Another List Monad ?

リストデータ型にのるモナド構造はいくつあるのでしょう。

「リストのモナドは
`return x = [x]`
`xs >>= f = concatMap f xs`
だけじゃないの。 他にあるの？」

と思った人も多いと思いますが実はそれだけじゃないんです。

# モナドである条件

まず、モナドである条件を確認しておきましょう。
今回はリストのことだけを考えるので型はリストに限定して書きます。

リストにのるモナド構造とはモナド則を満たす2つの多相関数

```haskell
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](http://qiita.com/1to100pen/items/3ac5864b648b1d7b81ae) にもう少し詳しく書いています）


標準のリストモナドでは

```
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?](https://stackoverflow.com/questions/32931549/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