#数楽 モナド話続き。Haskellを使うためにはモナド必須なのでモナドについて知りたい人が増えているんだと思いますが、数学抜きで理解せざるを得ない人達が多くて、大変なことになっている様子をググると確認できる感じ。「自然な写像」の概念抜きだと何もかも複雑に見えてしまう。

#数楽 Stateモナドの話。集合の圏におけるStateモナドはTX=(X×S)^S=(S→X×S)=(SからX×Sへの函数全体の集合)と定義されます。実際にはこれとある種の自然な写像を組み合わせたものがモナドです。ここで、Sは「状態」全体の集合です。続く

#数楽 続き。Haskellに関する解説で、Sの例として「整数を格納したスタックの状態(スタックにどのような数が積まれているか)全体の集合」を採用している場合が多いようです。より一般にコンピューターのメモリーの状態全体の集合をイメージしておけばよいのだと思います。続く

#数楽 Stateモナドは2つの函手FX=X×S={(x,s)|x∈X,s∈S} (直積)、UX=X^S=(S→X)={f:S→X} (べき乗)の合成UFX=U(X×S)=(X×S)^Sに等しいです。直積とべき乗は随伴函手なのでその合成は自然にモナドになります(一般論)。続く

#数楽 続き。しかし、一般論をいきなり勉強しても大抵の場合「死ぬ」と思います。まずは具体例で「どのような写像(函数)が自然にそこにあるか」を確認しまくって感覚を磨く方がよいと思う。これは、24程度の整数を見たこともない人が整数論の一般論を学び始めても「死ぬ」のと同じことです。

#数楽 例えば、函数φ:X→Yに対して、函数f:S→Xを合成函数φ⚪︎f:S→Yに移す函数(写像)が自然に定まり、(x,s)∈X×Sを(f(x),s)∈Y×Sに移す函数(写像)も自然に定まる。数学に慣れるとこの手の自然に定まる写像は「常に最初からある」という感覚になります。続く

#数楽 続き。Sの直積とSによる場合べき乗に関する自然な写像(函数)の作り方は、それらを合成したStateモナドTX=(X×S)^Sの方にも伝搬します。自然に写像を作る仕組みが自然に伝搬する仕組みを抽象化したものが圏論だと思うことができるので、こういうことの認識は重要です。続く

#数楽 函数φ:X→Yが与えられると、函数S→X×S,s↦(f(s),u(s))を函数S→Y×S,(φ(f(s)),u(s))に対応する函数Tφ:TX=(S→X×S)→(S→Y×S)=TYが自然に得られます。これでTは函手とみなされる。

#数楽 AからBへの写像全体の集合をHaskellっぽく(A→B)と書いているのですが(通常の数学記号ではB^A)、直積の方はA×Bと通常の数学記号を使っています。直積はHaskell的には(A,B)のことです。大文字小文字のスタイルもHaskellと違っている。

#数楽 自然な写像達がおりなす世界をコンピューター上に実現するためには、一つひとつ自然な写像のコードを書かないといけないのですが、数学に慣れていると極めて不快な程度に面倒に感じられます。コンピューターが最初から数学を知っていて自然な写像は全部自動的に定義されていて欲しい。

#数楽 自然な写像がすべて自動的に最初からある環境でプログラミングできたら、プログラミングは今よりも易しくなるように思えます。

#数楽 https://twitter.com/genkuroki/status/830200074441420800 …訂正「に対応する函数」→「に対応させる函数」

#数楽 自然な写像(函数)の話の続き。函数f:X×S→Yと函数g:X→(S→Y)のあいだには自然な一対一対応があります。fに対応するgはg:x↦(s↦f(x,s))であり、gに対応するfはf:(x,s)↦g(x)(s)です。所謂カーリー化とその逆の対応の話です。

#数楽 一般に(FX→Y)と(X→UY)の間に自然な一対一対応があるときFとUは互いに随伴であると言います。FX=X×SとUY=Y^Sは互いに随伴です。直積とべき乗は最も易しい随伴函手の一例になっています。随伴函手の正確な定義を知らなくても易しい随伴函手の例は認識可能です。

#数楽 自明過ぎる自然な写像に恒等写像1_X:X→Xがあります。恒等写像が自然な写像を作る操作でどのように伝搬して行くかを見ることはとても基本的です。1_{S→Y}:(S→Y)→(S→Y)には函数の評価函数eval:(S→Y)×S→Y,(g,s)↦g(s)が対応しています。続き

#数楽 続き。1_{X×S}:X×S→X×Sにはη_X:X→(S→X×S),x↦(s↦(x,s))が自然に対応しています。TX=(S→X×S)なので、η_XはXをTXに自然に埋め込む写像になっています。η_XはHaskellではreturnと書く習慣になっているようです。

#数楽 eval:(S→Y)×S→Yで、Y=X×Sとおき、さらに全体をS乗することによって、(S→(S→X×S)×S)→(S→X×S)f↦eval⚪︎fという自然な写像も得られます。これはμ_X:TTX→TXと書かれ、η_X:X→TXと合わせて、Tのモナド構造を定めます。

#数楽 続き。モナドの一般的な定義を知らなくても、自然な写像の伝搬の例を知っていれば、モナドの簡単な例を認識することは容易です。

#数楽 Stateモナドのモナド則(自己函手の圏でモノイドになっていること)についてコメント。結合律はevalの順番によらず結果が同じことを意味しています。

#数楽 函数φ:X→(S→Y×S)には自然に函数φ':X×S→Y×Sが対応するので、函数f:S→X×Sに函数φ'⚪︎f:S→Y×Sを対応させることもできます。Haskellではφ'⚪︎fをf>>=φと書きます。(注意：Stateモナド以外ではφ'⚪︎fは別のものになる。)

#数楽 これで写像( )^*:(X→TY)→(TX→TY)φ↦φ^*=(f↦φ'⚪︎f)が定まった。これに対応する写像TX→((X→TY)→TY)がHaskellでの>>=です。( )^*=μ_Y⚪︎T、μ_Y=(1_{TY})^*なので( )^*もモナドを定めます。

#数楽 以上で述べた自然な写像の作り方を数学科で習った覚えはないのですが、大学1年〜2年レベルの話を習っていればそこから容易に導き出せる話です。初めて触れるとややこしく感じるかもしれませんが、すべて自明(trivial)です。どこにも特別なアイデアは含まれていない。完全に自明。

#数楽 しかし、自明なことさえ理解できないようだと、アイデアが必要な場面で手も足も出なくなくなるので、たとえ完全に自明で退屈な話であっても地道に手を動かして納得しておくことは大事なことだと思います。ただし、自明で退屈な話に過ぎないと認識しておくことも大事。どっちも大事。

#数楽 しまった。説明するのを忘れていた。x↦f(x)はxをf(x)に対応させる函数を意味しています。数学では標準的に↦記号がよく使われています。とても便利です。おすすめ。λx(f(x))\x->f(x)などと同じ意味です。

#数楽 以上ではStateモナドTX=(X×S)^S=(S→X×S)の周辺にどのような函数(写像)が自然にあるのかについて地道に説明してみたのですが、その説明はそのままモナドとしてのTの定義の解説そのものになっています。自然な函数達は「最初からある」と思えないと不便。

#数楽 圏論的な仕組みは自然な函数達が最初からあるように見えるようにする道具だとみなせます。そういう道具が豊富にあれば、当然あるべき自然な函数達のかなりの部分は最初からあるということになるので、その分のコードを書かなくてすむようになるわけです。

#数楽 チョー専門外の話なので、以下の話をあんまり信用しないで欲しいのですが、StateモナドにおけるTX=(S→X×S)の要素(函数になる)S→X×S,s↦(f(s),u(s))は、状態s(例：スタックにどのように数が積まれているか)から出発した計算結果がf(s)で〜続く

#数楽 続き〜、u(s)は計算後の状態(例：計算後にスタックにどのように数が積まれているか)の状態を意味しています。計算結果と状態が変化していく様子は函数φ':X×S→Y×Sで記述されます。もとの函数h:S→X×S,s↦(f(s),u(s))との合成でより複雑な計算が記述される。

#数楽 函数φ':X×S→Y×Sはカーリー化によって函数φ:X→(S→Y×S)=TYと一対一に対応しているのでした。X→TY型の函数は一つ前の計算結果と状態を引き継いで、次の計算結果と状態を作り出す函数だとみなせます。

#数楽 函数の合成を矢線の連結で表すとSに含まれる状態が変化しながら計算が進む様子は函数の合成S→X_1×S→X_2×S→…→X_n×Sで記述され、これはX_1→TX_2, X_2→TX_3, …という値がTX_iに含まれる函数達からモナドの仕組みを使って得られる〜続く

#数楽 続き〜写像の列TX_1→TX_2→…→TX_nの合成によって、TX_1=(S→X_1×S)の要素をうつしたものになっているわけです。このようにして、状態s∈Sが次々と変化しながら計算が進む様子を記述している函数の合成をStateモナドを使って記述できるわけです。

#数楽 注意：以上ではモナドという用語は使っていてもその定義は使っていない。集合と写像(函数)と自然な写像(函数)に関する自明な話しか使っていません。さらに、読者の便のためにHaskellでの記号法にも触れましたが、プログラミング言語によらない普遍的な話しかしていない。

#数楽 以上でしたような説明の仕方になっている解説文が見つからない(もしくは見つけにくい)のはおそらく「コードを書くためには直接的に役に立たないから」だと思う。Haskellではdo構文によって以上に述べたようなことをあまり意識しなくていいように工夫されている。

#数楽 いきなり、do構文を使って説明されると裏で何をやっていると思えばよいのかわかりにくくなるような気がしないでもない。

#数楽 Stateモナドについてググってみた。随伴との関係1/2随伴がモテないのはどう考えてもモナドが悪い！（モナドとコモナドの関係が分かる話） - Moon? Shadow! - Misc Memohttp://kagamilove0707.hatenablog.com/entry/2014/11/02/210400 …

#数楽 モナドと随伴の関係2/2Monads as adjunctions (StackOverflow)http://stackoverflow.com/questions/4697320/monads-as-adjunctions …

#数楽 目次https://twitter.com/genkuroki/status/827554504056807424 …集合Xを不定元(変数)の集合とみなしてそれから生成される体K上の多項式環をTX=K[K[x]]と書くとＴはモナド。集合Xから生成される自由モナドをList X=[X]と書くとList=[ ]はモナド。続く

#数楽 目次↓に続くhttps://twitter.com/genkuroki/status/830669374847488001 …

#数楽 目次続きhttps://twitter.com/genkuroki/status/827567695235198977 …Maybe X=X⊔{Nothing}とおくとMaybeはモナド。Either_R X=X⊔RとおくとEither_Rはモナド。

#数楽 記号法X⊔Y=(集合XとYの交わりのない和集合(直和))。XとYの交わりのないコピーを作って、それらの和集合を作ったと考えるとよい。Haskellの記号法ではX|Y。X×Y={(x,y)|x∈X,y∈Y}(直積)。Haskellの記号法でのタプル(X,Y)と同じ。

#数楽 記号法Y^X=(X→Y)=(XからYへの写像(函数)全体の集合)。べき乗。x↦f(x)はxをf(x)に対応させる函数(写像)を表す。λx(f(x))や\x->f(x)と同じ。写像と函数を同じ意味で使うつもり。g⚪︎fは函数fとgの合成。g⚪︎f(x)=g(f(x))

#数楽 任意の集合X,Y,etcを扱うのはちょっとあれなのですが、そういうことは気にしない方針。自然な写像(函数)達はわざわざ定義しなくても常に最初から文脈ごとに適切に決まっていると思い続ける。(この機能がプログラミング言語でもあるととてもありがたい。誰か実装して！)

#数楽 目次https://twitter.com/genkuroki/status/828208139904258048 …『圏論の歩き方』の表紙はかわいい。モナドを理解するにはモナドT上のEilenberg-Moore代数(T代数)の圏(EM圏)と自由T代数の圏(Kleisli圏)の概念が最も基本的。

#数楽 目次https://twitter.com/genkuroki/status/828684949662228480 …HaskellではMonadをさらに一般化したArrowが実装されているが、Arrowも実はモナドだった(Arrowはprofunctorsの圏におけるモナド)。

#数楽 目次https://twitter.com/genkuroki/status/828944225437835264 …モナドの理解のためにはEM圏やKleisli圏が基本的だが、それらを理解するためにはモナドと随伴函手対の関係について理解することが基本的。随伴函手F:C→DとU:D→CからT=UFであらゆるモナドを作れる。続く

#数楽 続き。自然にHom_D(FX,Y)≃Hom_C(X,UY)のときT=UF:C→Cはモナド。逆にモナドT:C→Cに対して、T代数の圏(EM圏)をDとすることによってそのようなFとUを作れる。モナドTのEM圏から来るFとUの組はTを作るFとUの組の中での親玉(終対象)。続く

#数楽 続き。EM圏の中には自由T代数達TXの圏(Kleisli圏)が含まれており、Kleisli圏からもTを作るFとUの組が得られる(モナドTを作るFとUの組の圏の中での始対象)。自由T代数間の射f^*:TX→TYは函数f:X→TYと一対一に対応する。続く

#数楽 続き。例えば、TX=(Xから生成される自由モノイド)のケースでは、T代数はモノイドと一致し、自由モノイド間のモノイドの準同型写像TX→TYは写像X→TYと自然に一対一に対応している。一般のモナドTでも同様のことが起こっている。続く

#数楽 続き。Haskellのモナドでは函数f:X→TYに函数f^*:TX→TYを対応させる函数(=<<):(X→TY)→(TX→TY)が定義されているが、これは函数f:X→TYから自由T代数間のT代数の射f^*:TX→TYが得られるという事実を実装しているに過ぎない。続く

#数楽 続き。Haskellでのモナドの使い方の基本は、「文脈」込みのTXからTYへの函数が、XからTYへの任意の函数から得られるという使い方。XからTYへの函数fに、TXの元xを「代入」して、TYの元x>>=fを得ることができる。数学を知っていればどう見ても自由〇〇代数の話。

#数楽 目次https://twitter.com/genkuroki/status/828976295568670721 …Beckのモナド性定理はDeligneさんによる淡中圏の理論の構成に使われた。淡中圏の定義はおおざっぱには「群の表現の圏のような圏」のことであり、そこから逆に群を作ることができる。

#数楽 目次https://twitter.com/genkuroki/status/829008592825053184 …MaybeモナドTX=X⊔{Nothing}EitherモナドTX=X⊔AモノイドSに関するWriterモナドTX=X×S

#数楽 目次https://twitter.com/genkuroki/status/829146392044007424 …Maybeモナドの話をより詳しく。Maybeモナド上の代数(Maybe代数)は点付き集合(1点が指定された集合)の圏に一致。X⊔{⊥}は集合Xから生成された自由な「点付き集合」(指定されている点は⊥)になっている。

#数楽 https://twitter.com/genkuroki/status/829314379350945794 …関連数学用語解説。「Aから生成されたB」とは。「自由〇〇代数」(自由モノイド、自由群、…)とは。

#数楽 目次https://twitter.com/genkuroki/status/829666571194769409 …Sが空でない集合のとき、集合の圏でのStateモナドTX=(X×S)^S上の代数(T代数)の圏は集合の圏と同値。集合YにY^Sを対応させる函手が圏同値を与える。

#数楽 モナド話目次https://twitter.com/genkuroki/status/830190990002511872 …StateモナドTX=(X×S)^S=(S→X×S)を題材に「自然な写像」(自然に得られる函数)の例を紹介。圏論について勉強する前に「自然な写像」の概念を理解しておくと超絶楽になる。個人的には必須だと思う。

#数楽 StateモナドTX=(X×S)^Sは互いに随伴な直積函手FX=X×Sとべき乗函手UY=Y^S=(S→Y)からT=UFで得られるのでした。問題：空でない集合Rに関する継続モナドTX=R^(R^X)はどのような随伴函手対から得られるか？

#数楽 継続モナド続き。以下集合全体の圏をCと書き、射の向きを逆転させた双対圏をC'と書きましょう。問題の答え：F:C→C', FX=R^XとU:C'→C, UY=R^Yは互いに随伴であり、継続モナドはUFX=R^{R^X}として得られる。

#数楽 答え続き。FとUが随伴函手対になっていることの証明：Hom_{C'}(FX,Y)≃Hom_{C'}(R^X,Y)≃Hom_C(Y,R^X)≃Hom_C(X×Y,R)≃Hom_C(Y×X,R)≃Hom_C(X,R^Y)≃Hom_C(X,UY)

#数楽 継続モナドTの定義TX=R^R^X=R^(R^X)η:X→TX=R^R^Xη(x)=(f↦f(x)), x∈X, f∈R^Xμ:TTX=R^R^R^R^X→TX=R^R^Xμ(f)=(g↦f(h↦h(g))), f∈TTX, g∈R^X, h∈R^R^X

#数楽 問題：(1)TX=R^R^Xのとき自然な写像X→TXとTTX→TXの作り方は一つ前のツイートの定義以外に無さそうなことを確認せよ。(2)随伴函手対からTを作ること経由で一つ前のツイートの定義と同じ写像が出て来ることを確認せよ。地道にやるしかないので解答例は無し。

#数楽 ηの方は簡単。(X→TX=R^R^X)≃(X×R^X→R)の型の自然な函数はeval(x,f)=f(x)であり、これに対応する函数がη:X→TXです。μの方も地道にかつ冷静に観察すれば「同様」であることがわかる。

#数楽 φ:X→TY=R^R^Yに対して、φ^*:TX=R^R^X→TY=R^R^Yが次のように自然に定まる。φ^*(f)=f(x↦φ(x)(g)), f∈R^R^X, x∈X, φ(x)∈R^R^Y, g∈R^Y, φ(x)(g)∈RHaskellではf>>=φと書く。

#数楽 Haskellではφ^*(f)をf>>=φと書き、ηをreturnと書く。

#数楽 nLabでのcontinuation monadの解説https://ncatlab.org/nlab/show/continuation+monad …

#数楽 訂正https://twitter.com/genkuroki/status/830669374847488001 …集合Xから生成される体K上の多項式環はK[K[x]]でないです。TX=K[X]もしくはTX=K[{t_x}_{x∈X}]です。

#数楽 モナドに限らず、圏論的なツールをコンピューター上で実現するためにはたくさんの函数を書かなければいけません。それを解読する側はどうすれば「わけのわからない函数がたくさん定義されている」と思わずにすむか？一つの方法は数学を勉強して「自然な写像」の構成になれることです。

#数楽 続き。圏論的に自然な構成は自然な写像(自然に作られる函数)たち(canonical mappings)を地道に確認して行くことで数学的な自然さを理解できることが多いです。数学科では集合と写像の話とか代数での準同型写像やテンソル積などで経験する話と言ってよいのかな？

#数楽 訂正。文字数制限に負けた。https://twitter.com/genkuroki/status/830726170404548609 …φ^*(f)=(f>>=φ)の正しい定義はφ^*(f)=(g↦f(x↦φ(x)(g))), f∈R^R^X, x∈X, φ(x)∈R^R^Y, g∈R^Y, φ(x)(g)∈R

#数楽 計算用紙に矢線を描いた図式を描いて考えるときには間違えようがないのですが、打ち込むときにミスる。自然な写像達を最初からコンピューターが知っていて人間がコードを打ち込む必要がない方がストレスが減る。

#数楽 函数(写像)を矢線などで表した図で考えるときに、常にすべての矢線にf,g,etcのような名前をつけようとすると気軽に考えることができなくなって死にます。大部分の矢線に名前をつけずにA→Bのまま扱ったりします。文脈的にどの函数なのかが明らかならそれで困らない。

#数楽 一方、コンピューターに複雑な写像の合成の仕方を教える場合には全部コードを書いてやらなければいけません。たとえ数学的に「その自然な写像は文脈的にあれしかない」となるケースであってもそうしなければいけない。それはストレスなのでコンピューターで自動化されている方がありがたい。

#数楽 継続モナド話続きリンクメモhttps://www.slideshare.net/mobile/RuiccRail/ss-52718653 …並行プログラミングと継続モナドKousuke Ruichi継続モナドの使い方の解説でこれは分かりやすそうだと思いました。

#数楽 リンクメモhttp://u1roh.hatenadiary.jp/entry/2014/12/18/000849 …例として【画面上の2点をクリックするとその2点を結ぶ直線を作図する機能を課題】に用いて継続モナドの解説

#数楽 継続モナド話は一旦中断して、モノイドとコモノイドの話。以下、1=(1点集合)={・}とします。集合Aがモノイドであるとは、積A×A→Aと単位元1→Aが定められていて、結合法則と単位元の条件が成立していることです。これの矢線の向きを逆にしたものをコモノイドと言います。