リストがモナドであることを確かめてみた。

きっかけは、モナドの定義とか - 檜山正幸のキマイラ飼育記 (はてなBlog)あたりが分かったような分からないようなもやもやした気分になったから。
わからないのは一方的にこっちの勉強が足りないからなので、考えてみることにした。
とりあえず、リストは本当にモナドか？というところをやってみた。

まず、手持ちの圏論の本のモナドの定義を眺めてみたが、エントリにあったKleisli tripleと結びつかなかった。
ということで、リストが(圏論の本の定義の)モナドかどうか自分で確かめることにした。

リストはモナド

結論だけ。
リストの圏 $D$ は以下のように決めればよい。イメージしやすさのため、Double(実数)のリストとする。

対象: $D_0, D_1, D_2, \ldots$

ここで, $D_0 :=$ Double(実数の集合), $D_1 := D_0$ のリストの集合, $D_2 := D_1$ のリストの集合(==実数のリストのリストの集合), $\ldots D_n := D_{n-1}$ のリストの集合, $\ldots$ *1

射:以下のようなもの。例で説明する。値の表現はyaml風。

flatten(concat, join)系

flatten :: D3 -> D2, [[[1,2,3],[4,5]],[[6,7]]] -> [[1,2,3],[4,5],[6,7]]

1 2 3 4                      1   2 3  [<=入れ子の深さ]
-                            -
  -                             
    -                            -
      - 1                          - 1
      - 2                          - 2
      - 3  flatten(concat)         - 3
    -     =================>     -
      - 4                          - 4
      - 5                          - 5
  -                             
    -                            -
      - 6                          - 6
      - 7                          - 7

要するに、第2列の「-」を縦に消していくのがflatten。
また、第3列を消すのはmap.flattenと書ける。第4列があれば、map.map.flatten。
以上のようにして、各Diについて定義できるだけの(map^n).flattenを定義しておく。

singleton(return)系

singleton :: D3 -> D4, [[[1,2,3],[4,5]],[[6,7]]] -> [[[[1,2,3],[4,5]],[[6,7]]]]

1 2 3 4                      1 2 3 4 5  [<=ネストの深さ]
                             -
-                              -        
  -                              -      
    -                              -    
      - 1                            - 1
      - 2                            - 2
      - 3  singleton(return)         - 3
    -     ===================>     -    
      - 4                            - 4
      - 5                            - 5
  -                              -      
    -                              -    
      - 6                            - 6
      - 7                            - 7

要するに、第1列のさらに左に「-」を入れるのがsingleton。
第1列と第2列の間に-を入れるのはmap.singletonと書ける。

map.singleton :: D3 -> D4, [[[1,2,3],[4,5]],[[6,7]]] -> [[[[1,2,3],[4,5]]],[[[6,7]]]]

1 2 3 4                        123 4 5  [<=ネストの深さ]

-                              -
 (ここ)                         -
  -                              -      
    -                              -    
      - 1                            - 1
      - 2                            - 2
      - 3  singleton(return)         - 3
    -     ===================>     -    
      - 4                            - 4
      - 5                            - 5
 (ここ)                         -
  -                              -      
    -                              -    
      - 6                            - 6
      - 7                            - 7

同様に、2列と3列の間に入れるのはmap.map.singleton,...とつづく。
以上のようにして、各Diについて定義できるだけの(map^n).singletonを定義しておく。

圏の射は、上のようにして作ったflatten系の関数と、singleton系の関数(と、恒等写像)とする。

これで、圏の設定ができた。

モナドであること

このリストの圏にはモナド構造を入れることができる。
モナドは自己関手 $T$ 、自然変換 $\eta$ 、自然変換 $\mu$ の組[tex:]で、ある性質を満たすもの。
$T$ は自己関手なので、 $T:D \to D$ 。
自然変換 $\eta$ は、 $\eta:I \to T$ ( $I$ は恒等関手)。
自然変換 $\mu$ は、 $\mu:T^2 \to T$ 。
満たすべき性質は、図式を使うので省略。http://www.ipsj.or.jp/07editj/promenade/4703.pdfの定義5を参照。
リストの圏に対しては、 $T$ をHaskellのmapとすればよい。
$\eta,\mu$ は自然変換なので、対象から射への写像となり、それぞれ、
$\eta(D_n)$ = $\mbox{singleton} :: D_n \to D_{n+1}$
$\mu(D_n)$ = $\mbox{flatten} :: D_{n+2} \to D_{n+1}$
とすればよい。これでモナドの定義を満たしている。
確認はめんどくさいだけで、コツコツやれば比較的簡単にできる。
これで、リストの圏で $<\mbox{map},\eta,\mu>$ がモナドになっていることがわかった。

めでたい。
と思ったが、やっぱりHaskellのモナド則には見えてこない。
色々探して、Haskellのモナド則に対応する圏論の概念は、Kleisli tripleというものらしい。
http://www.ipsj.or.jp/07editj/promenade/4703.pdfなどによると、Kleisli tripleからモナドを構成することができるらしい。
Listがモナドだと分かったから、モナド→Kleisli tripleの構成ができればいいはずだけど、モナドからKleisli tripleの構成がわからなかった。
ので、やってみる。

モナド→Kleisli triple

話を一般化して、Listに限らないモナドからKleisli tripleを構成する。

圏を $D$ 、モナドを[tex:]とする。

モナドからでる可換性

準備として、モナドからでる可換性をまとめておく。(a)、(b)は自然変換から、(c)、(d)はモナドから出る可換性。
$\phi:A\to B\quad(A,B\in D)$ とする。

(a) $(T\phi)\cdot\mu_A = \mu_B\cdot(T^2\phi)$

(b) $(T\phi)\cdot\eta_A = \eta_B\cdot\phi$

(d) $\mu_A\cdot\eta_{TA} = \mu_A\cdot(T\eta_A) = \mbox{id}_{TA}$

Kleisli tripleの定義

http://www.ipsj.or.jp/07editj/promenade/4703.pdfから引用。文脈に合わせてちょっと改変。

圏 $D$ 上の関手 $T:D\to D$ , 自然変換 $\eta:I\to D$ , 射 $\phi:X\to TY$ に対し、 $\phi^\ast : TX\to TY$ が以下の性質を満たすとき、[tex:]をKlisli triple という。

$\eta^\ast_X = \mbox{id}_{TX}$

$\phi^\ast\cdot\eta_X = \phi$

$\psi^\ast\cdot\phi^\ast = (\psi^\ast\cdot\phi)^\ast$ 　 $(\phi:X\to TY,\quad\phi:Y\to TZ)$

モナドからKleisli tripleを構成する

Kleisli triple[tex:] はモナド[tex:]から、

$T,\quad\eta$ はそのまま
$\ast:\phi \vdash\to \mu_Y\cdot(T\phi), \quad \phi:X \to TY, \quad (X,Y\in D)$

とすればよい。

(1) $\eta^\ast_X = \mbox{id}_{TX}$ ?

$\eta^\ast_X = \mu_X\cdot(T\eta_X)$ 　(定義)
　　　 $= \mbox{id}_{TX}$ 　　　　　　　(d)
OK!

(2) $\phi^\ast\cdot\eta_X = \phi$ ?

$\phi^\ast\cdot\eta_X = \mu_Y\cdot\underline{(T\phi)\cdot\eta_X}$ 　　(定義)
　　　　　　 $= \underline{\mu_Y\cdot\eta_{TY}}\cdot\phi$ 　　　　　　　　(b)
　　　　　　 $= \mbox{id}_{TY}\cdot\phi$ 　　　　　　　　　　　(d)
　　　　　　 $= \phi$