この記事の目的は二つあります。一つめは、相対モナドの簡単で面白い例を提供すること。二つめは、図式順記法のプロモーションです。図式順記法を使えば気持ち良く計算が出来るよ、とアピールしたい。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\twoto}{\Rightarrow }
%\newcommand{\thrto}{\Rrightarrow }
\newcommand{\In}{\text{ in }}
\newcommand{\id}{\mathrm{id}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\bang}{\boldsymbol{!}}
\newcommand{\u}[1]{\underline{#1}}
%\newcommand{\o}[1]{\overline{#1}}
\newcommand{\hyp}{ \text{-} }
%\newcommand{\Iff}{ \Leftrightarrow }
%\newcommand{\Imp}{ \Rightarrow }
`$
内容:
※色付きテキストは次の約束で使います。
- 青い文字: 重要な概念・用語だがこの記事内では定義・説明してないもの。
- 赤い文字: この記事内で導入・定義した概念・用語。過去の定義の再掲・繰り返しのときもある。
- マゼンタの文字: この記事内の後方で定義されるか参照〈リンク〉される概念・用語。
相対モナド
相対モナドの定義は「相対モナドと集合係数の線形代数 // 相対モナド」に書いてあります。「アドホック随伴系は相対随伴系 // 相対モナド」にも説明があります。が、ここで定義と説明を(割と丁寧に)繰り返します。
相対モナド〈relative monad〉の構成素を三グループに分けます。基礎部分とオペレーター達と法則達です。基礎部分の構成素は:
- 圏 $`\cat{A}`$
- 圏 $`\cat{C}`$
- 関手 $`J: \cat{A} \to \cat{C}`$
これらは、相対モナドの土台となる部分です。関手 $`J`$ を、相対モナドのルート関手〈root functor〉と呼びます。$`J = \mrm{Id}_\cat{C}`$ (恒等関手)のとき、相対モナドは通常の $`\cat{C}`$ 上のモナドです。相対モナドは、通常のモナドとさほどの差はありません*1。
次にオペレーター達は:
- オペレーター $`T`$ 、相対モナドの台
- オペレーター $`\eta`$ 、相対モナドの単位
- オペレーター $`\mrm{Ext}`$ 、相対モナドのクライスリ拡張
ここで、「オペレーター」ってなんじゃい? って話になりますよね。「アドホック随伴系は相対随伴系 // 相対モナド」でも愚痴ってますが、関手や自然変換とはいえない対応付け/値割り当てに適切な呼び名がないんですよ。行き当たりばったりに、「コンストラクタ〈構成子〉」、「フォーマー〈形成子〉」、「オペレーター〈演算子〉」、「コンビネータ」、「モダリティ」、「サプライ」、「コネクティブ〈結合子〉」とか呼んでますが、広く合意された定義も基準もありません。定番の記述方法・記法も特にないので、一個ずつ個別に説明します。
あっ、「アドホック随伴系は相対随伴系 // 相対モナド」で、$`T`$ は関手で、$`\eta`$ は自然変換だと書いてます(脚注に言い訳ありです)が、オペレーターの説明がめんどくさかったからです。すんません。
圏 $`\cat{A}`$ の対象はラテン文字小文字 $`a, b`$ などで書くことにします(「アドホック随伴系は相対随伴系 // 相対モナド」でもそうしました)。
オペレーター $`T`$ は、$`\cat{A}`$ の対象に $`\cat{C}`$ の対象を割り当てます。
$`\text{For }a \in |\cat{A}|\\
\quad T(a) \in |\cat{C}|
`$
これは、$`|\cat{A}| \to |\cat{C}|`$ の関数〈写像〉なので、オペレーターとしては単純です。関数 $`T`$ を、相対モナドの台〈carrier | underlying operator〉と呼びます。$`T`$ は関手に仕立てられる*2ので、台関手〈underlying functor〉と呼ぶこともあります。
オペレーター $`\eta`$ は、$`\cat{A}`$ の対象に $`\cat{C}`$ の射を割り当てます。
$`\text{For }a \in |\cat{A}|\\
\quad \eta_a : J(a) \to T(a) \In \cat{C}
`$
$`\eta`$ は関数〈写像〉 $`\cat{A} \to \mrm{Mor}(\cat{C})`$ ではありますが、条件が付いていて $`\eta_a \in \cat{C}(J(a), T(a))`$ です。オペレーター $`\eta`$ を、相対モナドの単位〈unit〉と呼びます。
オペレーター $`\mrm{Ext}`$ は、$`\cat{A}`$ の対象のペアでインデックス付けられた関数〈写像〉の族で、$`\mrm{Ext}_{a, b}`$ は $`\cat{C}`$ の射に $`\cat{C}`$ の射を割り当てます。
$`\text{For }a, b \in |\cat{A}|\\
\text{For } f \in \cat{C}(J(a), T(b))\\
\quad \mrm{Ext}_{a, b}(f) : T(a) \to T(b) \In \cat{C}
`$
オペレーター $`\mrm{Ext}`$ を、相対モナドのクライスリ拡張オペレーター〈Kleisli extension operator〉と呼びます。用語(呼び名)の省略のパターンを列挙すれば:
- クライスリ拡張オペレーター
- クライスリ拡張
- 拡張オペレーター
- 拡張
- クライスリ・オペレーター
クライスリ拡張 $`\mrm{Ext}_{a, b}`$ が作用する相手〈オペランド〉である $`f: J(a) \to T(b)`$ の形の射をクライスリ射〈Kleisli morphism〉と呼びます。
なお、関数空間型(ブラケットで書く)とパイ型〈依存関数空間型〉を知っているなら、オペレーターの型(オペレーターが所属する集合)を以下のように記述できます。
$`\quad T \in [|\cat{A}| , |\cat{C}|]\\
\quad \eta \in \prod_{a\in |\cat{A}|}\cat{C}(J(a), T(a)) \\
\quad \mrm{Ext} \in \prod_{(a, b)\in |\cat{A}|\times |\cat{C}|} [\cat{C}(J(a), T(b)), \cat{C}(T(a), T(b))]
`$
相対モナドの法則は、普通のモナドと同じです。
$`\text{For } a, b, c\in |\cat{A}|\\
\text{For } f:J(a) \to T(b) \In \cat{C}\\
\text{For } g:J(b) \to T(c) \In \cat{C}\\
\quad \mrm{Ext}(\eta_a) = \id_{T(a)} \In \cat{C}\\
\quad \eta_a ; \mrm{Ext}(f) = f \In \cat{C}\\
\quad \mrm{Ext}( f;\mrm{Ext}(g) ) = \mrm{Ext}(f); \mrm{Ext}(g) \In \cat{C}
`$
相対モナドに関する用語法と記法
構成素達が $`(J, T, \eta, \mrm{Ext})`$ である相対モナドを、記号の乱用〈abuse of notation〉で書くときは次のようにします。
$`\quad T = (J, T, \eta, \mrm{Ext})`$
基礎部分である $`J`$ を分けたいときは:
$`\quad T = (T, \eta, \mrm{Ext})/J`$
$`J`$ の域・余域まで明示したいなら:
$`\quad T = (T, \eta, \mrm{Ext})/(J:\cat{A} \to \cat{C})`$
英語だと relative monad on $`T`$ over $`J`$ のような言い方もするようですが、on, over を日本語で区別するのは難しいので、「$`J`$ に沿った、台が $`T`$ である相対モナド」のような言い回しを使います。ルート関手 $`J`$ と台 $`T`$ は、どちらも $`\cat{A} \to \cat{C}`$ という関手(またはオペレーター〈コンストラクタ〉)なので、「$`\cat{A}`$ から $`\cat{C}`$ への相対モナド」とも言います。
記号の乱用が好ましくないときは、次の書き方をします。
$`\quad M = (J^M, T^M, \eta^M, \mrm{Ext}^M) = (T^M, \eta^M, \mrm{Ext}^M)/J^M`$
「相対モナドと集合係数の線形代数 // 自然数係数の有限次元線形代数のために」ではこの書き方をしています。
クライスリ射 $`f`$ に対するクライスリ拡張 $`\mrm{Ext}(f)`$ は、上付きの印で略記されます。$`f^*`$ とか $`f^\dagger`$ とか。僕は $`f^\#`$ を使っていたのですが、クライスリ拡張は共変的に作用するので、$`f_\#`$ のほうが適切だ*3と思うので、今回は下付きシャープを使います*4。相対モナドの法則は以下のように書けます。
$`\quad (\eta_a)_\# = \id_{T(a)} \In \cat{C}\\
\quad \eta_a ; f_\# = f \In \cat{C}\\
\quad ( f; g_\# )_\# = f_\#; g_\# \In \cat{C}
`$
単元集合のポインティング関手に沿った相対モナド達
ここから、相対モナドの具体例を挙げます。ひとつの個別特定の相対モナドの例ではなくて、相対モナドのクラスを定義します。それらの相対モナド達は、同じルート関手に沿ったモナド達です。まずはルート関手を定義しましょう。
$`\mbf{I}`$ は、単一の対象と恒等射だけを持つ自明な圏〈trivial category〉とします。$`|\mrm{I}| = \{0\}`$ とします。一方、$`\mbf{1} \in |\mbf{Set}|`$ は特定された単元集合とします。圏 $`\mbf{I}`$ の唯一の対象 $`0`$ に、集合圏の特定の対象である $`\mbf{1}`$ を対応させる関手を $`\bang`$ (ボールド体の感嘆符)とします。
$`\quad \bang : \mbf{I} \to \mbf{Set} \In \mbf{CAT}`$
$`\mbf{I}`$ から集合圏への関手 $`F`$ とは、単一の集合 $`F(0)\in |\mbf{Set}|`$ を指し示すので、集合 $`F(0)`$ のポインティング関手〈pointing functor〉と呼びましょう。集合 $`A\in |\mbf{Set}|`$ に対して、$`A^\sim`$ と書くことにします。
$`\quad A^\sim : \mbf{I} \to \mbf{Set} \In \mbf{CAT}
\quad \text{where }A^\sim(0) = A
`$
これから考える相対モナドは、特定された単元集合 $`\mbf{1}`$ のポインティング関手である $`\bang = \mbf{1}^\sim`$ に沿った相対モナド $`M`$ です。
$`\quad M = (T^M, \eta^M, \mrm{Ext}^M)/\bang`$
$`T^M, \eta^M, \mrm{Ext}^M`$ はそれぞれ、次のように書けます。
- $`{T^M}: \mbf{I} \to \mbf{Set} \In\mbf{CAT}`$
- $`{\eta^M}_0: \bang(0) \to {T^M}(0) \In \mbf{Set}`$
- $`{\mrm{Ext}^M}_{0, 0}: \mbf{Set}(\bang(0), {T^M}(0)) \to \mbf{Set}({T^M}(0), {T^M}(0))\In \mbf{Set}`$
$`\bang(0) = \mbf{1}`$ でした。$`\u{M} := {T^M}(0) `$ と置きましょう。$`\u{M}`$ は、相対モナド $`M`$ から決まる集合です。あらずもがなな下付きの $`0`$ は省略します。集合圏のホムセットは $`\mrm{Map}(\hyp, \hyp)`$ と書きます。すると:
- $`{\eta^M}: \mbf{1} \to \u{M} \In \mbf{Set}`$
- $`{\mrm{Ext}^M}: \mrm{Map}(\mbf{1} , \u{M} ) \to \mrm{Map}( \u{M}, \u{M} ) \In \mbf{Set}`$
$`\mrm{Ext}^M(\hyp)`$ の略記は $`\hyp_\#`$ としたうえで、相対モナドの法則を書いてみると以下のようです。
- $`(\eta^M)_\# = \id_{\u{M}} \In \mbf{Set}`$
- $`{\eta^M}; f_\# = f \In \mbf{Set}`$
- $`( f; g_\# )_\# = f_\#; g_\# \In \mbf{Set}`$
次節でさらに分かりやすい形に書き換えます。
相対モナドからモノイドへ
関数集合 $`\mrm{Map}(\mbf{1}, \u{M})`$ と集合 $`\u{M}`$ を同一視します。$`\mbf{1} = \{0\}`$ として対応は次のようです。
$`\quad \mrm{Map}(\mbf{1}, \u{M}) \ni u \longleftrightarrow u(0)\in \u{M}`$
この同一視により、$`\eta^M`$ に対応する要素を $`e`$ と置きます。
$`\quad \mrm{Map}(\mbf{1}, \u{M}) \ni \eta^M \longleftrightarrow e = \eta^M(0) \in \u{M}`$
以上の同一視により、$`(\hyp)_\#`$ は、$`\u{M}\to \mrm{Map}(\u{M}, \u{M})`$ という関数とみなせます。また、$`\u{M}`$ の要素は $`x, y`$ などで書きます(気分の問題に過ぎませんが)。相対モナドの法則は次のようになります。
- $`e_\# = \id_{\u{M}} \In \u{M}`$
- $`e.x_\# = x \In \u{M}`$
- $`( x. y_\# )_\# = x_\#; y_\# \In \mrm{Map}(\u{M}, \u{M})`$
ここで、$`e.x_\#`$ は、関数の引数を左から渡す書き方で、$`x_\#(e)`$ と同じです(次段落で説明)。あらためて、上記の3つの法則を満たすような構造 $`M = (\u{M}, e, (\hyp)_\#)`$ を“$`\bang`$ に沿った相対モナド”だと考えます。
“$`\bang`$ に沿った相対モナド”とモノイドが同じ概念であることを計算で示す際に、図式順記法が便利です。図式順記法とは、関数の結合〈合成〉を($`g\circ f`$ ではなく) $`f;g`$ と書く書き方です。関数への引数渡しも($`f(x)`$ ではなく) $`x.f`$ と書きます。
$`\quad (x.f).g = g(f(x))\\
\quad x.(f;g) = (g\circ f)(x)
`$
ドット演算子は左結合的で、セミコロンがドットより優先度が高いと約束すれば、括弧は不要になります。
$`\quad x.f.g = (x.f).g\\
\quad x.f;g = x.(f;g)
`$
上記は等しいので、次の法則があります。
$`\quad x.f.g = x.f;g`$
さて、モノイド $`X`$ を、$`X = (\u{M}, *, e)`$ とします。ここで、集合 $`\u{M}`$ は相対モナドのあの $`\u{M}`$ です。$`e\in \u{M}`$ も相対モナドのあの $`e`$ です。モノイドの二項演算 $`*`$ は次のように定義します。
$`\text{For }x, y\in \u{M}\\
\quad x*y := x.y_\#
`$
こうして定義した $`(\u{M},*, e)`$ が実際にモノイドになっていることを以下に示します。ダブルスラッシュはコメントです。
まず右単位律:
$`\quad x* e \\
\text{// モノイド二項演算の定義により}\\
= x.e_\# \\
\text{// 相対モナドの1番目の公理により}\\
= x.\id_{\u{M}}\\
\text{// 恒等写像は値を変えないから}\\
= x
`$
次は左単位律:
$`\quad e*x \\
\text{// モノイド二項演算の定義により}\\
= e.x_\# \\
\text{// 相対モナドの2番目の公理により}\\
= x
`$
最後に結合律:
$`\quad (x*y)*z \\
\text{// モノイド二項演算の定義により}\\
= (x.y_\#).z_\# \\
\text{// 関数の法則により}\\
= x.(y_\# ; z_\#)\\
\text{// 相対モナドの3番目の公理により}\\
= x.(y.z_\#)_\# \\
\text{// モノイド二項演算の定義により}\\
= x*(y*z)
`$
これで、“$`\bang`$ に沿った相対モナド”からモノイドが構成可能なことが分かりました。次節で逆方向の構成をします。
モノイドから相対モナドへ
$`M = (\u{M}, *, e)`$ をモノイドだとします -- と書くと、前節までの相対モナドと名前がコンフリクト〈衝突〉します。が、この節では気分を新たに(文脈をリセットして)モノイドありきから議論を始めるとします。
$`M`$ はモノイドなので、右単位律、左単位律、結合律は満たします。台集合の要素 $`y\in \u{M}`$ に対して、関数 $`y_\# : \u{M}\to\u{M}`$ を次のように定義します。
$`\text{For } x\in \u{M}\\
\quad x.y_\# := x * y
`$
$`(\u{M}, e, (\hyp)_\#)`$ が相対モナドの3つの公理を満たすことを示します。
まず1番目の公理:
$`\text{For }x\in \u{M}\\
\quad x.e_\#\\
\text{// 下付きシャープの定義より}\\
= x * e \\
\text{// 右単位律より}\\
= x
`$
したがって、$`e_\# = \id_{\u{M}}`$ です。
次は2番目の公理:
$`\text{For }x\in \u{M}\\
\quad e.x_\#\\
\text{// 下付きシャープの定義より}\\
= e * x \\
\text{// 左単位律より}\\
= x
`$
したがって、$`e.x_\# = x`$ です。
最後に3番目の公理:
$`\text{For }x, y, z\in \u{M}\\
\text{For }t \in \u{M}\\
\quad t.(x.y_\#)_\#\\
\text{// 下付きシャープの定義より}\\
= t.(x*y)_\# \\
\text{// 下付きシャープの定義より}\\
= t*(x*y)\\
\text{// 結合律により}\\
= (t*x) *y \\
\text{// 下付きシャープの定義より}\\
= (t.x_\#).y_\# \\
\text{// 関数の法則により}\\
= t.(x_\# ; y_\#)
`$
したがって、$`(x.y_\#)_\# = x_\# ; y_\#`$ です。
“$`\bang`$ に沿った相対モナド”からモノイドの構成と、モノイドから“$`\bang`$ に沿った相対モナド”の構成が、互いに逆構成なことは各自確認してみてください。
おわりに
相対モナドのなかでも非常に特殊なクラスである“$`\bang`$ に沿った相対モナド”達が、実はお馴染みのモノイド達だったのです。この事実からも、相対モナドの表現力と適用範囲の広さを垣間見ることが出来るでしょう。
それと、“$`\bang`$ に沿った相対モナド”とモノイドが事実上同一であることを示すときに使った図式順記法ですが、どうでしょう? 気持ちよくありませんか。