今年の1月頃、Twitterでこのようなツイートをしました。
favの数だけモナドについての豆知識をツイートします
— こば(競プロのプロを目指す) (@kobae964) January 9, 2016
このツイートは界隈で広まり、(2016/12/18現在)133favをいただきました。しかしまだ56個しかツイートできていません。終わりが見えないのじゃ…(トホホ)
モナドtips1個消化するたびにノルマが2,3個増えるんだけど(歓喜)
— こば(競プロのプロを目指す) (@kobae964) 2016年11月6日
この記事では、このモナドtipsツイートに書いた知見をまとめていきたいと思います。
1月(卒論)
卒論でStone dualityについて調べていた。当然モナドについての知見が得られることとなった。((7)から(20)まで)
(7) モナドは随伴からできるし、モナドがあったら随伴を作る事ができる。複数の随伴から同じモナドができることがあるので、感覚的にはモナドの数は随伴の数より少ない。
— こば(競プロのプロを目指す) (@kobae964) 2016年1月9日
(20) 圏C,Dの間の随伴F-|GとD,Eの間の随伴J-|Kがある時、それらの合成の間にも随伴J.F -| G.Kが存在する。J,KがD上のモナドTを与えるとき、合成された随伴はC上のモナドG.T.Fを与える。
— こば(競プロのプロを目指す) (@kobae964) 2016年1月10日
11月
ラボでcall-by-push-valueについての発表をすることとなり、それについての知識を得ることになった。
(55) 副作用を持つ計算の表示的意味論を考えるときはモナドを使うと嬉しいことが知られている。評価戦略が値呼びの場合はクライスリ圏Kl(T), 名前呼びの場合はアイレンベルク・ムーア圏EM(T)を使うと良いことが知られている。
— こば(競プロのプロを目指す) (@kobae964) 2016年11月5日
(56) 値呼びと名前呼びの両方の評価戦略を埋め込める計算体系として、Call by push value calculusというものが知られている。詳しくはhttps://t.co/eUqnKnynQh を参照されたい。
— こば(競プロのプロを目指す) (@kobae964) 2016年11月6日
これから
まだ取り扱っていないテーマ(bialgebra, free monadの具体的な構成方法)などはやっていないはずなので、これから勉強してツイートしていきたい。