前々回の記事 リストデータ型にのるモナド構造の単位射は a -> [a] だけ (1) と
前回の記事 リストデータ型にのるモナド構造の単位射は a -> [a] だけ (2) の続きです。
本記事内で出てくる「性質2」「性質3」「性質4」「性質5」は前々回、前回の記事を参照してください。
今まで (n,0,...0)のn個形のリストとそれを join した結果のリストの長さ r を中心に考えてきましたが、
今度は (0,n,0,...0)のn個形のリストとそれを join した結果のリストの長さ（r' で表します）を中心に考えていきます。
(0,n,0,...0) のように少なくとも2番目に値があるケースを考えたいので少なくとも長さが 2以上でないとそのような形になりません。そのため今回は n > 1 を仮定します。
性質3、性質4、性質5と似たような結果の性質3'、性質4'、性質5'をこれから導いていきますが、その際「同様の考え方で」という表現を多用します。
本当に「同様の考え方で」うまくいくのか気になるでしょうから結論の後の付録で少し説明を補足します。余裕があればそちらも読んでチェックしてください。
では (0,n,0,...0)のn個形のリストを考察していきましょう。
性質3と同様の考え方で (0,n,0,...0)のn個形のリストをn個並べたリストの join のモナド則を考察することによって
性質3'
n > 1 のとき r' * n形の xss に対して
join [
[x11, x12, ... x1r'],
[x21, x22, ... x2r'],
...
[xn1, xn2, ... xnr']] = [x21, x22, ... x2r']
{- 別の書き方だと -}
join xss = xss!1
性質3とは違って最初のリストではなくて2番目のリストがそのまま出てくることに注意してください。
性質4と同様の考え方で
zs = [
[[1,1...1], [0,0...0], [0,0...0], [0,0...0], ... [0,0...0]],
[[], [2,2...2], [], [], ... []],
[[0,0...0], [0,0...0], [3,3...3], [0,0...0], ... [0,0...0]],
...
[[0,0...0], [0,0...0], [0,0...0], ... [0,0...0], [n,n...n]]]
の join のモナド則を考察することにより
性質4'
r' > 0 であり、
n > 1 のとき (n,r',n,...n) のn個形のリストの join は
join [
[x11, x12, x13, ... x1n],
[x21, x22, ... x2r'],
[x31, x32, x33, ... x3n],
...
[xn1, xn2, xn3, ... xnn]] = [x11, x21か...x2r'のどれか, x33, ... xnn]
{- 別の書き方だと -}
join xss = xss!0!0: xss!1 の要素のうちのどれか : [xss!i!i | i <- [2..n-1]]
性質4とは違って (r,n,...n)形ではなくて (n,r',n,...n)形のリストに対してであること、
join結果は最初の要素ではなく2番目の要素に特徴があることに注意してください。
性質5と同様の考え方で
xs1 = [[-1,...-1], [0,...0], [0,...0], ... [0,...0]] -- r * n形
xs2 = map return [1,2...r] -- n * r形
xs3 = [[0,...0], [0,...0], [-3,...-3], ... [0,...0]] -- r * n形
...
xsn = [[0,...0], [0,...0], [0,...0], ... [-n,...-n]] -- r * n形
zs = [xs1, xs2, xs3,... xsn]
の join のモナド則を考察することにより
性質5'
n > 1 のとき
r' = 1 であり、
1 * n形の join は
join [[x1], [x2], ... [xn]] = [x2]
性質5とは違って最初の要素ではなくて2番目の要素が出てくることに注意してください。
結論
n > 1 のとき 1 * n形のリスト [[1], [2], ... [n]] に性質5と性質5'を当てはめると
性質5から
join [[1], [2], ... [n]] = [1]
性質5'から
join [[1], [2], ... [n]] = [2]
これは矛盾。
つまり、
n > 1 の n複製ユニットモナドは存在しない。
ゴールしました。お疲れ様でした。
この結論の応用として
ZipListアプリカティブがモナドに拡張できない
ことを示すことができます。
なぜなら、もし ZipListアプリカティブがモナドに拡張できたとしたらそのモナドの単位射は
return x = pure x = repeat x
つまり ∞複製ユニットということになりますから上記の結論よりそのようなモナドは存在しないということが導かれます。
ただし「ZipListアプリカティブはモナドに拡張できない」ことだけに限ればもっと短く証明（ZipListアプリカティブファンクタはモナドに拡張できるか）することができます。
以下、性質3'、性質4'、性質5'の補足説明です。
付録
性質3'、性質4'、性質5'の説明を n = 3 のときの具体例で補足します。
性質3'の補足説明
{- (0,3,0)形の3つのリスト -}
xs1 = [[], [1,2,3], []]
xs2 = [[], [4,5,6], []]
xs3 = [[], [7,8,9], []]
ys1 = join xs1
ys2 = join xs2
ys3 = join xs3
zs = [xs1, xs2, xs3]
{- = [
[[], [1,2,3], []]
[[], [4,5,6], []]
[[], [7,8,9], []]
-}
として zs での join のモナド則
join (join zs) = join (map join zs)
を観察しましょう。
左辺 = join (join zs)
{- zs は 3*3形なので性質2より対角線要素を集めて -}
= join [[], [4,5,6], []]
= join xs2
= ys2
右辺 = join (map join zs)
= join [join xs1, join xs2, join xs3]
= join [ys1, ys2, ys3]
つまり
join [ys1, ys2, ys3] = ys2
ここまで確認すれば後の説明はもういいですよね。
性質4'の補足説明
xs1 = [[1,1,1], [0,0,0], [0,0,0]] -- 3 * 3形
xs2 = [[], [2,2,2], []] -- (0,3,0)形
xs3 = [[0,0,0], [0,0,0], [3,3,3]] -- 3 * 3形
ys2 = join xs2 {- 長さ r' -}
zs = [xs1, xs2, xs3]
{- = [
[[1,1,1], [0,0,0], [0,0,0]],
[[], [2,2,2], []],
[[0,0,0], [0,0,0], [3,3,3]]]
-}
として zs での join のモナド則
join (join zs) = join (map join zs)
を観察しましょう。
左辺 = join (join zs)
{- zs は 3 * 3形なので性質2より対角線要素を集めて -}
= join [[1,1,1], [2,2,2], [3,3,3]]
{- 3 * 3形なので性質2より対角線要素を集めて -}
= [1,2,3]
右辺 = join (map join zs)
= join [join xs1, join xs2, join xs3]
{- xs1 と xs3 については 3 * 3形なので性質2より対角線要素を集めて -}
= join [[1,0,0], ys2, [0,0,3]]
つまり
join [[1,0,0], ys2, [0,0,3]] = [1,2,3]
ここまで確認すれば後の説明はもういいですよね。
性質5'の補足説明
仮にr' = 2 だったとして話を進めます。
xs1 = [[-1,-1], [0,0], [0,0]] -- r' * n形
xs2 = map return [1,2] = [[1,1,1], [2,2,2]] -- n * r'形
xs3 = [[0,0], [0,0], [-3,-3]] -- r' * n形
ys1 = join xs1
{- xs1 は r' * n形なので性質3'より2番目の要素を取って -}
= [0,0]
ys2 = join xs2 = join (map return [1,2])
{- map return のモナド則より -}
= [1,2]
ys3 = join xs3
{- xs3 は r' * n形なので性質3'より2番目の要素を取って -}
= [0,0]
zs = [xs1, xs2, xs3]
{- = [
[[-1,-1], [0,0], [0,0]],
[[1,1,1], [2,2,2]],
[[0,0], [0,0], [-3,-3]]
-}
とします。
xs1 の長さは n である 3、 xs2 の長さは r' である 2、 xs3 の長さは n である 3 なので zs は (n,r,n) である (3,2,3)形をしていることを覚えておきましょう。性質4'が使える形です。
zs での join のモナド則
join (join zs) = join (map join zs)
を観察しましょう。
左辺 = join (join zs)
{- zs は (3,2,3)形なので性質4'より -}
= join [[-1,-1], [1,1,1] か [2,2,2] のどれか, [-3,-3]]
右辺 = join (map join zs)
= join [join xs1, join xs2, join xs3]
= join [ys1, ys2, ys3]
{- ys1, ys2, ys3 は上ですでに具体的な値として求まっているので -}
= join [[0,0], [1,2], [0,0]]
{- 2 * 3形をしているので性質3'より2番目の要素を取って -}
= [1,2]
つまり
join [[-1,-1], [1,1,1] か [2,2,2] のどれか, [-3,-3]] = [1,2]
ここまで確認すれば後の説明はもういいですよね。
以上で補足説明も終わり！
May Monad be with you