プログラミングにおけるモナドの初期の歴史について

• P. Wadler "How to Replace Failure by a List of Successes" (1985)
• E. Moggi "Computational Lambda-Calculus and Monads" (1988)
• M. Spivey "A Functional Theory of Exceptions" (1990)
• E. Moggi "Notions of Computation and Monads" (1991)
• P. Wadler "The Essence of Functional Programming" (1992)
• S. Peyton Jones、P. Wadler "Imperative Functional Programming" (1993)

あたりのこと。
目次:

• E. Moggi "Computational Lambda-Calculus and Monads" (1988)
  • プログラムの解釈
  • 意味論で使う操作
  • モナド則
• M. Spivey "A Functional Theory of Exceptions" (1990)
• P. Wadler "The essence of Functional Programming" (1992)
  • きれいな値と汚い値
  • きれいな関数と汚い値 (Applicative)
• S. Peyton Jones、P. Wadler "Imperative Functional Programming" (1993)

E. Moggi "Computational Lambda-Calculus and Monads" (1988)

プログラミングにおけるモナドの起源としては、モッジの「Computational Lambda-Calculus and Monads」(1988)、「Notions of Computation and Monads」(1991)あたりがあげられる。ただしモッジの論文はプログラムの意味論についてのものなので、実際のプログラムでモナドを利用している訳ではない。

プログラムの解釈

モッジの論文の基本の考えは意味論上で値と計算を区別するということ。

たとえば

7

とか

gcd(123,45)

というプログラムがあったとき、普通の意味論ではこれらを整数の集合 ℤ の要素として解釈する。
しかしモッジは、これを ℤ ではなくそれと別の Tℤ で扱うことを提案した。また整数ℤに限らず、計算結果が型AになるところをTAとする。ここでTℤとかTAが何を表すかというと、それは扱うプログラミング言語の性質次第。

たとえば、ランダムウォークでの次の位置を返す関数randwalkを持つ言語を扱うとする。すると関数呼び出し

randwalk(5)

は、4または6を返すけれど、どちらを返すかは非決定的になる。
この「 randwalk(5) 」のプログラミング言語上の型はint型だけど、意味論上ではこれをℤの要素として扱うのは適切ではないだろう。このような非決定計算を含む言語を考える場合、

TA = P(A) (= Aの部分集合全体)

または

TA = P(A)_fin (= Aの有限部分集合全体)

と考える。

プログラム	意味
7	{7}
randwalk(5)	{4, 6}

あるいは load、store命令を持つ言語を考えてみる。
この言語では書き換え可能なメモリが用意されていて、x番地に入っている整数を返すload(x)と、x番地の値を整数aに書き換えるstore(x, a)を使うことができる。
この言語でのプログラム

load(1000)

の型はint型だけど、これも意味論上では領域ℤの特定の値として解釈するわけにはいかない。
このような言語については、メモリの状態が集合Sの要素で表されるとして、

TA = S→(A×S) (「メモリの状態」を入力して、「結果の値」と「実行後のメモリの状態」を返す関数)

として扱うことができる。

プログラム	意味
7	s →(7, s)
load(1000)	s → (s(1000), s)	※ s(1000) は、メモリの1000番地の値

さらに非決定計算と書き換え可能領域の両方を持っている言語では、

TA = S→(P(A)×S)

または

TA = S→(P(A)_fin×S)

とすればよい。
このように領域Aに加えて領域TAを考えることで、いろいろな種類の計算に対処できるようになる。

意味論で使う操作

プログラムの意味を考えるとき、プログラムの小さなパーツ(項とか式)の意味を合成して、より大きな部分の意味が決まっていく。プログラムの意味は集合の要素や関数で表されるので、意味を合成させるときには「関数を値(引数)へ適用する」や「関数の合成」が基本的な操作になる。
しかし今考えている意味論では、領域Aとは別に領域TAも導入されたので、通常の「関数の適用」「関数の合成」以外の操作が必要になる。
モッジは圏論に基づいた意味論を展開していくので、関数適用ではなく射の合成による定式化をしているのだけど、ここでは普通のプログラムとの繋がりを考えて圏論にこだわらずに関数適用中心の形で考える。
まず普通の関数適用と関数合成の型を考えると、次のようになっている(Haskellで対応する表記も書いておいた)。

	関数	要素	関数適用	Haskell		関数	関数	関数の合成	Haskell
型	A → B	A	B		型	B → C	A → B	A → C
値	f	a	f(a)	f a f $ a	値	g	f	g o f λx.(g(f(x))	g . f

TAとかTBのようにTのついた領域についても次のような場合は関数適用をおこなうことができる。

f : TA → TB
m : TA
⇒ f(m) : TB

しかし次のような場合、型が合っていないので関数適用はおこなえない。

f : A → TB
m : TA

しかしAとTAは別の型ではあるけれど、結果の型がAになる計算をTAで解釈しているので関連性は強い。そこでこのような型に対する関数適用(に類似の操作)を付け加える。そしてそれを2項演算「 f ◁ m 」と書いたり、関数適用と類似の見た目の「 f{m} 」と書くことにする。また

f : A → TB
g : B → TC

に対する関数合成(に類似した)演算を「 g◇f 」と書くことにする。ただし g◇f = λx.(g ◁ (f ◁ x)) が成り立つので実際に導入したのは「 ◁ 」だけと考えてよい。
新しく導入した操作の型は次のようになる。

	関数	要素	関数適用の類似	Haskell		関数	関数	関数合成の類似	Haskell
型	A → TB	TA	TB		型	B → TC	A → TB	A → TC
値	f	m	f ◁ m f{m}	f =<< m m >>= f	値	g	f	g ◇ f λx.(g ◁ (f ◁ x)) λx.(g{f{x}})	g <=< f f >=> g

「 ◁ 」は関数適用に類似した役目を果たすのだけれど、実際にどのような操作になるかはTAの定義次第。

例えば非決定性言語の場合 TA = P(A) で

f : A → TA ( = A → P(B) )
m : TA ( = P(A) )

に対して

f ◁ m ≡ ∪{f(x) | x∈m}　 (mの各要素に対してfを適用した計算結果(複数)を全て合わせる)

と定義できるし、load、store付き言語での TA =「S→(A×S)」の場合

f : A→TB ( = A→(S→(B×S)) )
m : TA ( = S→(A×S) )
f ◁ m ≡ λs₀.( let (a, s₁) = m(s₀) in f(a)(s₁) )

と定義できる(状態を表す値を受け取って、それを計算に使って、計算後の状態と計算結果を返すように定義する)。

「 ◁ 」を連鎖させた

… j ◁ i ◁ h ◁ g ◁ f ◁ m
…{j{i{h{g{f{m}}}}}

は関数適用(関数呼び出し)を連鎖させた

…(t(s(r(q(p(a)))))

と似てみえるけれど、関数適用を行うだけでなく、複数結果に対する扱いとか記憶状態の扱いといったことを裏でやっている。
ただし、そもそもモッジの論文には「 ◁ 」のような演算子は出てこない。モッジの論文は圏論に基づいて意味論を展開しているので、2項演算子ではなく射に対する操作「 ^* 」が用いられている。これは

f^*(m) = f ◁ m

が成り立つので同じようなものではあるけど、「 ^* 」は射f : A→TB に対して別の型の射 f^* : TA→TB を対応させる操作なところが違う。こちらを使うと関数合成に類似の操作は「 g◇f ≡ g^*o f 」と定義できる。
この「f^*」は、Haskell ではセクションを使った「 (f=<<) 」に対応する。
それから、関数適応(の類似)「 ◁ 」の他に、A型の値をTA型に変換する操作

η_A : A → TA

が導入される。これも実際にどんな操作になるかはTAの定義次第だけど、Aのときの情報をなるべく保ったままTAに変換する操作だと考えられる。
例で出した非決定性言語なら「 η(a) ≡ {a} 」となり、load、store付き言語なら「 η(a) ≡ λs.(s,a)) 」となるだろう。
また、この「 η 」と「 ◁ 」を使うと

f : T(A→B)
m : TA

からTB型の値を得る操作(「◁」のときとは型が違う)が次のように定義できる(見やすさのために「◁」の引数の順番を入れ替えた「▷」を使った)。

f ◀ m ≡ f ▷(λf₀. m▷(λm₀. η(f₀(m₀))))

これはHaskellにおける「 ap 」「 <*> 」にあたる。

モナド則

以上のように「 η 」と「 ◁ 」(あるいは「 η 」と「 ^* 」)が導入された。これらが具体的にどのような操作なのかは個々の場合に応じて違うのだけど、共通している部分もある。
外から見る限り、「 η_A 」はAのときの情報を保存したままTAに変換する操作のように見え、「 ◁ 」は関数適用に類似した操作のように見える(実際には関数適用を行っていなかったり関数適用以外の操作をしているかもしれないけれど、外側からは関数適用っぽく見える)。
このことをより形式的に表したのが、いわゆるモナド則になる(モッジはそう呼んでなくてクライスリ・トリプルの性質と呼ばれる)。論文では当然ながら圏論的な形で表示しているけど、ここでは他の形でも表示してみる。
「関数適用を使った表示」と「普通の関数で類似した式」を比べると、「 η 」が恒等関数idと類似の振る舞い(情報を保存して変換)をして「 ◁ 」が関数適用と類似した振る舞いをすることを表していると読める。

圏論的な表示	Haskell での表示	関数適用を使った表示	普通の関数で類似した式
ηA* = idTA	(return=<<) ≡ id	ηA{m} = m	id(x) = x
f* o ηA = f	(f=<<) . return ≡ f	f{ηA(x)} = f(x)	f(id(x)) = f(x)
g* o f* = (g* o f)*	(g=<<) . (f=<<) ≡ (((g=<<).f) =<<)	g{f{m}} = (g◇f){m}	g(f(x)) = (g o f)(x)
	return =<< m ≡ m	ηA ◁ m = m	id $ x = x
	f =<< return x ≡ f(x)	f ◁ ηA(x) = f(x)	f $ id(x) = f(x)
	g =<< f =<< m ≡ (g=<<).f =<< m	g ◁ f ◁ m = (g◇f) ◁ m	g $ f $ m = (g . f) $ m

do記法とlet構文の類似が、「 f ◁ m 」と関数適用「 f(a) 」の類似に由来していることも分かる。

do記法	let構文
(λx. ・・・) ◁ m (λx. ・・・){m}	(λx. ・・・)(a)
↓(do記法に書き換え)	↓(let構文に書き換え)
do { x <- m ; ・・・}	let x = a in ・・・

M. Spivey "A Functional Theory of Exceptions" (1990)

モッジの論文がプログラムの意味論でモナドを使っていたのに対して、実際のプログラムとの関連でモナドに言及した最初のものがおそらくスパイビーの論文になる。
スパイビーの論文はワドラーの「How to Replace Failure by a List of Successes」(1985)で述べられた手法を踏まえてそれを発展・改良したものになっている。ワドラーの論文では、例外やバックトラックの起きうる関数の戻り値をリスト型にして例外や探索失敗を空リストで表すという手法が遅延評価関数型言語で有効に使えることが述べられている。そのワドラーの手法を、高階関数を系統的に使って推し進めるというのがスパイビーの論文の趣旨(ただしリスト型よりも主にMaybe型を使って論じている)。
そこで使われている(α→β)→(Maybe α→ Maybe β)型の演算子「 ● 」(リストに対する「map」の類似演算)が、モナドの三つ組(T、μ、η)での関手Tにあたり(Haskellでの「fmap」にあたる)、論文の終わり近くでμ、ηにあたる関数(Haskellの「join」と「return」)が定義され、それらがモナドの性質を満たすことが述べられる。またリストの演算についても(T、μ、η)との対応が述べられる。(他には論文に出てくる演算子「 ? 」が、 MonadPlusクラスの「mplus」、Alternativeの「 <|> 」にあたっている)。

P. Wadler "The Essence of Functional Programming" (1992)

モッジとスパイビーの論文を受けて、ワドラーによってモナドについての論文(共著ふくむ)が多く書かれることになる。
最初に書かれた「Comprehending Monads」(1990、改訂版1992)ですでにモナドの典型的な使用例の多くが説明されているけれど、一方で「fmap」「join」「unit」を基本演算に使い、さらにリスト内包表記をモナドに一般化したものを導入して用いているので、現在のモナドを使ったプログラムとはかなり違った雰囲気がある。
次の「The Essence of Functional Programming」(1992)になると、基本演算が「unit」と「bind」(Haskellの「return」と「>>=」、この文章での「 η」と「▷」)になり、基本の枠組みが定まっている。またdo記法についてもすでに可能な専用構文として言及されている。名前はdoでなくletMだけど。

きれいな値と汚い値

「The Essence of Functional Programming」は「Shall I be pure or impure?」という文から始まる。
ところでワドラーには「Call-by-Value is Dual to Call-by-Name」(2003)、「Call-by-Value is Dual to Call-by-Name, Reloaded」(2005)という論文がある。「The Essence of …」の続編がもし書かれるなら、タイトルは「The Essence of Functional Programming, RePure」だろうか。
モッジがAとTAを「値」と「計算」と呼んで対比させたのと比較すると、ワドラーの論文でのAとTAは、値と計算の区別というよりも、関数型プログラミングにとって純粋きれいなものがAで汚いものがTAという対比として見ることができる。
ここで汚いというのは、次のようなこと。

• 関数が、引数以外によって外部から影響を受けたり、戻り値を介さず外部へ影響を与えている(参照透明性を破っている)。 例:大域的な状態の変更、関数内からログの記録をする、関数の挙動を外部から変更する、など。
• ある関数呼び出しの結果の影響が、制御の流れに広い範囲で波及する。例:探索の失敗やエラーがあったら、標準の計算の流れを順次飛ばしていく(大域ジャンプや例外機構を使いたくなる状況)。解に複数の候補があり探索が失敗したら別の候補がある場所まで戻って新たに計算する(バックトラック)、など。(例外については参照透明性の観点からも面倒。cf. S. Peyton Jones et al.「A Semantics for Imprecise Exceptions」(1999))

これらのことは、

• ある関数の関数適用(関数呼び出し)の挙動・影響が局所化しておらず、広い範囲について影響を与えたり受けたりする。

とまとめることもできる。(cf. 「関心の局所化と静的な記述」)
純粋な計算を「→」で、汚い計算を「⇒」で表すと、全てが純粋な計算は次のような関数適用の連鎖になる。

A → B → C → D → … → Y → Z

しかし、大域的な変数の変更や参照があるプログラムは、

A → B ⇒ C → D → … → Y ⇒ Z

のようになるし(⇒の部分で大域状態を書き換えたり読み込んだりしている)、途中で失敗したり複数の可能性がある探索をおこなうプログラムは、

A → B → C ⇒ D ⇒ … ⇒ Y ⇒ Z

になったりする(四角カッコで囲まれた部分のどこかで失敗したらそこから先は計算せずに飛ばしたり、バックトラックで戻ったりする)。
汚い計算は純粋関数型言語でも扱うことはできる。例えばエラーや失敗は関数呼び出しごとに逐次チェックすればよい。また大域状態の参照・変更は、大域状態にあたる値を引数・戻り値として渡していけばよい。つまりA→B型の関数にさらに大域状態にあたる引数・戻り値を追加して(A×S)→(B×S)型またはカリー化させてA→(S→(B×S))型とすれば大域的な状態を扱うことができる。ただしこうした引数・戻り値の扱いを色々な関数に対して広い範囲で繰り返し行う必要がある。
これに対するワドラーの考えの基本は、汚い計算をおこなう関数の型を A→B から A→TB にする、というもの(2.1節)。
つまり純粋関数型言語で扱いにくい汚い計算「A⇒B」を、関数型言語内では「A→TB」型の関数として扱う。もともと純粋関数型言語内で扱えた計算はunit(return、η)によって汚い計算の領域に持っていくことができるので、あとはTA型の値とA→TB型の関数に対して、bind( >>=、▷)で関数適用を繰り返していけば、汚い計算を純粋関数型言語の中で系統的に扱うことができることになる。

TA → TB → TC → TD → … → TY → TZ

こうした計算の様子の例をdo記法で書けば、例えば

do b <- 汚い計算(a)
   c <- return 純粋な計算(b)
   d <- 汚い計算(c)
   ⋮
   y <- 汚い計算(x)
   汚い計算(y)

みたいに表せる。

きれいな関数と汚い値 (Applicative)

ワドラーが(そしてモッジが)主に扱っていたのはA→TB型の関数(射)だったけれど、その代わりに

純粋な関数 f : A→B
汚い値 m : TA

の組み合わせで関数適用することを考える。この場合、複数のやり方がある。

• fをη(return)と関数合成して (ηo f) : A→TB 、それに「 ◁ 」( =<< )を使う。 (η o f) ◁ m 、  (η o f){m}
• η(return、pure)をfに適用させて η(f) : T(A→B)、それに「 ◀ 」(ap、<*>)を使う。 η(f) ◀ m 、  η(f)[m]
• 関手T(fmap)をfに適用させて T(f) : TA→TB、それに普通の関数適用をおこなう。  T(f)(m)

これらはどれを使っても同じ結果で、見た目もそんなに違わない。
これが引数が増えて、

f : A₁→A₂→…→A_n→B
m₁ : TA₁ 、 m₂ : TA₂ 、 …、 m_n : TA_n

になると

• m₁ ▷ (λx₁. m₂ ▷ (λx₂. … m_n▷ (λx_n.η(f x₁ x₂ … x_n)…))
  またはdo記法で、 do{x₁ <- m₁; x₂ <- m₂; …; x_n <- m_n; return (f x₁ x₂ … x_n)}
• 「 ◀ 」を左結合として η(f) ◀ m₁ ◀ m₂ … ◀ m_n 、  η(f)[m₁][m₂]…[m_n]

となって、「 ◀ 」を使った方が簡潔に書ける(関手Tを使った場合、T(f)を最初の引数に適用した所で「◀」を使う形に帰着する)。
この

「 ◀ 」と「η」 (「<*>」と「pure」)

は、モナドの基本演算

「 ◁」と「η」 (「=<<」と「return」)

よりも弱いのだけど(「◁」「η」から「◀」は定義できるが、「◀」「η」から「◁」は定義できない)、これを基本演算にするのがApplicative(C.McBride、R. Paterson「Applicative Programming with Effects」(2008))

S. Peyton Jones、P. Wadler "Imperative Functional Programming" (1993)

モナドの枠組みを用いることによって、普通に書こうとすると参照透明性を破るようなプログラムを純粋関数型言語内で系統的に扱うことができるようになった。しかし入出力についてはそれだけではダメでもう少し工夫が必要になる。「Comprehending Monads」や「The Essence of Functional Programming」でも入出力について扱われているけれど、入出力を文字列データにマッピングして扱っていて、実際の入出力を扱っている訳ではない。
ペイトン・ジョーンズ、ワドラーの「Imperative Functional Programming」で、遅延評価機構の枠内で入出力の順序を制御しそれをモナドで包んで隠す手法が提案され、モナドによって入出力が扱えるようになる。

ここまでの内容は、アイドルの子が筒井康隆『モナドの領域』を雑誌掲載時(単行本になる前)に読んでいるのを知ったのをきっかけに書き出したものなので(モナド違い)、結論とかは特にない。