前回の記事 ZipListアプリカティブファンクタはモナドに拡張できるか (1) の続きです。
本記事内で出てくる「性質1」は前回の記事を参照してください。
前記事に続きこの記事でもリストについて ZipList の話しかしないので構築子の ZipList を書くのは省略します。
ZipListモナドの性質2 (The property of ZipList monad (Part 2))
as = [[], [1, 2]]
as' = [[], [3, 4]]
ws = [as, as'] {- [ [[], [1, 2]], [[], [3, 4]] ] -}
ys = join as
ys' = join as'
として ws の join について観察しましょう。
as と as' は要素の値は違いますが2重リストとしての形状は同じなので join されたときの作用も同じになります。（join 関数の多相性）
したがって ys と ys' のリスト長は等しくなります。このことは後で使います。
join のモナド則
join (join ws) = join (map join ws)
の左辺と右辺をそれぞれ計算します。
左辺 (left side)
= join (join [[], [1, 2]], [[], [3, 4]])
{- 行列の形をしているので対角線を集める -}
= join [[], [3, 4]]
= join as'
= ys'
右辺 (right side)
= join [join as, join as']
= join [ys, ys']
つまり
ys' = join [ys, ys']
前述したとおり ys と ys' のリスト長は等しいので [ys, ys'] は行列的な形になっています。
したがって性質1から右辺の join [ys, ys'] は [ys, ys'] の対角線を集めたリストになっています。
ys が空リストでなければ [ys, ys'] の対角線の最初の要素は ys の最初の要素である ys!!0 ですから、このときは左辺には ys がまったく現れていないのに右辺には ys!!0 が現れるという状況になっています。
直感的には ys の要素に現れる値と ys' の要素に現れる値はまったく別のものという気がしますが念のためもう少し確認しましょう。
ys = join as でしたから ys には as の中に登場した値しか現れません。
as = [[], [1, 2]] でしたから、ys には 1 か 2 しか現れないということになります。同様に ys' には 3 か 4 しか現れません。
改めて ys が空リストでなかったときの状況をみると、左辺である ys' には 3 か 4しか現れえないのに対し右辺には対角線の最初の要素 ys!!0 として 1 か 2 のどちらかが必ず現れるというおかしなことになっています。
こういうことはありえないので、ys は空リストでなければならないということになります。
as として [[], [1, 2]] の例で考えましたが要素が整数である必要もなかったし、as の第2要素のリストの長さが 2 である必然性もなかったので一般化して考えると
ZipListモナドの性質2 (The property of ZipList monad (Part 2))
任意のリスト xs に対して
join [[], xs] = []
ということがわかります。
ZipListモナドの性質3 (The property of ZipList monad (Part 3))
ゴールまでもうちょっと！
xss = [ [[1,2], [3,4]], [[], [5,6]] ] の join を観察しましょう。
join のモナド則
join (join xss) = join (map join xss)
の左辺と右辺をそれぞれ計算します。
左辺 (left side)
= join (join [ [[1,2], [3,4]], [[], [5,6]] ])
{- 行列の形をしているので対角線を集める -}
= join [[1,2], [5,6]]
{- 行列の形をしているので対角線を集める -}
= [1,6]
右辺 (right side)
= join [join [[1,2], [3,4]], join [[], [5,6]]]
{- 行列の形をしている方は対角線を集め、もう片方は性質2 で [] になることがわかる -}
= join [[1,4], []]
左辺には 6 が現れています。一方、具体的な形はわかっていないものの少なくとも右辺に 6 が現れないことはわかります。右辺の登場人物は 1 と 4 だけですから。
つまり
ZipListモナドの性質3 (The property of ZipList monad (Part 3))
性質1を満たす join は
[ [[1,2], [3,4]], [[], [5,6]] ] に対しては join のモナド則は成り立たない。
ということがわかりました。
性質1は ZipListモナドであるための必然でしたから、
結論 (Conclusion)
ZipListモナド、そんなものはなかった。 (There is no such thing as a ZipList monad)
リストデータ型にのるモナド構造についてさらに (More about monad instance for list data type)
今回は join [[f x y | y <- ys] | x <- xs] = zipWith f xs ys からスタートして結論を導き出しましたが実は return が return a = [a] ではないことからだけでも同じ結論を導くことができます。
興味ある方は リストデータ型にのるモナド構造の単位射は a -> [a] だけ (1) もご覧ください。
また、リストデータ型にのるモナド構造にはよく知られているリストモナド以外のものがあるかについて興味のある方は リストのモナドは1つだけか？ もご覧ください。
May Monad be with you