「モナド (プログラミング)」の版間の差分

削除された内容追加された内容

インライン

2014年12月30日 (火) 15:49時点における版

計算機科学におけるモナド（英: Monad）とは、計算機科学者のEugenio Moggiによって提案されたモジュール性を持たせた表示的意味論の枠組みを言う^[1]。プログラムとはクライスリ圏の射である（a program is an arrow of a Kleisli category）、という要請^[2]から合成規則としてクライスリトリプル(Kleisli triple)というモナドと等価^[3]なものが用いられる。型システムへの適用であるプログラミング言語のHaskellで用いられるものがよく知られている。

モナドの名称は、圏論のモナド（モノイド＋トライアド）に基づく。なお、圏論のモナドはライプニッツのモナド（単子論）から命名された。

概要

"プログラム"の圏とクライスリ圏（categories of "programs" and Kleisli categories）

プログラミングの教則として、引数と返り値をもつことからプログラム（program）とは数学の関数、すなわち集合写像（mapping）であると教えられることがある。
しかしながらこの喩えは

入出力等をもたらすプログラム
例外を返すプログラム
引数に対して値を返さない（停止しない）プログラム
同じ引数でも返り値が異なる可能性のあるプログラム

などを説明することができない。つまり、プログラムは集合写像ではない（a program is NOT a mapping）^[4]。
プログラム（program）の数学的モデルを見つけ出す過程において、Moggi は圏論と表示的意味論の観点からプログラムは圏の射、型は圏の対象とみなすことができ^[5]、さらに直感的解釈として、関数が値を取り値を返すものであるのに対しプログラムが値を取り計算した値を返す^[6]、すなわち引数の型と返り値の型の間にはなにか違いがあり単純な射の合成ができない、と考えた。

集合写像（関数）：値　→　　　　　　　値

プログラム　　　：値　→　"計算した"　値

Moggi はこのような射としてのプログラムの数学的モデルとしてクライスリ圏（Kleisli category）の射が妥当であると主張し^[7]実際に副作用、例外処理、非決定計算などの効果^[8]をうまくクライスリ圏の枠組みで統一的に定式化できることを示した。
そういった壮大な背景をもつ理論であるが、実用上重要であるのは『引数と返り値の型がデータとして同一であっても合成することができず、クライスリトリプルに由来した合成規則を用いなくてはならない』という点である。

モジュール性を持たせた表示的意味論（modular denotational semantics）

対象言語の各項の意味をその対象言語を語るメタ言語^[9]の値に割り当てる表示的意味論はプログラミング言語の理論の中でも重要な手法の一つであるが、伝統的な表示的意味論は言語機能のモジュール性と拡張性が欠如しており^[10]、実際の実装及び実装したプログラミング言語の機能追加を行う際に既存コードの大幅な修正・設計の大幅なやり直しなどの困難をもたらす。Moggi のプログラムをクライスリ圏の射とみなすモナドの理論は、言語の一つの特徴的機能を自由に組合せ可能な一つのモジュールとする実装方式^[11]を与え、分割統治不可能であった言語の実装を分割統治可能なものにする^[12]。

計算の概念と計算効果（notions of computation and computational effects）

Moggi の理論の骨子は、『型 A の値（values of type A）』と『計算によって得られた型 A の値（computations of type A）』を明確に区別することにある^[13]。すなわち、副作用、例外処理、非決定計算などの計算方式でその計算効果（computational effects）を伴いつつ計算によって得られた型 A の値は、型を引数にとる型構築子 T を型 A に適用した新たな型 T A の値として表現するのである（Moggiの原理）^[14]。

Moggi の原理（Moggi's principle）^[15]

計算によって得られた型 A の値（computations of type A）は、型 T A の値に対応する

（Computations of type A correspond to values of type T A.）

なお、このときこの型構築子 T を計算の概念（a notion of computation）と呼ぶ^[16]。

プログラムの概念とその合成に関する問題点（a notion of programs and the problem of composition）

計算の概念の導入により、引数を取りつつ計算効果を伴った上で計算した値を返すものであるプログラム（program）の概念は次のように特徴付けることができるようになる。

Moggi が（暗黙的に）主張するプログラムの概念: 型 A の引数を取り T の計算効果を伴いつつ計算をした型 B の値を返すプログラム（program）とは、A → T B の型を持つものである^[17]。

このように特徴付けることによって計算効果を伴うプログラムとなんら計算効果を持たない単なる集合写像（関数）を分類することが可能となる。しかしながら、プログラムをこのように定式化すると大きな問題が発生することがわかる。すなわち、２つのプログラムの合成を単純に行うことができなくなってしまうのである。

例えば、program1 :: A → T B と program2 :: B → T C が与えられたとき、その合成を行おうと思っても、型 B というデータの型としての共通性はあっても計算の概念の分だけ型に違いがあるため、実際にプログラムの合成を行うことはできない。

program2 :: B → T C × program1 :: A → T B （合成不可）

この致命的な問題点を解消するために導入されるのがクライスリトリプル（Kleisli triple）である。

「クライスリ圏#クライスリトリプル（Kleisli triple）」も参照

直感的な記法となるが、クライスリトリプル（T,η, _^*）が与えられれば、「_^*」演算子の機能からprogram2^* :: T B → T C となり

program2^* . program1 :: A → T C （合成可能）

という形でプログラムの合成が可能となる。おおよそこのような理由から Moggi はクライスリ圏の射とプログラム（program）とは対応するものであるとした^[18]。

クライスリ圏に合致する計算の概念（notions of computation which suit Kleisli categories）

Moggi はクライスリ圏を構成する計算の概念として以下の計算効果を挙げている^[19]。

部分性（partiality）: T A = A_⊥（= A + { ⊥ }）; η_A は A から A_⊥ の中への包含（inclusion）; f : A -> T B であれば、f^*(⊥) = ⊥ 、f^*(a) = f(a) ただし、a ∈ A
非決定性（nondeterminism）^[20]: T A = P_fin(A); η_A は単要素（singleton）写像 a ↦ {a}; f : A -> T B かつ c ∈ T A であれば、f^*(c) = ∪_{x ∈ c}f(x)
副作用（side-effects）: T A = (A × S)^S; η_A は写像 a ↦ (λs: S.<a,s>); f : A -> T B かつ c ∈ T A であれば、λs:S.(let <a, s'> = c(s) in f(a)(s'))
例外（exceptions）^[21]: T A = A + E; η_A は入射（injection）写像 a ↦ inl(a); f : A -> T B であれば、f^*(inr(e)) = e (ただし、e ∈ E) かつ f^*(inl(a)) = f(a) (ただし、a ∈ A)
継続（continuations）: T A = R^{(R^A)}; η_A は写像 a ↦ (λk: R^A. k(a)); f : A -> T B かつ c ∈ T A であれば、f^*(c) = (λk: R^B .c(λa: A.f(a)(k)))

多階層化インタプリタ（stratified interpreter）

脚注

^ 佐伯(2001) p.11
^ Moggi(1991) p.3
In order to justify the axioms for a Kleisli triple we have first to introduce a category C_T whose morphisms correspond to programs.

※ここで圏 C_T はクライスリ圏（定義1.3）
他蓮尾(2011)
^ 尾上(2006) p.306
^ つまり、Set もしくは Ens の普通の射ではない。
^ Moggi(1989)a p.17
^ Moggi(1989)a p.17
3.2.1 A justification for monads

In order to justify the use of monads for modelling notions of computations we adopt the following intuitive understanding of programs: a program is a function from values to computations.
^ Moggi(1989)a p.18
^ 計算効果（computational effects）と呼ばれる。Filinski(1994)、勝股(2011)
^ メタ言語としては、プラトン主義的にしか存在し得ない完全な言語としての数学でなければならないかのような説明が一部でされることもあるが、そのような必然性は特に無く、対象言語を意味づけるに十分な形式言語（プログラミング言語）であればよい。
^ Liang,Hudak pp.1-2
^ このモジュールのことをモナド（monad）、計算（computation）などと呼ぶこともある。
^ Wadler(1992), Espinosa(1995)
^ 参照
1 A categorical semantics of computations

The basic idea behind the categorical semantics below is that, in order to interpret a programming language in a category C, we distinguish the object A of values (of type A) from the object TA of computations (of type A), and take as denotations of programs (of type A) the elements of TA. In particular, we identify the type A with the object of values (of type A) and obtain the object of computations (of type A) by applying an unary type-constructor T to A. We call T a notion of computation, since it abstracts away from the type of values computations may produce. There are many choices for TA corresponding to different notions of computations.
Moggi(1991) pp.2-3
^ なお、Moggi はプログラミング言語のML（MetaLanguage）のような型システムを持つ言語を前提に理論を展開している。
^ Filinski(1994) p.447
^ Moggi(1991) p.3
^ これは例えば入出力の効果をもたらす計算（入出力の計算効果）では、一例として、文字列 String 型の値を取り単位型 () を返し入出力の計算効果をもたらすプログラム putStrLn の型は（その計算効果を表す型名を T ではなく IO とすれば）
putStrLn :: String -> IO ()
となることを意味する。すなわち、
putStrLnプログラム：文字列の値 -> 入出力（IO）"計算した" 単位型の値
と把握されるものであるということである。なお、例えばプログラミング言語のHaskellにおいては、他にも、例外処理の計算効果であれば Error、継続（continuation）の計算効果であれば Cont などの型名が与えられている。
^ Moggi(1989)a pp.17-18
^ Moggi(1991) pp.4-5
^ プログラミング言語のHaskellにおいてはリストモナドとして知られる。
^ HaskellにおいてはMaybeモナドとして知られる。inr(e) = Nothing、inl(a) = Maybe a

参考文献

第５章３節『関数とはなにか』において、圏Set（もしくは Ens）の普通の射に計算（computation）概念は全く含まれていないことが確認できる。

David Espinosa (1995), Semantic Lego

モナドを用いたモジュラーな意味論を採用することでレゴブロックを組み立てるように言語を組み立てることができることを実証した。

[1] 佐伯(2001) p.11

[2] Moggi(1991) p.3
In order to justify the axioms for a Kleisli triple we have first to introduce a category C_T whose morphisms correspond to programs.

※ここで圏 C_T はクライスリ圏（定義1.3）
他蓮尾(2011)

[3] 尾上(2006) p.306

[4] つまり、Set もしくは Ens の普通の射ではない。

[5] Moggi(1989)a p.17

[6] Moggi(1989)a p.17
3.2.1 A justification for monads

In order to justify the use of monads for modelling notions of computations we adopt the following intuitive understanding of programs: a program is a function from values to computations.

[7] Moggi(1989)a p.18

[8] 計算効果（computational effects）と呼ばれる。Filinski(1994)、勝股(2011)

[9] メタ言語としては、プラトン主義的にしか存在し得ない完全な言語としての数学でなければならないかのような説明が一部でされることもあるが、そのような必然性は特に無く、対象言語を意味づけるに十分な形式言語（プログラミング言語）であればよい。

[10] Liang,Hudak pp.1-2

[11] このモジュールのことをモナド（monad）、計算（computation）などと呼ぶこともある。

[12] Wadler(1992), Espinosa(1995)

[13] 参照
1 A categorical semantics of computations

The basic idea behind the categorical semantics below is that, in order to interpret a programming language in a category C, we distinguish the object A of values (of type A) from the object TA of computations (of type A), and take as denotations of programs (of type A) the elements of TA. In particular, we identify the type A with the object of values (of type A) and obtain the object of computations (of type A) by applying an unary type-constructor T to A. We call T a notion of computation, since it abstracts away from the type of values computations may produce. There are many choices for TA corresponding to different notions of computations.
Moggi(1991) pp.2-3

[14] なお、Moggi はプログラミング言語のML（MetaLanguage）のような型システムを持つ言語を前提に理論を展開している。

[15] Filinski(1994) p.447

[16] Moggi(1991) p.3

[17] これは例えば入出力の効果をもたらす計算（入出力の計算効果）では、一例として、文字列 String 型の値を取り単位型 () を返し入出力の計算効果をもたらすプログラム putStrLn の型は（その計算効果を表す型名を T ではなく IO とすれば）
putStrLn :: String -> IO ()
となることを意味する。すなわち、
putStrLnプログラム：文字列の値 -> 入出力（IO）"計算した" 単位型の値
と把握されるものであるということである。なお、例えばプログラミング言語のHaskellにおいては、他にも、例外処理の計算効果であれば Error、継続（continuation）の計算効果であれば Cont などの型名が与えられている。

[18] Moggi(1989)a pp.17-18

[19] Moggi(1991) pp.4-5

[20] プログラミング言語のHaskellにおいてはリストモナドとして知られる。

[21] HaskellにおいてはMaybeモナドとして知られる。inr(e) = Nothing、inl(a) = Maybe a

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

@@ 1行目: / 1行目: @@
-[[計算機科学]]における'''モナド'''とは、[[関数型言語]]において[[参照透過性]]を維持しつつ[[手続き型プログラミング|手続き型]]的な記述を行なうための枠組みを言う。主に[[プログラミング言語]][[Haskell]]で用いられる。
+[[計算機科学]]における'''モナド'''（{{lang-en-short|Monad}}）とは、計算機科学者の[[:en:Eugenio Moggi|Eugenio Moggi]]によって提案された[[モジュール]]性を持たせた[[表示的意味論]]の枠組みを言う<ref>[[#佐伯(2001)|佐伯(2001)]] p.11</ref>。'''プログラムとはクライスリ圏の射である（a program is an arrow of a Kleisli category）'''、という要請<ref>[[#Moggi(1991)|Moggi(1991)]] p.3
+:In order to justify the axioms for a Kleisli triple we have first to introduce a category C<sub>T</sub> '''whose morphisms correspond to programs'''.
+:<small>※ここで圏 C<sub>T</sub> はクライスリ圏（定義1.3）</small>
+他 [[#蓮尾(2011)|蓮尾(2011)]]
+</ref>から合成規則としてクライスリトリプル(Kleisli triple)というモナドと等価<ref>[[#尾上(2006)|尾上(2006)]] p.306</ref>なものが用いられる。型システムへの適用である[[プログラミング言語]]の[[Haskell]]で用いられるものがよく知られている。
+モナドの名称は、[[圏論]]の[[モナド (圏論)|モナド]]（モノイド＋トライアド）に基づく。なお、圏論のモナドは[[ゴットフリート・ライプニッツ|ライプニッツ]]の[[モナド (哲学)|モナド]]（単子論）から命名された。
-元来は[[入出力|I/O]]等の[[副作用 (プログラム)|副作用]]を伴う処理や、順序処理を自然に記述するために導入された。後に様々な領域でモナド形式による表現の有用性が発見され、現在では「モナド化」はHaskellプログラミング全般に強力な理論基盤を与えている。
+== 概要 ==
-モナドの名称は、[[圏論]]の[[モナド (圏論)|モナド]]（モノイド＋トライアド）に基づいており、[[ゴットフリート・ライプニッツ|ライプニッツ]]の[[モナド]]（単子論）とは無関係である。
+==="プログラム"の圏とクライスリ圏（categories of "programs" and Kleisli categories）===
+プログラミングの教則として、引数と返り値をもつことからプログラム（program）とは数学の関数、すなわち集合写像（mapping）であると教えられることがある。<br />
+しかしながらこの喩えは
+* 入出力等をもたらすプログラム
+* 例外を返すプログラム
+* 引数に対して値を返さない（停止しない）プログラム
+* 同じ引数でも返り値が異なる可能性のあるプログラム
+などを説明することができない。つまり、'''プログラムは集合写像ではない（a program is NOT a mapping）'''<ref>つまり、'''Set''' もしくは '''Ens''' の普通の射では'''ない'''。</ref>。<br />
+プログラム（program）の数学的モデルを見つけ出す過程において、Moggi は[[圏論]]と表示的意味論の観点からプログラムは圏の射、型は圏の対象とみなすことができ<ref>[[#Moggi(1989)a|Moggi(1989)a]] p.17</ref>、さらに直感的解釈として、関数が値を取り値を返すものであるのに対しプログラムが値を取り'''計算した 値'''を返す<ref>[[#Moggi(1989)a|Moggi(1989)a]] p.17
+;3.2.1 A justification for monads
+:In order to justify the use of monads for modelling notions of computations we adopt the following intuitive understanding of programs: '''a program is a function from values to computations.'''
+</ref>、すなわち引数の型と返り値の型の間にはなにか違いがあり単純な射の合成ができない、と考えた。<br />
+:集合写像（関数）：値　→　　　　　　　値
+:プログラム　　　：値　→　"計算した"　値
+Moggi はこのような射としてのプログラムの数学的モデルとして'''クライスリ圏（Kleisli category）の射'''が妥当であると主張し<ref>[[#Moggi(1989)a|Moggi(1989)a]] p.18</ref>実際に副作用、例外処理、非決定計算などの効果<ref>'''計算効果'''（computational effects）と呼ばれる。[[#Filinski(1994)|Filinski(1994)]]、[[#勝股(2011)|勝股(2011)]]</ref>をうまくクライスリ圏の枠組みで統一的に定式化できることを示した。<br />
+そういった壮大な背景をもつ理論であるが、実用上重要であるのは『引数と返り値の型が'''データとして'''同一であっても合成することができず、クライスリトリプルに由来した合成規則を用いなくてはならない』という点である。
+===モジュール性を持たせた表示的意味論（modular denotational semantics）===
-==概要==
+対象言語の各項の意味をその対象言語を語るメタ言語<ref>メタ言語としては、プラトン主義的にしか存在し得ない完全な言語としての数学でなければならないかのような説明が一部でされることもあるが、そのような必然性は特に無く、対象言語を意味づけるに十分な形式言語（プログラミング言語）であればよい。</ref>の値に割り当てる表示的意味論はプログラミング言語の理論の中でも重要な手法の一つであるが、伝統的な表示的意味論は言語機能のモジュール性と拡張性が欠如しており<ref>[[#Liang,Hudak|Liang,Hudak]] pp.1-2</ref>、実際の実装及び実装したプログラミング言語の機能追加を行う際に既存コードの大幅な修正・設計の大幅なやり直しなどの困難をもたらす。Moggi のプログラムをクライスリ圏の射とみなすモナドの理論は、言語の一つの特徴的機能を自由に組合せ可能な一つのモジュールとする実装方式<ref>このモジュールのことをモナド（monad）、計算（computation）などと呼ぶこともある。</ref>を与え、分割統治不可能であった言語の実装を分割統治可能なものにする<ref>[[#Wadler(1992)|Wadler(1992)]], [[#Espinosa(1995)|Espinosa(1995)]]</ref>。
-[[遅延評価]]をデフォルトでもつ純粋関数型言語では、実際の処理がどのタイミングで行なわれるのか予測することが難しく、またシステムの状態を保持して処理の流れを変えるような記述は困難である。
+== 計算の概念と計算効果（notions of computation and computational effects） ==
-モナドでは処理手順と型を構造化することで、局所的に手続き型に近い記述形式を導入し、自然な形で副作用や順序処理を埋め込んでいる。
+Moggi の理論の骨子は、『型 A の値（values of type A）』と『計算によって得られた型 A の値（computations of type A）』を明確に区別することにある<ref>参照
+;1 A categorical semantics of computations
+:The basic idea behind the categorical semantics below is that, in order to interpret a programming language in a category C, we distinguish the object A of values (of type A) from the object TA of computations (of type A), and take as denotations of programs (of type A) the elements of TA. In particular, we identify the type A with the object of values (of type A) and obtain the object of computations (of type A) by applying an unary type-constructor T to A. We call T a notion of computation, since it abstracts away from the type of values computations may produce. There are many choices for TA corresponding to different notions of computations.
+[[#Moggi(1991)|Moggi(1991)]] pp.2-3
+</ref>。すなわち、副作用、例外処理、非決定計算などの計算方式でその'''計算効果'''（computational effects）を伴いつつ計算によって得られた型 A の値は、型を引数にとる型構築子 T を型 A に適用した新たな型 T A の値として表現するのである（Moggiの原理）<ref>なお、Moggi はプログラミング言語の[[ML (プログラミング言語)|ML（MetaLanguage）]]のような型システムを持つ言語を前提に理論を展開している。</ref>。
+{{Quotation|
+;Moggi の原理（Moggi's principle）<ref>[[#Filinski(1994)|Filinski(1994)]] p.447</ref>
+:計算によって得られた型 A の値（computations of type A）は、型 T A の値に対応する
+:（Computations of type A correspond to values of type T A.）
+}}
+なお、このときこの型構築子 T を'''計算の概念'''（a notion of computation）と呼ぶ<ref>[[#Moggi(1991)|Moggi(1991)]] p.3</ref>。
+=== プログラムの概念とその合成に関する問題点（a notion of programs and the problem of composition） ===
+計算の概念の導入により、引数を取りつつ計算効果を伴った上で計算した値を返すものである'''プログラム'''（program）の概念は次のように特徴付けることができるようになる。
+;Moggi が（暗黙的に）主張するプログラムの概念
+:型 A の引数を取り T の計算効果を伴いつつ計算をした型 B の値を返すプログラム（program）とは、<code>A → T B</code> の型を持つものである<ref>これは例えば入出力の効果をもたらす計算（入出力の計算効果）では、一例として、文字列 String 型の値を取り単位型 () を返し入出力の計算効果をもたらすプログラム putStrLn の型は（その計算効果を表す型名を T ではなく IO とすれば）
+:<code>putStrLn :: String -> IO ()</code>
+となることを意味する。すなわち、
+:putStrLnプログラム：文字列の値 -> 入出力（IO）"計算した" 単位型の値
+と把握されるものであるということである。
+なお、例えばプログラミング言語のHaskellにおいては、他にも、例外処理の計算効果であれば <code>Error</code>、継続（continuation）の計算効果であれば <code>Cont</code> などの型名が与えられている。</ref>。
-言語が参照透過性を保つ限り、どこかに格納された値を書き換える事は不可能であるが、逆に言えば、どこにも格納されていない値であればどんな数値を取っても良い事になる。関数型言語でこれに適合するのは関数のリターンである。都合の良い事に、関数のリターンは必ず内部で呼び出した関数が全て終了してから行われるため、下位→上位というリターンの順序が崩れる事もない。
+このように特徴付けることによって計算効果を伴うプログラムとなんら計算効果を持たない単なる集合写像（関数）を分類することが可能となる。しかしながら、プログラムをこのように定式化すると大きな問題が発生することがわかる。すなわち、'''２つのプログラムの合成を単純に行うことができなくなってしまうのである'''。
+例えば、<code>program1 :: A → T B</code> と <code>program2 :: B → T C</code> が与えられたとき、その合成を行おうと思っても、型 B というデータの型としての共通性はあっても計算の概念の分だけ型に違いがあるため、実際にプログラムの合成を行うことはできない。
-この性質を利用し、順序処理を関数の入れ子に、また関数自体の値と平行して副値を走らせることで「副作用」をパッケージ化するというのがモナドのコンセプトである。通常の文法の範囲内でもモナドと近い処理は可能だが、プログラムが非常に書きづらい形になるため実用的とは言い難い。
+:<code>program2 :: '''B''' → T C</code> × <code>program1 :: A → '''T B'''</code> （合成不可）
+この致命的な問題点を解消するために導入されるのが[[クライスリ圏#クライスリトリプル（Kleisli triple）|クライスリトリプル]]（Kleisli triple）である。
+{{see also|クライスリ圏#クライスリトリプル（Kleisli triple）}}
+直感的な記法となるが、クライスリトリプル（T,η, _<sup>*</sup>）が与えられれば、「_<sup>*</sup>」演算子の機能から<code>program2<sup>*</sup> :: T B → T C</code> となり
+:<code>program2<sup>*</sup> . program1 :: A → T C</code> （合成可能）
+という形でプログラムの合成が可能となる。おおよそこのような理由から Moggi は[[クライスリ圏]]の射とプログラム（program）とは対応するものであるとした<ref>[[#Moggi(1989)a|Moggi(1989)a]] pp.17-18</ref>。
+=== クライスリ圏に合致する計算の概念（notions of computation which suit Kleisli categories） ===
+Moggi はクライスリ圏を構成する計算の概念として以下の計算効果を挙げている<ref>[[#Moggi(1991)|Moggi(1991)]] pp.4-5</ref>。
+;部分性（partiality）
+:T A = A<sub>&perp;</sub>（= A + { &perp; }）
+:&eta;<sub>A</sub> は A から A<sub>&perp;</sub> の中への包含（inclusion）
+:f : A -> T B であれば、f<sup>*</sup>(&perp;) = &perp; 、f<sup>*</sup>(a) = f(a) ただし、a &isin; A
+;非決定性（nondeterminism）<ref>プログラミング言語のHaskellにおいてはリストモナドとして知られる。</ref>
+:T A = P<sub>''fin''</sub>(A)
+:&eta;<sub>A</sub> は単要素（singleton）写像 a &#x21a6; {a}
+:f : A -> T B かつ c &isin; T A であれば、f<sup>*</sup>(c) = &cup;<sub>x &isin; c</sub>f(x)
+;副作用（side-effects）
+:T A = (A &times; S)<sup>S</sup>
+:&eta;<sub>A</sub> は写像 a  &#x21a6; (&lambda;s: S.<a,s>)
+:f : A -> T B かつ c &isin; T A であれば、&lambda;s:S.(let <a, s'> = c(s) in f(a)(s'))
+;例外（exceptions）<ref>HaskellにおいてはMaybeモナドとして知られる。inr(e) = Nothing、inl(a) = Maybe a</ref>
+:T A = A + E
+:&eta;<sub>A</sub> は入射（injection）写像 a &#x21a6; inl(a)
+:f : A -> T B であれば、f<sup>*</sup>(inr(e)) = e (ただし、e &isin; E) かつ f<sup>*</sup>(inl(a)) = f(a) (ただし、a &isin; A)
+;継続（continuations）
+:T A = R<sup>(R<sup>A</sup>)</sup>
+:&eta;<sub>A</sub> は写像 a  &#x21a6; (&lambda;k: R<sup>A</sup>. k(a))
+:f : A -> T B かつ c &isin; T A であれば、f<sup>*</sup>(c) = (&lambda;k: R<sup>B</sup> .c(&lambda;a: A.f(a)(k)))
+<!--
+;対話的入力（interactive input） T A = (&mu;&gamma;.A + &gamma;<sup>U</sup>)
+;対話的出力（interactive output） T A = (&mu;&gamma;.A + (U &times; &gamma;))
+-->
+== 多階層化インタプリタ（stratified interpreter） ==
-{{DEFAULTSORT:もなと}}
+==関連項目==
-[[Category:関数型プログラミング]]
+* [[モジュール]]
+* [[インタプリタ]]
+* [[領域理論]]
+* [[圏論]] - [[クライスリ圏]]
+* [[ホモロジー代数]]
+* [[自己反映計算 (計算機科学)]]
+==脚注==
-{{Computer-stub}}
+<references />
+==参考文献==
-[[ca:Mònada (programació funcional)]]
+* {{citation | author=Eugenio Moggi | year=1989 | title=An abstract view of programming languages | url=http://www.disi.unige.it/person/MoggiE/ftp/abs-view.pdf | ref=Moggi(1989)a }}
-[[de:Monade (Typkonstruktion)]]
+* {{citation | author=Eugenio Moggi | year=1989 | title=Computational lambda-calculus and monads | url=http://www.disi.unige.it/person/MoggiE/ftp/lics89.pdf | ref=Moggi(1989)b }}
-[[en:Monad (functional programming)]]
+* {{citation | author=Eugenio Moggi | year=1991 | title=Notions of computation and monads | url=http://www.cs.cmu.edu/~crary/819-f09/Moggi91.pdf | ref=Moggi(1991) }}
-[[fi:Monadi (funktionaalinen ohjelmointi)]]
+* {{cite book|author=S. マックレーン | others=赤尾和男, 岡本周一共訳 | title = 数学 －その形式と機能－ | year = 1992 | publisher =  森北出版 | location = | isbn = 9784627018303 }}
-[[fr:Monade (informatique)]]
+:<small>第５章３節『関数とはなにか』において、圏'''Set'''（もしくは '''Ens'''） の普通の射に計算（computation）概念は全く含まれていないことが確認できる。</small>
-[[it:Monade (informatica)]]
+* {{citation | author=David Espinosa | year=1995 | title=Semantic Lego | url=http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.2885 | ref=Espinosa(1995)}}
-[[ru:Монада (программирование)]]
+:<small>モナドを用いたモジュラーな意味論を採用することでレゴブロックを組み立てるように言語を組み立てることができることを実証した。</small>
-[[uk:Монади (програмування)]]
+* {{citation | author=Sheng Liang , Paul Hudak |  title=Modular Monadic Semantics | url=http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.136.1656 | ref=Liang,Hudak}}
-[[zh:单子]]
+* {{citation | author=佐伯 豊 | year=2001 | title=再利用可能な拡張機構を備えた言語処理系 | url=https://dspace.jaist.ac.jp/dspace/bitstream/10119/908/3/1184paper.pdf | ref=佐伯(2001)}}
+* {{citation | author=尾上 能之 |year=2006 |  title=自分自身を出力するプログラム | url=http://www.ipsj.or.jp/07editj/promenade/4703.pdf | ref=尾上(2006) }}
+* {{citation | author=梅村 晃広 | year=1993 | title=モナドに基づく代数仕様の書換え | url=http://ci.nii.ac.jp/naid/110002929389}}
+* {{citation | author=勝股 審也| year=2011 | title=圏論の歩き方(第5回)モナドと計算効果 | ref=勝股(2011) }}
+* {{citation | author=蓮尾 一郎| year=2011 | title=圏論の歩き方(第6回)モナドのクライスリ圏 | ref=蓮尾(2011) }}
+* {{citation | author=Philip Wadler | title=The essence of functional programming | url=http://www.eliza.ch/doc/wadler92essence_of_FP.pdf | ref=Wadler(1992) }}
+* {{citation | author=Andrzej Filinski | year=1994 | title=Representing Monads | url=http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.43.8213 | ref=Filinski(1994) }}
+* {{citation | title=Haskell 98 Language and Libraries The Revised Report | editor=Simon Peyton Jones, Paul Hudak 他 | year=2002 | url=https://www.haskell.org/definition/haskell98-report.pdf | ref=report98 }}
+{{DEFAULTSORT:もなと}}
+[[Category:設計]]
+[[Category:プログラミング]]
+[[Category:ホモロジー代数]]
+[[Category:圏論]]
+[[Category:計算機科学]]