状態モナド変換子〈state monad transformer〉は、「状態モナド・変換子」ではなくて「状態・モナド変換子」です。モナド変換子の目的はモナドの変換ですが、定義上はモナドじゃなくても関手を変換できるので、「状態をひっ付ける変換子〈state attachment transformer〉」とかが適切な名前でしょう。$`\newcommand{\id}{\mathrm{id} }
\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\hyp}{\text{-}}
\newcommand{\In}{\text{ in }}
\newcommand{\T}[1]{\mathscr{#1}}
\newcommand{\twoto}{\Rightarrow }
`$
内容：
定義
$`\cat{C} = (\cat{C}, \times, {\bf 1}, [\hyp, \hyp])`$ をデカルト閉圏とします*1。具体例として集合圏を想定してかまいません。そのときは、$`[A, B] := \mrm{Map}(A, B)`$ です。
$`F:\cat{C}\to \cat{C}`$ を自己関手とします。この自己関手 $`F`$ を変形します。対象 $`S \in |\cat{C}|`$ を選んで、次のような対応を考えます。
$`\quad X\in |\cat{C}| \mapsto [S, F(X \times S)]`$
デカルト閉圏の指数〈内部ホム〉を累乗〈ベキ乗〉形式で書けば：
$`\quad X\in |\cat{C}| \mapsto F(X \times S)^S`$
対象 $`X`$ に対して $`F(X \times S)^S`$ を考えましたが、射に対しても：
$`\quad (f:X \to Y) \in \mrm{Mor}(\cat{C}) \mapsto ( F(f \times \id_S)^{\id_S} : F(X \times S)^S \to F(Y \times S)^S )`$
を考えることができます。そして、$`F(\hyp \times S)^S`$ はやはり自己関手になります。
具体例として、$`\cat{C} = {\bf Set}`$ として、自己関手 $`F`$ はベキ集合関手とします -- $`F = \mrm{Pow} : {\bf Set} \to {\bf Set}`$ 。集合 $`X, Y`$ に対して次の写像を考えます。
$`\quad f: X \to \mrm{Pow}(Y \times S)^S`$
$`f`$ を反カリー化すると：
$`\quad t := f_\cup : X\times S \to \mrm{Pow}(Y \times S)`$
こうして得られた $`t`$ は、状態空間 $`S`$ 、入力アルファベット $`X`$ 、出力アルファベット $`Y`$ の非決定性状態遷移マシンの状態遷移関数になります。$`Y = {\bf 1}`$ と置けば、出力を持たない非決定性状態遷移マシンの記述 $`t: X\times S \to \mrm{Pow}(S)`$ になります。$`\mrm{Pow}`$ の代わりに恒等関手 $`\mrm{Id}`$ を取ると、$`t: X\times S \to S`$ は決定性状態遷移マシンです。
関手性
前節の手順で $`F`$ から得られた関手を $`\T{T}_S(F)`$ と書くことにします。すると、$`\T{T}_S = \T{T}_S(\hyp)`$ は以下のような写像*2になります。
$`\quad \T{T}_S : |{\bf CAT}(\cat{C}, \cat{C})| \to |{\bf CAT}(\cat{C}, \cat{C})|`$
ここで、$`{\bf CAT}(\cat{C}, \cat{C})`$ は自己関手の圏です。
$`\T{T}_S`$ を関手のあいだの射、つまり自然変換に対しても拡張すれば、$`\T{T}_S`$ は自己関手圏 $`{\bf CAT}(\cat{C}, \cat{C})`$ に働く自己関手になります。自然変換に対する $`\T{T}_S`$ を定義しましょう。
$`\alpha`$ を自己関手 $`F`$ から $`G`$ への自然変換とします。このことは以下のように書けます（どれも同じ意味）。
- $`\alpha : F \to G \In {\bf CAT}(\cat{C}, \cat{C})`$ ： 自己関手圏の射
- $`\alpha :: F \twoto G : \cat{C} \to \cat{C} \In {\bf CAT}`$ ： 圏の圏の2-射
- $`(\alpha_X : F(X) \to G(X) \In \cat{C} )_{X \in |\cat{C}|}\; \text{ natural}`$ ： 自然変換（自然性を持つ、射のインデックス族）
$`\alpha`$ を圏の圏の2-射と捉えると、
$`\quad \T{T}_S(\alpha) :: \T{T}_S(F) \twoto \T{T}_S(G) : \cat{C} \to \cat{C} \In {\bf CAT}`$
を定義すればいいですね。自然変換は成分で決まるので、成分を取り出すと：
$`\quad (\T{T}_S(\alpha))_X : (\T{T}_S(F))(X) \to (\T{T}_S(G))(X) \In \cat{C}`$
これを決めていけばいいわけです。$`\beta := \T{T}_S(\alpha)`$ と置いて、$`\T{T}_S`$ の定義により展開すると：
$`\quad \beta_X : F(X \times S)^S \to G(X \times S)^S \In \cat{C}`$
$`\alpha_{X\times S}: F(X \times S) \to G(X \times S)`$ と、肩〈指数〉の恒等射 $`\id_S`$ を組み合わせて、
$`\quad \beta_X := {\alpha_{X\times S}}^{\id_S}`$
とすればよさそうです。自然変換の記法を関手と揃えれば、
$`\quad \beta(\hyp) = \alpha(\hyp\times S)^S`$
と、関手と同じ形で書けます。自然変換の成分引数を下付き添字にしているのは単なる（場合によって好ましくない）習慣です。
$`\beta`$ が自然変換であることを示すには、$`f:X \to Y \In \cat{C}`$ に対して、次の可換図式を確認する必要があります。
$`\require{AMScd}
\begin{CD}
F(X \times S)^S @>{ {\alpha_{X\times S}}^{\id_S} }>> G(X \times S)^S \\
@V{F(f \times \id_S)^{\id_S} }VV @V{G(f \times \id_S)^{\id_S} }VV \\
F(Y \times S)^S @>{ {\alpha_{Y\times S}}^{\id_S} }>> G(Y \times S)^S
\end{CD}\\
\text{commutative in }\cat{C}
`$
これは、比較的容易に確認できるでしょう。
$`\T{T}_S`$ にはパラメータ $`S`$ も入っているので、$`S`$ に関する関手性も示したくなりますが、$`S`$ は反変な部分も持つので細工が必要です。ここでは、状態空間は対象だけ考える（状態空間のあいだの射を考えない）ことにします。
すると、$`S`$ は $`\cat{C}`$ の対象の集合を走ることになるので：
$`\quad \T{T} : |\cat{C}|\times {\bf CAT}(\cat{C}, \cat{C}) \to {\bf CAT}(\cat{C}, \cat{C})
\In {\bf CAT}`$
$`|\cat{C}|`$ を離散圏と考えているので、$`\T{T}`$ は双関手〈二項関手〉と言えます（一応の定義上は）。あるいは、$`|\cat{C}|`$ でインデックスされた自己関手の族とも言えます。
$`\quad \T{T} : |\cat{C}| \to {\bf CAT}({\bf CAT}(\cat{C}, \cat{C}) , {\bf CAT}(\cat{C}, \cat{C}) ) \In {\bf CAT}`$
モナド
自己関手圏 $`{\bf CAT}(\cat{C}, \cat{C})`$ は、関手の結合（図式順記法 $`*`$ を使う）と恒等関手をそれぞれモノイド積／単位対象としてモノイド圏 $`({\bf CAT}(\cat{C}, \cat{C}), *, \mrm{Id})`$ になります。このモノイド圏のなかのモノイド対象がモナドなので、次のように定義します。
$`\quad \mrm{Mnd}(\cat{C}) := \mrm{Mon}(\,({\bf CAT}(\cat{C}, \cat{C}), *, \mrm{Id})\,)`$
$`\mrm{Mon}(-)`$ は“モノイド圏内のすべてのモノイド対象とモノイド準同型射からなる圏”です。
「モナドはモノイドだ」という立場ですが、一言注意しておくと、モナドのあいだの射はモノイド準同型射に限りません。他のタイプのモナドの射（例えば、双加群類似物としての射）も考えます。また、「モナドはラックス2-関手だ」と考えたほうがいいときもあります。
「モナドはモノイドだ」のインパクトが強いのでしょうか？ 「モノイドだ」の見方がガチガチにこびり付いている人がいるみたいですが、他の定義・見方もありますからね。柔軟に考えましょう。
モナド変換子
$`M \in |\mrm{Mnd}(\cat{C})|`$ とします。つまり、$`M`$ は圏 $`\cat{C}`$ 上のモナドです。モナドは台関手〈underlying functor〉とモナド演算〈実体は自然変換〉を持つので、$`M = (F, \mu, \eta)`$ と書きましょう。$`M \mapsto F`$ という対応は忘却関手 $`U`$ を定義します。
$`\quad U: \mrm{Mnd}(\cat{C}) \to {\bf CAT}(\cat{C}, \cat{C}) \In {\bf CAT}`$
先に定義した関手の変換子（自己関手圏の自己関手） $`\T{T}_S`$ を思い出します。これは、
$`\quad \T{T}_S : {\bf CAT}(\cat{C}, \cat{C}) \to {\bf CAT}(\cat{C}, \cat{C}) \In {\bf CAT}`$
でしたが、モナドの変換子になるとは言ってません。モナドの変換子にしたいなら、以下の可換図式の疑問符の部分を埋めなくてはなりません。
$`\begin{CD}
\mrm{Mnd}(\cat{C}) @>{? }>> \mrm{Mnd}(\cat{C})\\
@V{U}VV @VV{U}V\\
{\bf CAT}(\cat{C}, \cat{C}) @>{\T{T}_S}>> {\bf CAT}(\cat{C}, \cat{C})
\end{CD}\\
\text{commutative in }{\bf CAT}
`$
疑問符を埋める関手を $`\widetilde{\T{T}_S}`$ とします。$`M' := \widetilde{\T{T}_S}(M)`$ として：
- $`M' = (F', \mu', \eta')`$
- $`F' = \T{T}_S(F) = F(- \times S)^S`$
となります（上の可換図式の条件から）。あとは、$`\mu', \eta'`$ がモノイド演算になるように決めてあげればいいわけです。成分で具体的に書けば：
- $`\mu'_X : F(F(X \times S)^S \times S)^S \to F(X \times S)^S \In \cat{C}`$
- $`\eta'_X : X \to F(X \times S)^S \In \cat{C}`$
$`\mu', \eta'`$ を $`\mu, \eta`$ から構成する方法は、しばらくモニョモニョすれば見当が付くでしょう。
しかしルーティンはけっこう残っていて、
- 定義した $`(F, \mu', \eta')`$ が実際にモナドになること（モナド法則）の確認。
- モナドのあいだの射（モノイド準同型射） $`\psi : M \to N \In \mrm{Mnd}(\cat{C})`$ に対して、$`\widetilde{\T{T}_S}(\psi)`$ を定義する。
- 対象と射に対して定義した $`\widetilde{\T{T}_S} : \mrm{Mnd}(\cat{C}) \to \mrm{Mnd}(\cat{C})`$ が関手性を持つことを示す。
いつものことですが、あまり面白くない計算を愚直にするしかありません。僕は気力が切れたのでここまでにしておきます。
