元祖圏論勉強会ではない方の圏論勉強会 第13回の最終回です。資料とustreamは公開されています。
- ワークスアプリケーションズさんに感謝
- 三脚復活してる！
第13回: 随伴・モナド / 講師 @9_ties さん
- 「モナドが途中で終わるのは嫌でしょう」「随伴を説明しないわけにはいかない」
- 随伴のHom集合による定義
- unitによる定義
- あるη:1→GFが、任意のf:X→GYについてf:FX→Yが唯一存在するとき(満たすべき可換図式は略)
- counitによる定義は双対なもの
- 例: Δ(X)=(X, X)の右随伴をcounit definitionで調べる
- counitの成分はC×Cの射なので、(π1,π2)として可換図を書き下す
- 積の可換図式が現れる。Δ|-×
- 同様に＋|-Δ
- Q. ＋と×が双対なのはたまたま？
- A. 一般には違う。Δの双対がΔなのでこうなる
- Q. |-はいつまでもチェーンになる？
- A. 随伴は存在しないこともある。無限に随伴が続くことがあるのかはわからないので各自調べて
- Q. テキストは向きが逆だけど？
- A. テキストは-|らしいので、読み替えて
- 例: 一般の対角関手: ΔJ:C→C^JはΔ_J(X)(A) = X、ΔJ(X)(f) = id_Xで定義
- colim J |- ΔJ |- lim Jとなる
- 例: (-)×A|-(-)^Aをcounit definitionで考えてみる → counitがevaluation mapとなる
- 例: 自由モノイドをunit definitionで考えてみる → 忘却関手の左随伴Fが存在するための条件となる
- counit definitionで考えてみる → counitがfold。foldMap f = fold . map fが出てくる
- Fの右随伴、左随伴は、同型を除いて一意
- 米田の補題で証明できる
- 随伴を用いて定義するとwell definedになることを意味する
- F|-Gの時、Fは余連続(colimを保存)、Gは連続
- 米田の補題より
- 右随伴はlimを保存するので、1^A =~ 1、(B×C)^A =~ B^A×C^A
- 左随伴はcolimを保存するので、0×A =~ 0、(B+C)×A =~ B×A+C×A 分配則
- Q. 随伴のイメージとは？
- モナドはもともと圏論の概念。それが計算機に応用されたもの
- 自己関手Tとη:1→T、μ:TT→Tで、モナド則を満たすもの
- 例: リストモナド
- Setsにおいて、T(A)をAの要素の列の集合、TfはTAの要素全てにfを適用する関数
- モナド則をghciで実際に確認してみる
- モナドの圏論的な文脈
- 随伴F|-Gについて、GFとunit、G(ε_F)、の3つ組はモナド
- 証明については「GFGFGFとかでてきて読むのが嫌になりますね」
- リストモナドは、自由モノイドFと忘却関手Uとすると、UF
- G(ε_F)を考えると、concatを忘却したものになる
- (-)×S |- (-)^Sからはstateモナドが出てくる。stateモナドはカリー化と関連している
- モナドから随伴を作れる。ただし、モナドと随伴は1対1ではない
- Eilenberg-Moore圏。T代数の圏
- 随伴の場合は圏Dが必要。このとり方に自由度がある
- モノイド対象
- モノイドをSetsにおける圏の言葉で定義できる
- 前提条件「直積があること、結合的であること、1×MとMが同型であること」
- モノイダル圏
- 関手(*)があり、(X(*)Y)(*)Z =~ X(*)(Y(*)Z)、I(*)X =~ X =~ X(*)I
- コヒーレンス条件も必要(ほとんどの場合成り立つらしい)
- Setsでモノイド対象を考えると、モノイドが出てくる
- 自己関手の圏でモノイド対象を考えると、モナド。
- 自己関手の圏 → 対象は自己関手C→C。射を自然変換。
- モナドはモノイドと思ってよい
- 理論計算機分野でのモナド
- 表示的意味論の分野で、Moggiによる提案が始まり
- Computational effect
- 計算とは、「インプットがあってアウトプットがあるもの」。関数として表現しようとする
- computational effect。計算作用
- 例: 値を返さない、複数の計算結果、副作用、エラー、継続
- 計算作用を自己関手Tで表す。A→T B。Kleisli arrowと呼ぶ
- 表し方
- 値を返さない → TB = B + 1
- 複数の計算結果 → TB = P(B)
- 副作用 → TB = (S×B)^S。A×S→B×Sをカリー化したと思えばよい
- 例外 → TB = B + E
- 継続 → TB=(R^R)^B
- 計算は合成できる A→TB、B→TCを合成するとA→TB→TTC
- 計算作用が二度起こると考えればよいが、計算作用の種類が違ってよくない
- μ:TT→Tでたたみ込める
- 計算作用の畳み込みは結合的 → TTTの畳込みは結合的になるだろう
- 何もしない計算があった方がよい。η:1→T
- 何もしない作用は単位的になるはず。ηは単位元になるだろう
- Haskellでは、ηはreturn、μはjoin
- return 1の[Int]、Maybe Int、IO Int、State () Intなどの例
- joinの例
- モナドのありがたさ
- 数学的な表示により、計算機作用の数学的な解析が可能になる
- プログラムの検証、最適化などに使える
- カリーハワード対応により、理論計算機分野以外への貢献も
- haskellにおけるdo記法。並べられた文の合成法を与えている
- プログラムの設計にも(いいか悪いかはともかく)影響を与えているだろう
- Q. 学校でモナドが出てこないのなんで？
- Q. 数学からもっといい抽象化が？
- A. ありうる。モナドより広いArrow、狭いApplicative、など
- Q. 違う種類のTとT'を合成することができるのか
- A. 同じ種類のものしか合成できない。モナド変換子がそのようなもの。TとT'を合成した一つの関手T''を作る
- Q. 層圏トポスに圏論だとスッキリって書いてあったけど本当？
- A. 集合論で証明するのは難しいって話か、もしくはトポスの話？？圧倒的に楽になる理論があるのは確か。すべてがやさしくなるわけではない
- この回は入門なので、本を読み、練習問題をやってほしい。理論計算機分野の論文も読むと良い
お疲れ様でした。それにしても、東京で13回かけて話された内容を去年名古屋で2時間で話したのだから、名古屋の怖さがよくわかりますね！
まだ物足りない方は、コンセプタンや元祖圏論勉強会に出席されるとよいでしょう。
最後になりますが、講師を勤めてくださった@9_ties さん、どうもありがとうございました。大変勉強になりました。
