圏論におけるFreeモナド

$\require{AMScd}$

はじめに

HaskellではFreeモナドという関手からモナドを作る機構があり，次のように定義される．

data Free f a = Pure a | Free (f (Free f a))

instance Functor f => Monad (Free f) where
  return = Pure
  Pure a >>= f = f a
  Free m >>= f = Free (fmap (>>= f) m)

これが圏論の意味でモナドになっているかを書いている記事を見つけられなかったので書いてみた．

予備知識

圏論の基本的知識(余積，関手，自然変換)は仮定します．
また，Haskellの代数的データは圏論では始代数のことなので，始代数の知識も仮定します．

関手$T : \mathbf{C} \to \mathbf{C}$と自然変換$\eta : I \to T, \mu : T^2 \to T$の組$(T,\eta,\mu)$がモナドとは次の2つの等式を満たすこと．

• $\mu \circ T\mu = \mu \circ \mu T$
• $\mu \circ T\eta = 1 = \mu \circ \eta T$

仮定

本記事を通して，ある関手$F:\mathbf{C}\to\mathbf{C}$を固定し，任意の$X\in \mathbf{C}$について関手$Y \mapsto FY+X$の始代数が$\mathbf{C}$に存在すると仮定する．

また，余積$A+B$の入射を$\iota_1 : A \to A+B, \iota_2 : B \to A+B$とする．

Freeモナドの関手

仮定より$Y \mapsto FY+X$の始代数が$X$ごとに存在するのでその台を$TX$とする．つまり，
$$(TX, \alpha_X : FTX+X \to TX)$$が始代数である．

この対応は関手$T : \mathbf{C} \to \mathbf{C}$を定めることをみていく．

まず射$f : A \to B$に対して$Tf : TA \to TB$を次を可換にする射とする．

\begin{CD}
FTA+A @>{FTf+A}>> FTB+A \\
@V{\alpha_A}VV @VV{\alpha_B\,\circ(1+f)}V \\
TA @>>{Tf}> TB
\end{CD}

そのような射は始代数の普遍性からちょうど一つのみなことに注意する．

このとき$T1_A=1_{TA}$である．なぜならば，$T1_A$は次の可換性を満たすが，$\alpha_A\circ(1+1_A)=\alpha_A$なので，始代数から始代数への準同型となり，それは$1_{TA}$のみである．

\begin{CD}
FTA+A @>{FT1_A+A}>> FTA+A \\
@V{\alpha_A}VV @VV{\alpha_A\,\circ(1+1_A)}V \\
TA @>>{T1_A}> TA
\end{CD}

また，$T(g\circ f) = Tg\circ Tf$である．$T(g\circ f)$は次の可換性を満たす．

\begin{CD}
FTA+A @>{FT(g\circ f)+A}>> FTC+A \\
@V{\alpha_A}VV @VV{\alpha_A\,\circ(1+(g\circ f))}V \\
TA @>>{T(g\circ f)}> TC
\end{CD}

$Tg\circ Tf$についても以下のように同じ可換性を満たすことがわかる．

\begin{align}
Tg\circ Tf &= Tg \circ \alpha_B \circ (1+f)\circ(FTf+A) \\
&= \alpha_C \circ (FTg+g)\circ(FTf+f) \\
&= \alpha_C \circ (F(Tg\circ Tf) + (g\circ f))
\end{align}

よって，始代数の普遍性から$T(g\circ f) = Tg\circ Tf$である．

以上のことから関手$T:\mathbf{C}\to\mathbf{C}$が与えられた．

Freeモナドの自然変換

$\eta_X : X \to TX$を$\eta_X = \alpha_X \circ \iota_2$で定義する．また，$\mu_X : T^2X\to X$を次の図を可換にする射とする(ここで，$h=[\alpha_X\circ\iota_1,1_{TX}]$)．

\begin{CD}
FT^2X+TX @>{F\mu_X+TX}>> FTX+TX \\
@V{\alpha_{TX}}VV @VVhV \\
T^2X @>>{\mu_X}> TX
\end{CD}

このとき，$\eta_X, \mu_X$はそれぞれ自然変換になる．まず，$\eta_X$についてみていく．$\eta_X$が自然変換であることを示すには次が可換になることを示せばよい．

\begin{CD}
A @>{\eta_A}>> TA \\
@VfVV @VVTfV \\
B @>>{\eta_B}> TB
\end{CD}

これは次からわかる．

\begin{align}
Tf\circ\eta_A &= Tf\circ\alpha_A\circ\iota_2 \\
&= \alpha_B\circ(FTf+f)\circ\iota_2 \\
&= \alpha_B\circ\iota_2\circ f\\
&= \eta_B\circ f
\end{align}

次に$\mu_X$が自然変換なことを見るために，以下が可換なことを示す．

\begin{CD}
T^2A @>\mu_A>> TA \\
@VT^2fVV @VVTfV \\
T^2B @>>\mu_B> TA
\end{CD}

このとき，以下が可換になる．

\begin{CD}
FT^2A+TA @>{F(Tf\circ\mu_A)+TA}>> FTB+TA \\
@V\alpha_{TA}VV @VV{[\alpha_B\circ\iota_1, Tf]}V \\
T^2A @>>{Tf\circ\mu_A}> TB
\end{CD}

これは以下からわかる．

\begin{align}
Tf\circ\mu_A\circ\alpha_{TA}\circ\iota_1
&= Tf\circ[\alpha_A\circ\iota_1,1_{TA}]\circ(F\mu_A+1_{TA})\circ\iota_1 \\
&= TF\circ[\alpha_A\circ\iota_1,1_{TA}]\circ\iota_1\circ F\mu_A \\
&= Tf\circ\alpha_A\circ\iota_1\circ F\mu_A \\
&= \alpha_B\circ(FTf+f)\circ\iota_1 F\mu_A \\
&= \alpha_B\circ\iota_1\circ F(Tf\circ\mu_A) \\
&= [\alpha_B\circ\iota_1,Tf]\circ\iota_1 \\
Tf\circ\mu_A\circ\alpha_{TA}\circ\iota_2 
&= Tf\circ[\alpha_A\circ\iota_1, 1_{TA}]\circ(F\mu_A+1_{TA})\circ\iota_2 \\
&= Tf\circ[\alpha_A\circ\iota_1,1_{TA}]\circ\iota_2 \\
&= Tf \\
&= [\alpha_B\circ\iota_1,Tf]\circ\iota_2
\end{align}

同様にして次が可換になる．

\begin{CD}
FT^2A+TA @>{F(\mu_B\circ T^2f)+TA}>> FTB+TA \\
@V\alpha_{TA}VV @VV{[\alpha_B\circ\iota_1, Tf]}V \\
T^2A @>>{\mu_B\circ T^2f}> TB
\end{CD}

よって，始代数の普遍性より，$Tf\circ\mu_A = \mu_B\circ T^2f$．

Freeモナド

$(T,\eta,\mu)$はモナドであることを示す．

まず，$\mu\circ T\mu=\mu\circ \mu T$を示すが，これは$\mu_X\circ T\mu_X=\mu_X\circ \mu_{TX}$と同じであることに注意する．

ここで，次が成り立つ．

\begin{align}
\mu_X\circ T\mu_X \circ \alpha_{T^2X}
&= \mu_X \circ \alpha_{TX} \circ (FT\mu_X + \mu_X) \\
&= [\alpha_X\circ\iota_1, 1_{TX}]\circ (F\mu_X + TX)\circ(FT\mu_X + \mu_X) \\
&= [\alpha_X\circ\iota_1, \mu_X] \circ (F(\mu_X\circ T\mu_X) + T^2X)
\end{align}

すなわち，次が可換になる．

\begin{CD}
FT^3X+T^2X @>{F(\mu_X\circ T\mu_X)+T^2X}>> FTX+T^2X \\
@V\alpha_{T^2X}VV @VV{[\alpha_X\circ\iota_1, \mu_X]}V \\
T^3X @>>{\mu_X\circ T\mu_X}> TX
\end{CD}

また，次も可換になる．

\begin{CD}
FT^3X+T^2X @>{F(\mu_X\circ \mu_{TX})+T^2X}>> FTX+T^2X \\
@V\alpha_{T^2X}VV @VV{[\alpha_X\circ\iota_1, \mu_X]}V \\
T^3X @>>{\mu_X\circ \mu_{TX}}> TX
\end{CD}

これは次からわかる．

\begin{align}
\mu_X\circ\mu_{TX}\circ\alpha_{T^2X}\circ\iota_1
&= \mu_X\circ[\alpha_{TX}\circ\iota_1, 1_{T^2X}]\circ(F\mu_{TX}+T^2X)\circ\iota_1\\
&= \mu_X\circ\alpha_{TX}\circ\iota_1\circ F\mu_X \\
&= [\alpha_X\circ\iota_1, 1_{TX}]\circ(F\mu_X+TX)\circ\iota\circ F\mu_X \\
&= \alpha_X\circ\iota_1\circ F(\mu_X\circ\mu_{TX}) \\
&= [\alpha_X\circ\iota_1,\mu_X]\circ(F(\mu_X\circ\mu_{TX})+T^2X)\circ\iota_1 \\
\mu_X\circ\mu_{TX}\circ\alpha_{T^2X}\circ\iota_2
&= \mu_X\circ[\alpha_TX\circ\iota_1,1_{T^2X}]\circ(F\mu_{TX}+T^2X)\circ\iota_2 \\
&= \mu_X \\
&= [\alpha_X\circ\iota_1,\mu_X]\circ(F(\mu_X\circ\mu_{TX})+T^2X)\circ\iota_2
\end{align}

よって，始代数の普遍性から$\mu_X\circ T\mu_X=\mu_X\circ\mu_{TX}$．

次に，$\mu_X\circ\eta_{TX}=1_{TX}=\mu_X\circ T\eta_X$を示す．

\begin{align}
\mu_X\circ\eta_{TX}
&= \mu_X\circ\alpha_X\circ\iota_2 \\
&= [\alpha_X\circ\iota_1,1_{TX}]\circ(F\mu_X+TX)\circ\iota_2 \\
&= 1_{TX} 
\end{align}

よって，$\mu_X\circ\eta_{TX}=1_{TX}$．残りは$\mu_X\circ T\eta_X=1_{TX}$だが，それには次が可換になることを示せばよい．

\begin{CD}
FTX+X @>{F(\mu_X\circ T\eta_X)+X}>> FTX+X \\
@V\alpha_XVV @VV\alpha_XV \\
TX @>>{\mu_X\circ T\eta_X}> TX
\end{CD}

これは次からわかる．

\begin{align}
\mu_X\circ T\eta_X \circ\alpha_X\circ\iota_1
&= \mu_X\circ\alpha_{TX}\circ(FT\eta_X + \eta_X)\circ\iota_1 \\
&= [\alpha_X\circ\iota_1,1_{TX}]\circ(F(\mu_X\circ T\eta_X)+\eta_X)\circ\iota_1 \\
&= \alpha_X\circ\iota_1\circ F(\mu_X\circ T\eta_X) \\
&= \alpha_X\circ(F(\mu_X\circ T\eta_X)+X)\circ\iota_1 \\
\mu_X\circ T\eta_X\circ\alpha_X\circ\iota_2
&= [\alpha_X\circ\iota_1,1_{TX}]\circ(F(\mu_X\circ T\eta_X)+\eta_X)\circ\iota_2 \\
&= \eta_X \\
&= \alpha_X\circ\iota_2 \\
&= \alpha_X\circ(F(\mu_X\circ T\eta_X)+X)\circ\iota_2 \\
\end{align}

以上より$(T,\eta,\mu)$はモナドである．