黒木先生のモナドに関する話

あとでちゃんと読むためにまとめておく
1
黒木玄 Gen Kuroki @genkuroki

#数楽 リンクメモ追加 添付画像は sciencedirect.com/science/articl… より。partialityはMaybeで、exceptionはEither。 pic.twitter.com/aByMSJae0o

2017-02-04 14:58:48
拡大
黒木玄 Gen Kuroki @genkuroki

#数楽 リンクメモ 浜名誠 (2007) 関数型プログラマのためのモナド理論(1)(2)(3) takeichi.ipl-lab.org/~hamana/local/… 【主張:数学の方が簡単】 takeichi.ipl-lab.org/~hamana/local/… takeichi.ipl-lab.org/~hamana/local/…

2017-02-04 20:47:05
黒木玄 Gen Kuroki @genkuroki

#数楽 リンクメモ math.uchicago.edu/~may/REU2012/R… Sankarさんによるモナドに関する易しい解説(英語) 一つ前のリンク先の解説を読むために役に立つ。 私も「数学の方が簡単」だと思う。

2017-02-04 20:50:11
黒木玄 Gen Kuroki @genkuroki

#数楽 「数学の方が簡単」という話の続き。プログラミングの勉強のためにモナドについて勉強しようとした人であっても、もしかしたら、次のリンク先の本にその手の話が書いてあることはあまり知られていなかったりするんじゃないなかな? nippyo.co.jp/shop/book/6936…

2017-02-05 20:43:46
黒木玄 Gen Kuroki @genkuroki

#数楽 『圏論の歩き方』を最近自宅で見ていたら、「その表紙がかわいい本はなに?」と言われた。本の表紙は結構大事。

2017-02-05 20:46:22
黒木玄 Gen Kuroki @genkuroki

#数楽 リンクメモ nifty.works/about/AGjXDRbk… 【Beck's monadicity theorem gives a criterion that characterises monadic functors.】 リンク先がちょっと面白いので紹介

2017-02-05 21:56:23
黒木玄 Gen Kuroki @genkuroki

#数楽 モナドの概念を理解するためには、Kleisli圏(それを定義するための最小限の設定であるKleisli tripleがHaskellの意味でのMonadそのもの)やEilenberg-Moore代数(これについて知らないとモナドが数学的に何なのか不明瞭になる)に〜続く

2017-02-05 23:52:15
黒木玄 Gen Kuroki @genkuroki

#数楽 続き〜知らないと困ると思うのだが、「モナドだと分岐も扱えます」的な説明で終わっているものがググると見つかりまくり。 表現論を知っていれば淡中圏の話はもろにモナドの話の応用だとわかる。 異なる分野の比較は圏論を使う最大のメリットの一つなので、視界を狭めるのもったいない。

2017-02-05 23:58:17
黒木玄 Gen Kuroki @genkuroki

#数楽 ひとつ前のツイートの先頭の「続き〜」のあとに「について」を追加。

2017-02-06 00:12:23
黒木玄 Gen Kuroki @genkuroki

#数楽 リンクメモ slideshare.net/yoshihiromizog… 圏論のモナドとHaskellのモナド Yoshihiro Mizoguchi

2017-02-06 20:07:44
黒木玄 Gen Kuroki @genkuroki

#数楽 リンクメモ math.uchicago.edu/~may/VIGRE/VIG… A folkloric proof of Beck's manadicity theorem and several examples of monads C.Berger

2017-02-06 20:54:38
黒木玄 Gen Kuroki @genkuroki

#数楽 リンクメモ www-kb.is.s.u-tokyo.ac.jp/~asada/papers/… K.Asada Arrowはprofunctorsの圏におけるmonad with strengthだった。

2017-02-07 04:21:02
黒木玄 Gen Kuroki @genkuroki

#数楽 モナド話続き。monadについては少しは知っていた。HaskellのApplicativeそのものは知らなかったのですが、弱い意味で直積を保つ函手と同じものなので「全然知らなかった」とは言えない感じ。続く

2017-02-07 20:14:44
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。さらにHaskellではArrowが定義されていてどういうものか全然理解できなかったのですが、profunctorsの圏におけるmonad (with strength)と同じものだと書いてある文献が見つかった(まだ読んでいない)。現時点ではこんな感じ。続く

2017-02-07 20:18:12
黒木玄 Gen Kuroki @genkuroki

#数楽 対象の掛算が定義されていれば自然にモノイドのような代数系を定義できる。圏Cからそれ自身への函手全体の圏End C(射は自然変換)は函手の合成という自然な掛算を持っている。End Cにおけるモノイドをモナドと言う。これがモナドの定義。定義だけを見ても有用さはわからない。続く

2017-02-07 20:24:56
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。随伴函手の対からモナドは自然に構成される。よく出会う随伴函手の対の典型例は(モノイドや群や環などの)代数系の圏から集合の圏への忘却函手Uと集合をそれから生成される自由代数系に対応させる函手Fの対です。典型的なモナドはM=UFと構成されます。続く

2017-02-07 21:31:19
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。そのとき、集合Xに対してMX=UFX=(Xから生成された自由代数系の台集合)、たとえば代数系としてモノイドを選んだ場合にMXはXを文字集合とみなしたときの(有限の長さを持つ)文字列全体の集合になります(空文字列が単位元)。続く

2017-02-07 21:35:16
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。以下、例として、MX=(Xを文字集合とみなしたときの有限の長さを持つ文字列全体の集合)の場合を扱います。集合間の任意の写像f:X→Yに対して、MX内の文字列をfによって置換して得られるMY内の文字列を対応させる写像M:MX→MYが自明に定まります。続く

2017-02-07 21:59:35
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。こんな感じのMは函手(functor)の典型例でかつモナドの典型例になっています。 このとき、MMX=(MX内の各文字列をひとつの文字とみなし、それらを並べてできる「文字列」全体の集合)=(MX内の文字列を連結せずに単に並べたもの全体の集合)となります。続く

2017-02-07 22:04:12
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。文字列を連結せずに単に並べたものに対して、それらを連結した文字列を対応させる写像μ_X:MMX→MXが自然に定まります。さらにXの元を1文字だけの文字列に対応させる写像η_X:X→MXも自然に定まる。μとηが函手Mのモナド構造です。続く

2017-02-07 22:10:19
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。η_X:X→MXはHaskellではreturnと書かれています。さらに写像f:X→MYには写像f^*=μ_Y⚪︎Mf:MX→MYを自然に対応させることができます。Haskellではηがreturnで、f↦f^*が=<<:(X→MY)→(MX→MY)です。続く

2017-02-07 22:21:40
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。モナドMではMを2回作用させたMMXをμ_XによってMを1つだけ作用させたMXに戻せます。どから、Mを複数回作用させた結果を常にMを1回だけ作用させた場合に戻すことができる。そういうことを自然にできる設定がモナドの定義だと思っても問題ないと思います。続く

2017-02-07 22:25:44
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。集合Xから集合MXを作る操作は、Xの元を有限個並べたもの全体の集合を作る操作です。Xの元を有限個並べたものたちにはそれらを連結する演算が自然に定義されます。その演算がMの操作を2回繰り返したMMXから1回だけのMXへの写像μ_Xになっているわけです。続く

2017-02-07 22:29:54
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。これは一般のモナドのケースでも同様で、一般のモナドX↦TXのモナド構造μ_X:TTX→TXはTXに何らかの「演算」が定義されていることを表しているものとみなせます。続く

2017-02-07 22:33:08