モナド
Monad
Applicative
ZipList
アプリカティブ

ZipListアプリカティブファンクタはモナドに拡張できるか (2)

前回の記事 ZipListアプリカティブファンクタはモナドに拡張できるか (1) の続きです。
本記事内で出てくる「性質1」「性質2」は前回の記事を参照してください。

前記事に続きこの記事でもリストについて ZipList の話しかしないので構築子の ZipList を書くのは省略します。

ZipListモナドの性質3

as  = [[], [1, 2]]
as' = [[], [3, 4]]

ws = [as, as']     {- [ [[], [1, 2]], [[], [3, 4]] ] -}

ys  = join as
ys' = join as'

として wsjoin について観察しましょう。

asas' は要素の値は違いますが2重リストとしての形状は同じなので join されたときの作用も同じになります。(join 関数の多相性)
したがって ysys' のリスト長は等しくなります。このことは後で使います。

join のモナド則 

join (join ws) = join (map join ws)

の左辺と右辺をそれぞれ計算します。

左辺 = join (join [[], [1, 2]], [[], [3, 4]])
       {- 行列の形をしているので対角線を集める -}
     = join [[], [3, 4]]
     = join as'
     = ys'
右辺 = join [join as, join as']
     = join [ys, ys']

つまり

ys' = join [ys, ys']

前述したとおり ysys' のリスト長は等しいので [ys, ys'] は行列的な形になっています。
したがって性質1から右辺の join [ys, ys'][ys, ys'] の対角線を集めたリストになっています。

ys が空リストでなければ [ys, ys'] の対角線の最初の要素は ys!!0 ですから、このときは左辺には ys がまったく現れていないのに右辺には ys!!0 が現れるという状況になっています。

直感的には ys の要素に現れる値と ys' の要素に現れる値はまったく別のものという気がしますが念のためもう少し確認しましょう。

ys = join as でしたから ys には as の中に登場した値しか現れません。
as = [[], [1, 2]] でしたから、ys には 12 しか現れないということになります。同様に ys' には 34 しか現れません。

改めて ys が空リストでなかったときの状況をみると、左辺である ys' には 34しか現れえないのに対し右辺には対角線の最初の要素 ys!!0 として 12 のどちらかが必ず現れるというおかしなことになっています。
こういうことはありえないので、ys は空リストでなければならないということになります。

as として [[], [1, 2]] の例で考えましたが要素が整数である必要もなかったし、as の第2要素のリストの長さが 2 である必然性もなかったので一般化して考えると

ZipListモナドの性質3

任意のリスト xs に対して

join [[], xs] = []

ということがわかります。

ZipListモナドの性質4

ゴールまでもうちょっと!

xss = [ [[1,2], [3,4]], [[], [5,6]] ]join を観察しましょう。

join のモナド則 

join (join xss) = join (map join xss)

の左辺と右辺をそれぞれ計算します。

左辺 = join (join [ [[1,2], [3,4]], [[], [5,6]] ])
       {- 行列の形をしているので対角線を集める -}
     = join [[1,2], [5,6]]
       {- 行列の形をしているので対角線を集める -}
     = [1,6]
右辺 = join [join [[1,2], [3,4]], join [[], [5,6]]]
       {- 行列の形をしている方は対角線を集め、もう片方は性質3 で [] になることがわかる -}
     = join [[1,4], []]

左辺には 6 が現れています。一方、具体的な形はわかっていないものの少なくとも右辺に 6 が現れないことはわかります。右辺の登場人物は 14 だけですから。

つまり

ZipListモナドの性質4

性質1を満たす join

[ [[1,2], [3,4]], [[], [5,6]] ] に対しては join のモナド則は成り立たない。

ということがわかりました。

性質1は ZipListモナドであるための必然でしたから、

結論

ZipListモナド、そんなものはなかった。

後記

記事を見直したら性質2をその後の証明で使っていませんでした。
でも性質2の見た目格が好いいので削除せずそのままにしておきます。

今回は join [[f x y | y <- ys] | x <- xs] = zipWith f xs ys からスタートして結論を導き出しましたが実は returnreturn a = [a] でないことからだけでも同じ結論を導くことができます。
興味ある方は リストデータ型にのるモナド構造の単位射は a -> [a] だけ (1) もご覧ください。
また、リストデータ型にのるモナド構造によく知られているリストモナド以外のものがあるかについて興味のある方は リストのモナドは1つだけか? もご覧ください。


May the Monad be with you