モナドの「変な結合」について(続き)
檜山さんからコメントをもらいました。
- 「変な結合」
- モナド一個分のズレという表現
にはツッコミが入らなかったので、そんなに間違ってはなかったんだろうと好意的に解釈しています。
コメントに関連して、昨日省略したところを補ってみます。
- モナド一個分のズレについて
return はそのまま
TA ↑ ｜return ｜ A
という図。
結合は、モナドになっている関手をTとして、A、B、C は型とすると
TA TB TC
┐ ┐
／ ／
f／ g／
／ ／
A B Cこのように書ける。このとき f と g は「変な結合」が可能。その結果は、型Aから型TCへの矢印になる。
BとTBのところでモナド T 一個分ずれているけれども、つながる。
どう見ても離れているが、ちゃんと本当につながないと意味がないので
T2C
┐｜
／ ｜
Tg／ ｜μC
／ ↓
TA TB TC
┐ ┐
／ ／
f／ g／
／ ／
A B C
のようにつなげる。g: B -> TC に 関手 T をかけて上に持ち上げて、モナドの定義にあるμ:T2 -> T を使ってTCに降ろす。f;Tg;μCで A -> TC の射ができる。
モナドの「変な結合」は、いちいちこの作業が入っている。
- Kleisli圏(自己流)
「変な結合」を普通の結合に、return を id にしたいので、次のように対象と射を作る。
(TA, A) (TB, B) (TC, C)
|______↑ |______↑
f' g'
(TX, X) という対を新しい対象として、ある対の第2要素からある対の第1要素への(元の圏での)射を新しい射とする。
図では、TB と B の間でつながってないように書いてあるが、さっきの持ち上げて降ろす作業が入っていると思うことにする*1。
return は、(TA, A) の形の対象の第2要素から自身の第1要素へ戻る射になる。線だけ外に引っ張り出せば、よくあるクルッと丸い線が書ける。モナドの公理(モナド則)のおかげで、return が新しい圏での id になっている(はず)。
こうして作った新しい圏をモナドの Kleisli圏という(らしい)。
という風な構成を考えたわけです。間違ってたらごめんなさい。
檜山さんのコメントやマックレーン本のやり方は、元の圏をじっとにらんでいると、心眼で新しい圏が見えてくるぞ、といったイメージで捉えています。具体的には、トレーシングペーパーで元の圏の対象だけまず写し取る。次に、元の圏での A -> TB の形の射を見つけたら、トレーシングペーパーの方の A と 「B」の間に射を書く。つなぎの持ち上げ降ろしは同様に処理。最終的にトレーシングペーパーに書かれたのが Kelisli圏。
どちらも多分同じだろうなあと思っています。
