リストデータ型にのるモナド構造の単位射は a -> [a] だけ (2)

前回の記事 [リストデータ型にのるモナド構造の単位射は a -> [a] だけ (1)](https://qiita.com/1to100pen/items/4c0909d07174203c1f8b) の続きです。

本記事内で出てくる「性質2」「性質3」は前回の記事を参照してください。

# 複製ユニットモナドの性質(4) (r,n,...n)のn個形の join

前回の性質2と3のときは n * n形と r * n 形と綺麗な形の join を考察しましたが今度は (r,n,...n)のn個形というちょっとややっこしい形の join を考察します。
また 3複製ユニットモナドの具体的な例で考えましょう。

```
xs1 = [[1,1,1], [], []] -- (3,0,0)形
xs2 = [[0,0,0], [2,2,2], [0,0,0]] -- 3 * 3形
xs3 = [[0,0,0], [0,0,0], [3,3,3]] -- 3 * 3形

ys1 = join xs1 -- 長さ r 

zs = [xs1, xs2, xs3]
{- = [
  [[1,1,1], [],      []],
  [[0,0,0], [2,2,2], [0,0,0]],
  [[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]
   {- xs2 と xs3 については 3*3形なので性質2より対角線要素を集めて -}
  = join [ys1, [0,2,0], [0,0,3]]
```
つまり

```
join [ys1, [0,2,0], [0,0,3]] = [1,2,3]
```

右辺の
1番目の要素 `1` は左辺の ys1 の中から出てきて、
2番目の要素 `2` は左辺の `[0,2,0]` の 2番目の要素が出てきて、
3番目の要素 `3` は左辺の `[0,0,3]` の 3番目の要素が出てきて
いることがわかります。

また、右辺の 1番目の要素 `1` が左辺の ys1 の中から出てくるためには ys1 が空リストであっては無理なので ys1 は空リストではない、つまり ys1 の長さ r は 0 でないということもわかります。

例えば ys1 の長さr が 2 だったとしましょう。
(2,3,3)形の join は

```
join [
  [x11, x12],
  [x21, x22, x23],
  [x31, x32, x33]] = [x11かx12のどれか, x22, x33]
```
ということになります。

今は `n = 3` で考えましたが一般の n で

```
zs = [
  [[1,1..1], [],       [], ...,     []],
  [[0,0..0], [2,2..2], [0,0..0], ... [0,0..0]],
  [[0,0..0], [0,0..0], [3,3..3], ... [0,0..0]],
  ...
  [[0,0..0], [0,0..0], ... [0,0..0], [n,n..n]]]
```
に対して上で書いたのと同様の考察をすると

**性質4**

`r > 0` であり、

(r,n,...n) のn個形のリストの join は

```
join [
  [x11, x21, ... x1r],
  [x21, x22, x23, ... x2n],
  [x31, x32, x33, ... x3n],
  ...
  [xn1, xn2, xn3, ... xnn]] = [x11か...x1rのどれか, x22, x33, ... xnn]

{- 別の書き方だと -}
join xss = xss!0 の要素のうちのどれか : [xss!i!i | i <- [1..n-1]]
```

n も r も有限としての書き方をしていますが、n = ∞ や r = ∞ であったときでも成り立ちます。

# 複製ユニットモナドの性質(5) r = 1 と 1 * n形の join

さらにややっこしくなってきますがこのステップでゴールに一気に近づきます。

また3複製ユニットモナドの具体的な例で考察します。
今までどおり (3,0,0)形を join した結果のリストの長さを r で表します。
仮に`r = 2` だったとして話を進めます。

```
xs1 = map return [1,2] = [[1,1,1], [2,2,2]] -- n(=3) * r(=2)形
xs2 = [[0,0], [-2,-2], [0,0]] -- r(=2) * n(=3)形
xs3 = [[0,0], [0,0], [-3,-3]] -- r(=2) * n(=3)形

ys1 = join xs1 = join (map return [1,2])
  {- map return のモナド則より -}
  = [1,2]
ys2 = join xs2
  {- xs2 は r * n形なので性質3より最初の要素をとって -}
  = [0,0]
ys3 = join xs3
  {- xs3 は r * n形なので性質3より最初の要素をとって -}
  = [0,0]

zs = [xs1, xs2, xs3]
{- = [
  [[1,1,1], [2,2,2]],
  [[0,0], [-2,-2], [0,0]],
  [[0,0], [0,0], [-3,-3]]
-}
```
とします。

`xs1` の長さは r である 2、 `xs2` の長さは n である 3、 `xs3` の長さは n である 3 なので `zs` は (r,n,n) である (2,3,3)形をしていることを覚えておきましょう。性質4が使える形です。

`zs` での join のモナド則

```
join (join zs) = join (map join zs)
```
を観察しましょう。

```
左辺 = join (join zs)
  {- zs は (2,3,3)形なので性質4より -}
 = join [[1,1,1] か [2,2,2] のどれか, [-2,-2], [-3,-3]]

右辺 = join (map join zs)
  = join [join xs1, join xs2, join xs3]
  = join [ys1, ys2, ys3]
   {- ys1, ys2, ys3 は上ですでに具体的な値として求まっているので -}
  = join [[1,2], [0,0], [0,0]]
   {- 2 * 3形をしているので性質3より最初の要素を取って -}
  = [1,2]
```

つまり

```
join [[1,1,1] か [2,2,2] のどれか, [-2,-2], [-3,-3]] = [1,2]
```
ということになります。
「[1,1,1] か [2,2,2] のどれか」が `[1,1,1]` の方だったとして考察を進めましょう。つまり

```
join [[1,1,1], [-2,-2], [-3,-3]] = [1,2]
```
左辺には `2` が現れないのに右辺には `2` が現れています。こういうことは起こりえません。
今度は「[1,1,1] か [2,2,2] のどれか」が `[2,2,2]` の方だったとすると

```
join [[2,2,2], [-2,-2], [-3,-3]] = [1,2]
```
となり今度は左辺には `1` が現れないのに右辺には `1` が現れています。これも起こりえません。
最初に `r = 2` を仮定したうえでの矛盾ですから `r = 2` はありえないということになります。

一般の `r` について同様に join のモナド則を考察すると、

```
join [[1,1,1] か [2,2,2] か ... か [r,r,r] のどれか, [-2,...-2], [-3,...-3]] = [1,2,..r]
```
が導かれます。
`r > 1` のときは左辺に 1 から r までのすべて数が同時に現れることはできません。
また性質4から `r > 0` でしたから、左辺と右辺のつじつまが合う可能性があるのは残る `r = 1` のときだけです。このとき

```
join [[1,1,1], [-2], [-3]] = [1]
```
ですから、これなら左辺の3つの `1` のうちのどれかが右辺に現れたと考えれば盾は起きません。
つまり

**3複製ユニットモナドの join に (3,0,0)形を適用した結果のリストの長さは `1` しかありえない**

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

`n = 3` の例で考えましたが一般の n に対して

```
xs1 = map return [1,2...r] -- n * r形
xs2 = [[0,...0], [-2,...-2], [0,...0],   ... [0,...0]] -- r * n形
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]
```
として `zs` に対する join のモナド則を上と同じに考えると

**n複製ユニットモナドの join に (n,0,...0)のn個形を適用した結果のリストの長さは `1` しかありえない。**

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

`r = 1` ということがわかったのでこれを性質3に当てはめると

**性質5**

1 * n形の join は

```
join [[x1], [x2], ...  [xn]] = [x1]
```

ここまできたらゴールはもう少しです。

次の記事 [リストデータ型にのるモナド構造の単位射は a -> [a] だけ (3)](https://qiita.com/1to100pen/items/1c833aae652dd7bc262b) に続きます。

---

May Monad be with you