#数楽 続き「抽象的な説明」についてHaskellの入門的解説をググって読むと、構文レベルの話(場合によっては単なるsyntax sugarの話)と応用の話と「それがどのような函手であるか」などなどの異なる事柄をすべてミックスした説明になっていて、私には分かり難い。続く

#数楽 「抽象的」話の続きもっと抽象的に説明してくれればわかりやすいのになと思うことが個人的には多い。これはあくまでも私個人の問題なのですが、「抽象的」という言葉を使ったせいで誤解されることが多いので補足させて下さい。続く

#数楽 続き。期待していることは、構文の詳細、実装の詳細、応用の詳細によらずに理解できることをざくっと解説してくれることである。いきなり完璧な理解は無理なので逐次近似的な理解を目指したいのですが、第0近似として「抽象的な説明」＝「実装の詳細によらない説明」があるとありがたいのだ。

#数楽 続き。構文のスタイルを変えても、実装の仕方を変えても、応用先を変えても変わらない基本的な考え方を知りたい。それを一言で「もっと抽象的に説明して欲しい」と言っているのだ。これは「抽象」という言葉の意味的にも正しい言い方だと思います。続く

#数楽 続き。まとめ：抽象的な説明によって、構文のスタイル、実装の仕方、応用先などなどを変えても変わらない基本的な考え方を説明してもらうことができれば、「どのように細かいことを気にしなくてもよいか」がわかって、逐次近似的な理解の出発点になる「第0近似」が得られる。

#数楽 たぶん、「どのように細かいことを気にしなくてもよいか」がわかることが大事なことなんだと思う。

#数楽 続き。数学の解説でも「どのように細かいことを気にしなくてもよいか」が不明瞭な説明は多いと思う。私もよくやってしまう。これは個人的な意見なのだが、特に「他人によって与えられた定義から出発する」という発想になるとどんどんつらくなることが多いと思う。続く

#数楽 続き。定義の背景にある考え方もしくは頭の使い方を理解することによって、定義から出発する必要が無くなるようにしないと、覚えなければいけないことが次々に増えて、自分の能力の限界を超えて永久に理解できない気持ちに陥る場面が増えると思う。

#数楽 @beyondDNShttps://usi-pl.github.io/lc/sp-2015/doc/Bird_Wadler. Introduction to Functional Programming.1ed.pdf … をありがたくダウンロードしました。ついでにリンクメモhttp://www.disi.unige.it/person/MoggiE/ftp/lics89.pdf …Moggiさんの有名なモナド論文(1989)

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

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

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

#数楽 アマゾンへのリンクhttps://www.amazon.co.jp/dp/4535787204 

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

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

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

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

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

#数楽 リンクメモhttp://www.slideshare.net/yoshihiromizoguchi/haskell-14848553 …圏論のモナドとHaskellのモナドYoshihiro Mizoguchi

#数楽 リンクメモhttp://www.math.uchicago.edu/~may/VIGRE/VIGRE2011/REUPapers/Berger.pdf …A folkloric proof of Beck's manadicity theorem and several examples of monadsC.Berger

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

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

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

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

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

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

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

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

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

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

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

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

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

#数楽 続き。自由モノイドの(すなわち「文字列」全体の集合を与える)X↦MXの話に戻る。モナドが与えられるとそのモナドに対応する「代数系」の概念が自然に定義されます。MXの代数系の構造(文字列が連結できること)はたった一つの写像μ_X:MMX→MXで表現されるのでした。続く

#数楽 続き。同様に集合Aにモノイドの構造が入っていれば、集合Aの元を並べたものにAのモノイド構造を使って連結して得られるAの元を対応させる写像α:MA→Aが得られます。写像αはAのモノイド構造の情報をすべて持っている。このような(A,α)をM代数と呼びます。続く

#数楽 続き。M代数の満たすべき公理系はモノイドの作用の公理系と完全に同じなので省略。モナドMはそれ1つだけでM代数と呼ばれる代数系のみたすべき条件をすべて知っているわけです。集合にそれから生成される自由モノイドを対応させるモナドはモノイドのみたすべき条件をすべて知っている。続く

#数楽 続き。これは自由群を作るモナドなど他のたくさんの代数系についても同じです。随伴函手の話に戻る。一般に圏C上のモナドTとT代数の圏C_T (C_TにはEilenberg-Moore圏という権威ありそうな名前が付いているが名前にびびるのは非数学的)のあいだには〜続く

#数楽 続き〜、T代数にT代数の構造を忘れたもの対応させる函手U_T:C_T→Cと、Cの対象Xに自由T代数TXを対応させる函手F_T:C→C_Tが自然に定まり、随伴函手対になり、自明にT=U_T F_Tとなります。T代数の正体がわかっていればこれで基本設定は〜

#数楽 続き〜終了なのですが、そうでないときには、具体的な随伴函手対U:D→C、F:C→DでモナドをT=UFと作ったとき、DがT代数の圏C_Tといつ同値または同型になるかを知る方法が必要。それがBeckのmonadicity定理です。MacLaneの圏論の教科書に書いてある。

#数楽 証明を読んだこともないし、詳しくもないのですが、DeligneさんはBeckの定理を「群」の概念を理解するためにもっとも基本的だと思われる淡中圏の理論の整備に使ったそうです。

#数楽 続く。群の定義は数学を少しかじった人達にはおなじみのものだと思いますが、実際に応用されるときには群そのものよりも、群の作用や表現の方が役に立つことが多いのです。群の作用や群の表現のように見えるもの達の方から群を作る方法があるのらば、群概念の応用範囲は大きく広がると〜続く

#数楽 続き〜考えられます。実際にそういう理論は作られており、現代ではそれらを総称して淡中双対性と呼ばれているようです。淡中先生は私が学生時代に習った先生達の先生です。各種の淡中双対性については→ https://ncatlab.org/nlab/show/Tannaka+duality …

#数楽 続き。群の表現のように見えるもの達(群の表現の圏のような圏)の中には条件を弱めると対応する群が無くなり、群概念を拡張する必要が出て来ます。量子群はそのような意味での群概念の一般化になっています。群では記述できない意味のある「対称性」が1970〜80年代に発見されました。

#数楽 私がモナドの話を始めたのでfunctionalプログラミングに興味を持った人が覗いて見たら、淡中双対性というガチ数学の話になって残念に思っている人達がいるかもしれませんが、これは数楽の雑談なので仕方がない。続く

#数楽 続き。というわけで、集合から自由モノイドを作るモナドM:C→Cの話に戻る。ここでC=(集合の圏)。このときC_M=(M代数の圏)=(モノイドの圏)となります。モノイドの圏の中には自由モノイドMX (Xは集合)達が含まれており、自由モノイド間の準同型g:MX→MYは〜続く

#数楽 続き〜、写像f:X→MYと一対一に対応しています。対応の作り方はf=η_X⚪︎gとg=f^*=μ_Y⚪︎Mfです。この対応は一般のモナドでも同様で、f↦f^*は、Haskellでの=<<::(X→MY)→(MX→MY)と書かれている"bind"です。続く

#数楽 続き。要するにHaskellでのモナドのbindは、圏論でのモナド上の自由代数間の射の記述そのものであるわけです。私にはこういう直観抜きにモナドの応用を理解できることが信じられません。理解の仕方には色々な経路があるものです。

#数楽 続き。一般に集合Xから生成される自由○○(○○はモノイドや群や環などの代数系の名前)をTXと書くと、TXからTYへの射(○○の準同型写像)はXからTYへの写像と自然に一対一に対応しています。これはXからTXへの写像(函数)にTXの元を代入できることを意味しています。続く

#数楽 続き。文字数制限の縛りに負けて「代入」と書くべきところでカギカッコを略してしまった。函数f:X→TYにTXの要素を文字通りの意味で代入することはできないのですが、TXが自由○○ならば「代入」できる。より一般にTがモナドでも同様に「代入」できるわけです。続く

#数楽 続き。自由○○(○○は代数系の名前、完全に一般の場合にはモナドTに対するT代数)に関する直観があれば、函数f:X→TYにTXの要素を代入できることは当然だと思えるようになります。Haskellではその操作をα∈TXについてα>>=fなどと書くわけです。

#数楽 続き。まとめ：モナドTに対するTXはXに新たな要素や演算を追加して作られた自由代数(「代数」の意味はT代数の意味でおそろしく拡張されている)であり、函数f:X→TYにTXの元を「代入」することができ、射f^*:TX→TYが自然に得られる。続く

#数楽 続き。以上の話は、自由モノイド、自由群などの例を知らず、「自由○○」という用語に関する直観を持たない人達にとってはありがたみがないかもしれませんが、そういう直観を持っていればHaskellのモナドについても「見たことがある！」と言えることを示した点で意味があると思います。

#数楽 もう一度まとめると、・モナドTはT代数を定める。・TXはXに新たな要素や演算を追加することによって作られた自由T代数である。・だから函数f:X→TYにTXの要素αを「代入」してTYの要素が得られる。・その「代入」操作をHaskellではα>>=fと書く。

#数楽 例：モナドMaybeをMaybe X=X⊔{Nothing}と定める。函数f:X→YはNothingをNothingに対応させることによって函数Maybe X→Maybe Yに拡張される。モナドの構造はNothingはNothingに移されるという規則で定まる。続く

#数楽 続き。Maybeモナドは計算できない場合にはNothingを返す函数を定義するために使えます。集合Xで生成される自由Maybe代数Maybe Xは集合XにNothingを追加して、Nothingは常にNothingに移すというルールで作られたものになっています。

#数楽 続き。Maybeモナドのモナド演算μ_X:Maybe Maybe X→Maybe Xは:Maybe Maybe Xで重複して追加された2つのNothingを1つにまとめる写像に過ぎません。

#数楽 例：任意の直和Maybeモナドは{Nothing}を任意の集合Aに置き換えた自明な一般化TX=X⊔A (disjoint union、交わりを持たない和集合、直和)を持ちます。モナド演算は重複して追加されたAをひとつにまとめる写像と定義されます。

#数楽 例：任意のモノイドS(たとえば文字列の集合S)に対して、TX=X×Sと定めると自然にTはモナドとみなせます。モナドの演算はμ_X:X×S×S→X×S, (x,a,b)↦(x,ab)です。これを使えばモノイドSの元(たとえば文字列)で計算のログを残すことができます。

#数楽 例：モナドは随伴函手から得られるのでした。FX=X×AとUY=Y^AからモナドTX=(X×A)^A=(A→X×A)が得られます。ここでB^A=(A→B)はAからBへの写像全体の集合。こういうものも実用的なのですが、出所は随伴函手の最も簡単な例のひとつである「カーリー化」。

#数楽 数学をある程度やると「自然な写像」の概念に馴染みます。自然な写像は特別に定義しなくてもいつでもそこにあるような気分になって来ます。そういう直観があれば様々な構成の詳細を見ることなく、色々理解できるようになります。そういう発想がないと圏論がらみの話はつらくなる一方だと思う。

#数楽 まとめ・モナドTに対してTXはXに新たな要素や演算を追加して作られる自由T代数であった。・モナドTによってXに様々なモノの追加して色々なことをできる。・モナド演算μ_X:TTX→TXはXに重複して追加されたモノをひとつにまとめる写像である。

#数楽 MaybeモナドTX=X⊔{⊥}の話の続き。Maybe X、NothingをそれぞれTX、⊥と書いた。TTX=X⊔{⊥}⊔{⊥'}と書き、以下x∈Xとする。モナド構造はη:X→TX, η(x)=x、μ:TTX→TX, μ(x)=x, μ(⊥)=μ(⊥')=⊥。続く

#数楽 続き。集合Aと写像α:TA→Aの組がT代数であるとは、η:A→TAとα:TA→Aの合成がid_Aに等しいことと、TTA→TA→A型の写像の合成α◦μ、α◦Tαが等しいこと。以下a∈Aとする。前者はα(a)=aを意味し、後者は常に成立。続く

#数楽 続き。集合AのT代数構造(=Maybe代数構造)α:TA→Aは集合Aの要素α(⊥)=:⊥_Aを任意に指定することしかしていない。要するにMaybe代数はpointed set(点付き集合、いち要素が指定されている集合)のことである。続く

#数楽 続き。T代数α:TA→Aとβ:TB→Bのあいだの射f:A→Bの定義は、写像f:A→BでTAからBへの写像としてf◦α=β◦Tfが成立することである。これはf(α(⊥))=β(⊥)を意味する。要するにT代数(=Maybe代数)のあいだの射は点付き集合の射と一致する。続く

#数楽 続き。要するに、集合の圏上のMaybeモナドが定めるMaybe代数の圏は点付き集合の圏に一致するということ。数学畑の人であってもMaybeモナドとか言われると「なにそれ？」と思う場合が大部分だろうが、点付き集合の圏であれば「ああ、それ知ってます」と感じると思う。

#数楽 点付き集合の圏の世界では、すべての集合Aに特別な要素⊥=Nothingが指定されていて、集合間の函数は⊥=Nothingを保つものしか考えない。函数の値が⊥=Nothingになることを「計算が失敗した」と解釈すると、函数の合成で何かを計算するときにどこかで失敗すると～続く

#数楽 続き～最終的な答えも⊥=Nothingになり、「途中の計算が失敗すると計算の全体も失敗する」と解釈できるようになる。たったこれだけの話なのだが、こういう話をコンピューター上でどのように実装するかに最初に詳しく触れてしまうと、超絶シンプルな話であることが見え難くなると思う。

#数楽 続き。関連数学用語解説【Aによって生成されたB】これは「Aを含む最小のB」という意味。例：整数全体の加法群をZと書くとき、「9と15で生成されたZの部分群」は「9と15を含むZの最小の部分群」という意味で3の倍数全体のなす加法群になる。

#数楽 関連用語解説続き代数系の名前○○に関する【自由○○】(自由モノイド、自由群、など)における「自由」(free)は必要最小限の関係式以外の関係式が「ない」という意味。例えば要素aから生成される自由群は無限巡回群{a^k|k∈Z}になる。続く

#数楽 続き。0でない整数nについてa^n=1という関係式が成立している場合には必要最小限ではない関係式が成立していることになるので自由群でなくなる。

#数楽 例：要素x,yから生成された自由な「体K上の可換環」は多項式環K[x,y]に同型になる。y^2=x^3のような必要最小限ではない関係式が成立していると自由ではなくなる。余計な関係に束縛されると自由でなくなるのはリアルな生活でもそうだろう。

#数楽 リンクメモhttps://arxiv.org/abs/math/0407251 …State monads and their algebrasF. Metayer集合の圏でのStateモナドTX=(X×S)^SのEM代数の圏は集合の圏と同値ということらしい(Sは空でないと仮定)。

#数楽 続き。集合XについてX^Sは自然にT上の代数になる。集合の圏におけるStateモナドT上の(Eilenberg-Moore)代数の圏をSets^Tと書くとき、( )^S:Sets→Sets^Tが圏同値を与えるということらしい。