ushumpei’s blog

生活で気になったことを随時調べて書いていきます。

モナドは自己関手の圏 (で自然変換を射、関手の合成を演算と見た場合) におけるモノイド対象

概要

自然変換の垂直合成、関手との合成がわかった結果

モナドは自己関手の圏 (で自然変換を射、関手の合成を演算と見た場合) におけるモノイド対象

だと言葉の意味を理解した。「自己関手の圏って言ったら射、演算は決まりきっているだろう」と言われたらそれまでだけど、知らなかったので。

まとめ

 Cモナドは関手  T: C \rightarrow C、自然変換  \eta : 1_C \Rightarrow T \mu : TT \Rightarrow T で次を満たすもの:

  •  \mu \circ T\mu = \mu \circ \mu T
  •  \mu \circ T \eta = \mu \circ \eta T

これを自己関手の圏 (自己関手を対象、自然変換を射、関手の合成を演算) と見た場合以下の図が可換なので、モナドは自己関手の圏におけるモノイド対象

モノイド対象 - Wikipedia

補足

自然変換の演算

http://alg-d.com/math/kan_extension/nat.pdf

そもそも自然変換の演算の種類を知らないとモナドの定義が読めない、上のサイトがとてもわかりやすかった。対象や射をある程度忘れて図を見ていくと、自分は議論を進められる程度にはわかった。必要な合成の種類は、垂直合成と関手との合成の 2 つ。

垂直合成

  • 圏:  C,  D
  • 関手:  F, G, H: C \rightarrow D
  • 自然変換:  \theta: F \Rightarrow G,  \sigma: G \Rightarrow H

とする、この時  \sigma \circ \theta: F \Rightarrow H a \in C に対し  ( \sigma \circ \theta )_a := \sigma_a \circ \theta_a と定義すれば、これは自然変換になる。

この合成は割と自然な感覚で理解できた。

関手との合成

  • 圏:  B,  C,  D,  E
  • 関手:  F, G: C \rightarrow D
  • 自然変換:  \theta: F \Rightarrow G

関手  H: D \rightarrow E が与えられた時、 H\theta: HF \Rightarrow HG a \in C に対し  (H\theta)_a := H(\theta_a) と定義すれば、これは自然変換になる (自然変換の型に出てくる  HF,  HG は関手の合成)

関手  H': B \rightarrow C が与えられた時、 \theta H': FH' \Rightarrow GH' a \in C に対し  (\theta H')_a := \theta_{H'(a)} と定義すれば、これは自然変換になる。

自然変換は関手によって "延長" できる。他に水平合成というものもあるが、一旦おいておく。

モナドの定義を眺める

モナドの定義は wiki から モナド (圏論) - Wikipedia

圏:  C 上のモナドは 関手:  T: C \rightarrow C と 2 つの自然変換  \eta : 1_C \Rightarrow T ( 1_C C 上の恒等関手) と  \mu : TT \Rightarrow T ( TT T を自分自身に合成した関手) で次を満たすもの:

  •  \mu \circ T\mu = \mu \circ \mu T
  •  \mu \circ T \eta = \mu \circ \eta T

ここで合成された自然変換の型を見てみる、まずは各関手による合成の型を括弧を省略せずにかく

  •  T \mu: T(TT) \Rightarrow TT
  •  \mu T: (TT)T \Rightarrow TT
  •  T \eta: TI \Rightarrow TT
  •  \eta T: IT \Rightarrow TT

 \mu \circ hoge は垂直合成で、結局以下になる

  •  \mu \circ T \mu: T(TT) \Rightarrow T
  •  \mu \circ \mu T: (TT)T \Rightarrow T
  •  \mu \circ T \eta: TI \Rightarrow T
  •  \mu \circ \eta T: IT \Rightarrow T

注意として、関手の合成は結合的なのと恒等関手の性質から、 \mu \circ T\mu = \mu \circ \mu T \mu \circ T \eta = \mu \circ \eta T はちゃんと意味がある (括弧を書いておくと後々わかりやすいので書いている)

この型を元に、自己関手の圏で眺めてみるとブログ冒頭のまとめの図式が得られる。

感想

  • 圏、関手、自然変換の定義はここ: 圏, 関手, 自然変換 - ushumpei’s blog
  • 自然変換が具体的になんなのかわかってなかったのだけど、結合法則とか恒等関手の性質も自然変換ってことだろうか
  • で何がわかったの?という気持ちにはなる
    • モノイド対象だから (>>=) :: IO a -> (a -> IO b) -> IO b みたいな二重の IO になりそうな部分で一つの IO にできる?
  • Haskell でいうと  \eta return か?
    •  \mu TT \rightarrow T なので >>= : : m a -> (a -> m b) -> m bm a -> m m b とした後 m m bm b にするのに使えそう、flatten みたいなものか?
  • 圏論を自然変換までやらなかったのかなり勿体無かったという気持ちになった
  • 垂直合成だと言い切ってしまったが今回の状況だと垂直合成と水平合成は一致する?