【追記あり】ChatGPTじゃなくて人力でモナドが発明された経緯を適当に調べた（ソース付き）。 #Haskell

モナドが何の役に立つのか書きそびれていたのでたらたらと追記した。(2023.2.15)

プログラミング言語が2-圏として考えられるということについてソースから訳出した。(2023.2.22)

動機

最近、chatGPTにいろいろ尋ねるのが流行っているらしい。Haskellで有名なモナドの概念がなぜ導入されたか尋ねている人を見かけて、そういやそういう記事見たことないなと思ったので適当に調べた。

一次ソース

元ネタは以下のマイナーだと思われる文献

An abstract view of programming languages
Eugenio Moggi教授のあんま読まれてない方の論文
Denotational Semantics
Peter D. Mosses教授のこの論文（2部あって後半の方）
邦訳があり邦訳で読んだ。

プログラミングのモナド発見の経緯

プログラミングのモナドはなんか包んだり抜き出したり見たいな感じの概念で知られてますが、プログラミングの概念をモジュール化する機構云々の開発の前段階がある。そもそもリストだかIOだか例外処理だかの概念をそれぞれ一つのモジュールにしようと思ったのにはわけがあり、それがプログラム意味論の中で一番数学的に美しいだかなんだか言われている表示的意味論の欠点批判にあった。

ピーターD.モーゼス教授による表示的意味論のモジュール性欠如批判

まず登場してくるのはイギリスの計算機科学者で表示的意味論の大家のピーターD.モーゼス教授である。

ピーターD.モーゼス教授のご尊顔

 Peter D. Mossesホームページから

1980年代に表示的意味論は完成の域に到達したかなんかで、ScottもGunterもMossesも文殊の知恵ともいわんばかりに表示的意味論の総論をまとめたレポートを報告して（2つ目の論文）、いやいや表示的意味論完成しましたねとばかりに祝杯をあげていたのかは知らないけれど表示的意味論の総まとめを行った。その中で著者の一人のモーゼスは公然と表示的意味論をディスり始めた。これがかの有名な？モーゼスの表示的意味論批判である。

該当部分の邦訳があるので引用すると以下のような批判である（2つ目の論文のp.106）。

表示的意味論の応用に関する別の問題として、意味記述の実用性（pragmatic aspects）の問題がある。”玩具の（toy）"言語に対して、”その領域をテーブルの上に並べ”、適当な（しかし、必ずしも十分に抽象的でない）意味を定義する意味方程式を与えるのはまったく簡単なことである。
しかし、（不幸なことに）”現実”のプログラミング言語の表示的意味記述には多数の複雑な領域が必要であるから、このアプローチを実用的なレベルにまで高めるのは容易ではない。部分的には、意味方程式が表示的意味の領域に陽に（explicitly）依存するという理由によって、大規模な意味記述を理解することがきわめて困難になる可能性がある。
関連する問題として、１つの言語（たとえば、Pascal）の意味記述の部分を、他の言語（たとえば、MODULA2）の意味記述に再利用することが現実的（feasible）でないという問題がある。ソフトウェア工学における同様な問題は、”モジュール（module）”の導入によって緩和された。 しかし、表示的意味論には、モジュールを表す記法がない。
実際、もし表示的意味の領域の定義をモジュールの中にカプセル化したとすれば、意味方程式の中でλ記法を使って意味を表すことは不可能になる。したがって、原始的（primitive）な意味を表現したり、意味を結合するために、モジュールの内部に限って定義される補助操作を使う必要がある。このようなわけで、高度のモジュール性（modularity）は（通常の）表示的意味論と両立しないように思われる。

正直この批判がすごくわかりにくいということが、プログラミングのモナドと一緒に語られることがほぼない原因だと思う。

ざっくり言うと、というかざっくりとしか言えないけれど、この批判を噛み砕いてみると、まず、表示的意味論では、意味関数を定義する必要があり、その定義を意味方程式（semantic equation）という。

↑こんな感じのやつ（2つ目の論文のp.74から）ここでモナディックオペレータがどうのこうの言っているがこれは単に単項演算かどうか言っているだけ。

この意味方程式は表示的意味論の意味が貧弱な時はすごくシンプルで数学的に取り扱いがしやすい。だけれども、意味領域を増やして（言語の機能を増やして）豊かな表現力を持たせると、当然命令に対して割り当てしなければいけない意味領域の意味が増えるので割り当てる意味領域に対する分岐条件とかの意味方程式が膨れ上がってくる。
このドンドコドンドコ膨れ上がる意味方程式の塊が読みにくいのわかりにくいのなんの。2つ目の論文読んでもらえればわかるように言語がどんどん拡張されていくごとに意味方程式が複雑怪奇になっていく。これはもうまとまりのない読書感想文をただ垂れ流しに数学的にやっているんじゃないかというばかりに非常に複雑な構造となっていって読みにくいわわかりにくいわ（2回目）。

ということで文句をいうと、意味ごとに分割して整理しろよと突っ込まれること間違いない。ところが、表示的意味論はその建付け上そういう意味領域ごとに意味方程式を整理して見通しの良い記述に書き直すということができない（モジュール性が欠如している）。

回りくどい話になったけれど、モーゼスが上の引用で言いたいことはそういう話で、こういう意味方程式が意味領域ごとに整理して見通しよい記述にする道具立てが全然ない、だから表示的意味論はダメなんだ！！と力いっぱい批判したのである。

これを便宜上、モーゼスによる表示的意味論のモジュール性欠如批判と呼んでおこう。

Eugenio Moggiによる鮮やかな解決（計算モナドの理論）

表示的意味論の大家であるモーゼスがこんなこと言いだしたもんだから、こりゃダメだ。表示的意味論はダメだという空気が蔓延することになったかどうかはわからないが、表示的意味論には致命的とは言わないまでも数学的に美しくない欠点が存在することが認知されるようになった。

意味方程式が膨れ上がってしまう上に、それを整理する手段が表示的意味論には存在しないという欠点は、素人目にも表示的意味論の理論を学んでみると明らかなことのように思われる。ああ、このまま表示的意味論はモジュール性の欠如という欠点を抱えたまま使っていくしかないのだ、と思われたその矢先（論文発表のものすごいすぐ、というか時系列的におかしいので集中講義かなにかで2つ目の論文発表の前か何かにMoggiは欠点を知っていたと思われる）、同じくイギリスのエジンバラ大学で計算機科学を学んでいた博士課程在学中の一院生のEugenio Moggiが、なんとこのモーゼスによる表示的意味論のモジュール性欠如批判の解決策を具体的に提案してしまったのである。

Eugenio Moggi教授のご尊顔（Wikipediaから）

その解決策というのが、計算モナドの理論なのである。

こんなことどこでも読んだことないが、1つ目の論文を読むとそういうことがそこはかとなく書いてある。1つ目の論文のp.3あたり。

「2-圏論」としてのプログラミング言語理論

どうやらMoggiはプログラミング言語の理論というものを圏論的に考えて

プログラミング言語　＝　２-圏
表示的意味論　　　　＝　２-関手
詳細化（refinement）＝　自然変換

という対応が成り立つと考えついたのがエポックなところだったようだ。つまり普通の圏論（１-圏論）ではなくプログラミング言語理論というものを、当時もあんまり情報がなかったろうに斬新に、２-圏論 、で考えたのである。
つまり、有名なHask圏 は通常の１-圏じゃなくて、２-圏じゃないといけないのだ～～～。ええ、な、なんだってー！（この記事で一番言いたかったこと）

こっからは２-圏もよく知らん圏論知らん人の感想みたいなことを書くと、２-圏だとモナドが普通に出てくるらしい。つまり、特殊な２-関手、つまり特別な表示的意味論が理論的に自動的に導出されるので、この特別な２-関手を調べてみるとうまい性質（モジュール性）があったということなんだろうかと思う（しらんけど）。

個人的に一番の変化としては、表示的意味論の一番重要だと思われる意味関数が発展的解消してしまうところが一番肝心なところだと思いました。つまり、意味関数の意味方程式が云々という前に、意味関数が発展的解消をしてしまうのである。

モナドは何の役に立つのか

あんまり語られないが、モナドって結局何の役に立つかというと、最初にも言っているが、非決定計算とかIOとか例外処理といった普通のプログラミング言語に備わっている基本機能をモジュール化することができるというところにある。

つまり、機能ごとに実装分離できるようになる。そんなこと当たり前じゃないか、と言われるかもしれないが、本当にそうだろうか。例えば実装が比較的簡単なSchemeから継続の機能だけ抜いたScheme--を簡単に作れるだろうか？（HaskellであればContモナドをインポートしないだけでできる）

Schemeであれば、言語の機能の呼び出しはeval関数に組み込まれており（このeval関数の実装が上で言った表示的意味論の意味方程式に相当する、eval関数はまんま意味関数に相当）、継続機能に関係する部分だけを単純にくくりだすということができない（類例はSICP2nd ed.の４章）。

逆にモナドにできるプログラミング言語の機能を新たに開発したとして、Haskellであれば基本インポートするだけでeval関数に相当する部分に手をいれず 簡単に言語を拡張することができる。この既存の部分に原則手をいれず簡単に言語の機能を拡張することができるというところが、モナドの有用な点なのである。

まとめ

Hask圏は2-圏。
プログラミング言語理論の圏論は２-圏論。
モナドは圏論的には2-圏から考えないとMoggiの考えは追えない。
モナドはIOとか非決定計算、例外処理といった機能をモジュール化して『驚異の』実装分離を可能にする（なんで驚異であるのかはSchemeのeval関数の実装を調べないとわからないところがわかりにくい。）

再追記（2023.2.22）

Hask圏が2-圏として扱えるということについて言葉足らずだったので追記

まず根拠の原典に当たってみる。
一つ目の論文"An abstract view of programming languages"の"Programming languages with type-constructors and polymorphic functions."の節を適当に訳出（間違いありましたらご指摘ください。）

Programming languages with type-constructors and polymorphic functions.

[HJ] proposes a reinterpretation of the paradigm of Categorical Logic in terms of data-refinement, more generally in terms of an implementation relation between two semantics for the same programming language:

programming language as category

denotational semantics as functor

refinement as natural transformation

The paper divides a programming language in an inner part, with only basic types and operations whose interpretation has to be supplied by the user, and an outter part, which specify type constructors(as endofunctors) and polymorphic operations(as natural transformations between endofunctors) with a fixed interpretation in every denotational semantics. However, it seems natural to let the user specify also the implementation of type constructors(e.g. List) and polymorphic functions(e.g. reverse). The paradigm proposed by Hoare shold be reformulated as follows:

programming language as 2-category( with finite products)

denotational semantics as 2-functor( preserving finite products)

refinement as lax-natural transformation

Intuitively, in the programming language L as a 2-category, 1-morphisms are names for type constructors(with an given arity) and 2-morphisms are names for polymorphic functions. If L has only one object(for simplicity), then a denotational semantics from L to Cat should map the only object of L to a category C, 1-morphisms to endofunctors on C, 2-morphisms to natural transformation, by respecting the arities.
Finally, to justify the choice of lax-natural transformations, we have to ask how does the simple view of a language as a category fit in the more general one, of a language as a 2-category, and then check whether the general notion of refinement specialises to natural transformations.
Given a category Path(G) freely generated from a graph G, we can identify it with the 2-ccategory with finite products Free(G) freely generated from an object L, 1-morphisms a : 1 -> L for each node of G and 2-morphisms f: a=> b for each edge from a to b in G.

型構築子と多相関数を持つプログラミング言語

[HJ]¹ は、圏論的論理（Categorical Logic）のパラダイムを、データ詳細化（data-refinement）の観点、さらにより一般的に、同じプログラミング言語に対する二つの意味論の間の実装関係という観点から、再解釈することを提案している。

圏としてのプログラミング言語

関手としての表示的意味論

自然変換としての詳細化（refinement）

この論文では、プログラミング言語を内側部分と外側部分に分割する。内側部分においては、ユーザが解釈を与えなければならない基本的な型と操作のみを持ち、外側部分においては、すべての表示的意味論において不動な解釈を持つ型構築子（自己関手）と多相演算（自己関手の間の自然変換）を指定している。しかしながら、型構築子（たとえばList）や多相関数（たとえば、reverse）の実装もユーザが指定できるようにするのが自然であると思われる。したがって、Hoareが提案したパラダイムは、以下のように再定式化されるべきである。

2-圏(有限積を持つ)としてのプログラミング言語

2-関手(有限積を保存する)としての表示的意味論

lax-自然変換として詳細化（refinement）

直観的には、2-圏としてのプログラミング言語 L において、1-射は(任意のアリティを持つ)型構築子の名前であり、2-射は多相関数の名前である。（簡単のため） L の対象が1つだけとするならば、L から Cat への表示的意味は、Lのただ一つの対象を圏 C に、1-射をC上の自己関手に、2-射を自然変換に、アリティをそのままに写せばよいことになる。
最後に、lax-自然変換の選択を正当化するために、言語を圏とする単純な見方、より一般的には、言語を2-圏とする見方が、どの程度適合するかを問わなくてはならないし、詳細化の一般概念が自然変換に特化しているかどうかを確認しなくてはならない。
グラフ G から自由に生成される（freely generated）圏 Path(G) が与えられたとき、我々はそれを有限積を持つ2-圏 Free(G) で対象 L から自由に生成されたものと同一視することができるし、Gの各ノードに対し 1-射 a: 1 -> L を、Gにおける a から b への各辺に対し2-射 f:a => bを同一視することができる。

まとめ２

2-圏の理論（も）さっぱりわからんので、なんとも言えないが無理やり書く。誤解があればご指摘ください。

1-圏としてのHask圏、2-圏としてのHask圏

まず、あの構造化プログラミングを提唱した一人としても有名なホーアがプログラミング言語理論の圏論的定式化を提唱していたというのは驚き。
Moggiはホーアの提唱が不適切だということで2-圏としてのプログラミング言語理論を提唱したという話の流れだ。
1-圏として見られるHask圏の議論はこのMoggi以前のホーアのプログラミング言語の圏論理論的なもののように解釈できる。つまり、1-圏としてのHask圏も間違っているわけではない（今回再追記した趣旨）。
1-圏としてのHask圏を信じるならばHJ¹は必読だろう（読みにくいので自分は読んでいない）。

Moggiの定式化にもどると、上記文で出てくる2-圏としてのプログラミング言語 L というのがHask圏と考えるべきだと（自分は）理解できる。（簡単のために）対象が１つだけという、実質制約が、出てくるが、ここはちょっと自分も単純に理解できないので有識者のご意見を待ちたい。

なんで2-圏で考えないといけないのかというと、1-圏だとユーザー定義の型構築子や多相関数の意味付けができないからである。 2-圏で考えると2-射、1-射それに対象としての圏の射についても関手で対応付けがとれる。1-圏だとすると意味付けの際に型構築子と多相関数の意味領域というものが無いので理論的にユーザー定義型構築子や多相関数が定義できない。それが不合理だということでMoggiは2-圏だとしたようである。

関手的意味論

関手が表示的意味論に相当するというのは、ローヴェアの関手的意味論の影響を受けている気もするが、次のようなことだろう。まず次の2つの圏が存在する。

プログラミング言語の圏 L
プログラミング言語の意味の圏Cat （数学的対象からなる圏、まさに数学で話題とする圏）

表示的意味論というのはプログラムを数学的対象に割り当てる対応のことだから、プログラミング言語 L の意味付けというのは対応付け
eval : L -> Cat（雑な記号の使い方）
のことであり、これは2-圏の間の対応付けといえる。つまり2-関手。だから2-関手は表示的意味論と解釈できるということだろう。

2-関手の像は対象を圏C、1-射を自己関手になるので、関手の像は圏とはならないが、自己関手の圏みたいな感じになる。そう考えると、ワドラーのジョークとされているもの『モナドは単なる自己関手の圏におけるモノイド対象だよ。何か問題でも？』は、実は真面目にMoggiの論文を引用した話かもしれず、この2-関手の意味論のことを言っているとも解釈できる。

lax-自然変換としての詳細化

まず謝罪。記事中で、lax-、をつけずに単に自然変換と書いてました（すみません）。lax-自然変換わからないので安直によくわからず省略しました。多分、表示的意味を変えないプログラムの変更みたいな操作でしょう。

C.A.R. Hoare,H.Jifeng. Natural transformations and data refinement(1988) 読んでないが、ホーアが著者に入っているのでここでいうrefinementは詳細化（構造化プログラミングの段階的詳細化,stepwise refinementの）のことだとわかる。 ↩ ↩²