クリスマスですか。
何年か前にトム・レンスター（Tom Leinster）が「クリスマスにはトポスを勉強しよう」とか書いてましたが、トポスじゃなくてモナドの話。
Maybeモナド（オプション・モナド、付点モナドなどとも呼ぶ）はモナドのなかでも一番簡単なものでしょう。Maybeモナドと正実数の掛け算を組み合わせたモナドを定義してみます。
正実数の掛け算と一点追加によるモナド
R+ = {x∈R | x ＞ 0} とします。また、O = {0} とします。
集合Xに対して、X×R+ + O という対応を関手に拡張したものをFとします。詳しく書くと：
- FはSet上の自己関手。
- X∈|Set| に対して、F(X) := X×R+ + O
- f:X→Y in Set に対して、F(f:X→Y) := λz∈(X×R+ + O).(if (z∈X×R+) then z = (x, r) として (f(x), r) else 0)
このFは、集合R+を直積で掛け算する関手と、一点集合Oを直和で付け加える関手を組み合わせたものです。“1次”の多項式関手です。
自然変換 η::Id⇒F:Set→Set と μ::FF⇒F:Set→Set は次のように定義します。
- ηX:X→F(X) := λx∈X.(x, 1)
- μX:FF(X)→F(X) := λw∈(X×R+×R+ + O×R+ + O).(if (w∈X×R+×R+) then w = (x, r, s) として (x, rs) else 0)
直積として掛け算したR+が、正実数の掛け算でモノイドになっているので、そのモノイド乗法をつかってμを定義しています。追加したOに関してはMaybeモノイドと同じ処理です。
(F, μ, η)がSet上のモナドになることはすぐにわかります。モノイドR+によるモノイダル・スタンピング・モナドとMaybeモナドの組み合わせが(F, μ, η)です。興味がある方は、ベックの分配法則を確認して、2つのモナドの複合モナドとして(F, μ, η)を構成してみてください。
質量モナドと仲間たち
前節で定義したモナドを質量モナドと呼ぶことにします。そのココロは次のようなことです； 集合Xの要素達は互いに区別はできるが個性を持ってない点達です。この点に質量という属性を持たせることにします。質量を持った点の集まりがF(X)です。
もとの集合Xを位置（存在場所）の集合とみなして、位置xにあって質量rを持つ点は (x, r) と表されるので、X×R+ の要素です。追加した0は、位置も質量を持たない点、つまり空虚／無存在です。各位置ごとに質量ゼロの点が存在するという見方もあるかも知れませんが、ここでは、空虚は唯一です（存在しないモノが空間ごとにただ1つ存在する）。
質量モナドからクライスリ圏を作ってみると、クライスリ圏の射は、f:X→(Y×R+ + O) の形をしています。x∈X が、(y, s) のような要素に移れば、位置はxからyに移り、質量はs倍されたと考えます。xが消滅してしまう場合は、f(x) = 0 （0はOの要素）となります。プログラム理論の書き方では、0より⊥（ボトム）が使われますね。
話を簡単にするために、集合圏Setを舞台にしましたが、可測空間と可測写像の圏Measのほうが、質量モナドのベース圏にふさわしいような気がします。
質量モナドを考えた動機は、「集合圏Set vs. 可測圏Meas」の対応表を埋めるためです。「測度的積分核と随伴構造」で述べた測度的積分核は、行列と似てますが、関係（二項関係）とも似てます。次の表のような対応があるように思えます。
| ベース圏 | モナド | クライスリ圏 | 備考 |
|---|---|---|---|
| 集合圏 | Maybeモナド | 部分写像の圏 | 未定義を許す |
| 可測圏 | 質量モナド | 質量付き写像の圏 | 質量可変で未定義（消失）を許す |
| 集合圏 | ベキ集合モナド | 関係圏 | 射は{0, 1}係数行列 |
| 可測圏 | R+値ジリィ・モナド | 測度的積分核の圏 | 射はR+係数行列と類似 |
ジリィ・モナド（Giry monad）をちゃんと説明したことはないですが、関連箇所は：
別な形の表にすると：
| 集合圏ベース | 可測圏ベース |
|---|---|
| Maybeモナド | 質量モナド |
| ベキ集合モナド | R+値ジリィ・モナド |
「集合圏←→可測圏」とベース圏を対応させると、「Maybeモナド←→質量モナド」と対応しそうだということです。この対応の根拠はまだ弱いので、もっと証拠を揃えたいところです。
