
\section{Compound Monads \textit{via} the Monadic Composition Axioms } 
\label{sec-comp}

Let the type constructors $M$ and $N$, with associated functions, be monads.
Then although it is not necessarily the case that 
we can combine these two monads to form a third, this is sometimes possible.

Compound monads can arise naturally and be practically useful
(\cite{wadler-essence}, \cite{jones-composing}).
% For example, the type \textit{reader} in the SML Basis Library 
% For example, the following type, analogous to the error monad
% (\cite[\S 2.3]{wadler-essence}) is used to represent a the outcome of
% program which either terminates with a result or fails to terminate.
In this section we consider two compound monads and show that it is easy to
prove that they are monads using the monad rules for \om, 
presented in Table~\ref{tab-assrules}.

In both cases $M$ is an arbitrary monad; we don't have to set up the monad $N$,
but proceed directly to define the compound monad $N_M$.
The simple monad $N$ may be obtained using the compound construction with
$M$ as the identity monad (in which \unit, \ext, \map\ and \join\ are all
the identity function).

\subsection{Example: the Compound State Monad}
Let $M$ be a monad.
Let \State\ be a fixed type, representing, for example, a program state.
Then the state monad is given by the type $\State \to \alpha * \State$
(where $\alpha * \beta$ denotes a pair type).
This represents a computation which takes a program state and returns
a result of interest and a new state.
The compound state monad is given by the type 
$\alpha S_M = \State \to (\alpha * \State) M$.
If, for example, $M$ is the list monad,
$S_M$ could be used to represent a non-deterministic program,
which may behave in any of a number of possible ways,
each way returning a result and new state.

To show that this is a monad, we use the functions \curry\ and \unc\
% (short for \textit{uncurry})
\begin{center} \textit{
\begin{tabular}{rcl}
curry g x y & = & g (x,y) \\
unc f (x,y) & = & f x y
\end{tabular}
} \end{center} 
noting that these are mutually inverse (so, in particular, \unc\ is 1-1).
Consider a function $f : \alpha \to \beta S_M$.
Then $\unc\ f$ is of type $\alpha * \State \to (\beta * \State) M$.
Given that $M$ is a monad,
it is easy to see how to compose functions of such a type -- 
we define \oSM\ and \unitSM\ by
\begin{center} \textit{
\begin{tabular}{rcl}
unc (g \oSM\ f) & = & unc g \oM\ unc f \\
unc \unitSM & = & \unitM
\end{tabular}
} \end{center} 

The \om\ rules are then easily proved.
For each rule \lhs\ = \rhs, as \unc\ is 1-1,
it suffices to prove \unc(\lhs) = \unc(\rhs).
The proofs use the corresponding rules for the monad $M$.
\textit{
\begin{description}
\item[] \textnormal{for (\klid) and (\krid):} \\
unc (\unitSM\ \oSM\ f) = 
  unc \unitSM\ \oM\ unc f = \unitM\ \oM\ unc f = unc f 
% \item[] \textnormal{for (\krid):}
unc (f \oSM\ \unitSM) =
  unc f \oM\ unc \unitSM\ = unc f \oM\ \unitM\ = unc f \\
\item[] \textnormal{for (\kass):}
unc (h \oSM\ (g \oSM\ f)) = unc h \oM\ (unc g \oM\ unc f) = \\
\mbox{} \hfill (unc h \oM\ unc g) \oM\ unc f = unc ((h \oSM\ g) \oSM\ f)  
\end{description}
}

It is simple but tedious to confirm (\omoIass\SM) directly.
We need only check that this definition corresponds to the usual ones.
Using (\extom\SM), % we get 
\begin{itemize}
\item[] \textit{\unitSM\ a s = curry \unitM\ a s = \unitM\ (a,s)}\ , and
\item[] \textit{\extSM\ k m s = (k \oSM\ id) m s = 
  curry (unc k \oM\ unc id) m s = \\
 \mbox{} \qquad \qquad
  (\extM\ (unc k) \oo\ unc id) (m,s) = \extM\ ($\lambda(a,t)$. k a t) (m s)}
\end{itemize}
Both of these agree with the definitions in \cite[\S 7.1]{lhj} 
(modified to switch the members of pairs).

\subsection{Example: the Compound Reader Monad} \label{sec-reader}
Again, let $M$ be a monad.
Let \Env\ be a fixed type.
Then the environment, or reader, monad
is given by the type $\Env \to \alpha$
(evaluating any monadic value also involves reading the environment).
The reader monad is given by the type 
$\alpha R = \Env \to \alpha$, and
the compound reader monad \cite[\S 7.2]{lhj}, \cite[\S 6.3]{jones-composing})
is given by $\alpha R_M = \Env \to \alpha M = (\alpha M) R$.

To show that this is a monad, we define a function 
\textit{ \ape\ f a = f a e}.
In similar proofs earlier, we had a function which was 1-1;
here we need to use the property
$$(\forall e. \mbox{\ape}\ f = \mbox{\ape}\ g) \Rightarrow f = g$$

We define \oRM\ and \unitRM\ by
\begin{center} \textit{
\begin{tabular}{rcl}
(g \oRM\ f) a e & = & (\ape\ g \oM\ \ape\ f) a \\
\unitRM\ a e & = & \unitM\ a
\end{tabular}
} \end{center} 
that is, 
\begin{center} \textit{
\begin{tabular}{rcl}
\ape\ (g \oRM\ f) & = & \ape\ g \oM\ \ape\ f \\
\ape\ \unitRM & = & \unitM
\end{tabular}
} \end{center} 

The \om\ rules are then easily proved.
For each rule \lhs\ = \rhs, it suffices to let $e$ be arbitrary,
and then to prove \textit{\ape}(\lhs) = \textit{\ape}(\rhs).
The proofs use the corresponding rules for the monad $M$.
\textit{
\begin{description}
\item[] \textnormal{for (\klid) and (\krid):} \\
\ape\ (\unitRM\ \oRM\ f) = 
\ape\ \unitRM\ \oM\ \ape\ f = \unitM\ \oM\ \ape\ f = \ape\ f 
% \item[] \textnormal{for (\krid):}
\ape\ (f \oRM\ \unitRM) =
\ape\ f \oM\ \ape\ \unitRM\ = \ape\ f \oM\ \unitM\ = \ape\ f \\
\item[] \textnormal{for (\kass):}
\ape\ (h \oRM\ (g \oRM\ f)) = \ape\ h \oM\ (\ape\ g \oM\ \ape\ f) = \\
\mbox{} \hfill 
  (\ape\ h \oM\ \ape\ g) \oM\ \ape\ f = \ape\ ((h \oRM\ g) \oRM\ f)  
\end{description}
}

It is straightforward to confirm (\omoIass\RM) directly.
We need only check that this definition corresponds to the usual ones.
Using (\extom\RM), % we get 
\begin{itemize}
\item[] \textit{\unitRM\ a e = \unitM\ a}\ , and
\item[] \textit{\extRM\ k m e = (k \oRM\ id) m e = 
  (\ape\ k \oM\ \ape\ id) m = \\
 \mbox{} \qquad \qquad
  (\extM\ (\ape\ k) \oo\ \ape\ id) m = \extM\ ($\lambda a$. k a e) (m e)}
\end{itemize}
Both of these agree with the definitions in \cite[\S 7.2]{lhj}.


\section{Compound Monads \textit{via} Partial Extension} 
\label{sec-pext}

Again, let $M$ and $N$ be monads, and consider compound monads
where the compound monad type is $(\alpha N) M$, which we will just write as
$\alpha N M$.
To get a compound monad, we will need a function
$$\mbox{\extNM} : (\alpha \to \beta N M) \to (\alpha N M \to \beta N M) $$
so-called, presumably, because it ``extends'' a function $f$ 
from a ``smaller'' domain, $\alpha$, to a ``larger'' one, $\alpha N M$.
Consider, therefore, a ``partial extension'' function which does part of this
job:
$$\pext : (\alpha \to \beta N M) \to (\alpha N \to \beta N M) $$
Table~\ref{tab-prules} gives three rules which are sufficient to define
a compound monad using such a function \pext.
Note also that the two rules (\pextlu) and (\pextfun) express the fact that
\pext\ is a functor, from the Kleisli category for $M$ to that for $NM$.

\begin{table}%[!hbt]
\caption{Monad rules for a compound monad using \pext} 
\label{tab-prules}
\begin{center} \textit{
\begin{tabular}{rcl@{\qquad\qquad}r}
pext f \oo\ \unitN & = & f & (\pextru) \\
pext \unitNM & = & \unitM & (\pextlu) \\
pext (g \oNM\ f) & = & pext g \oM\ pext f & (\pextfun)
\end{tabular}
} \end{center} 
\end{table}

\begin{theorem} \label{thm-pext}
Assume that $M$ is a monad and that functions \pext, \oNM, \unitNM\ and 
\unitN\ of the appropriate types are given,
satisfying the rules in Table~\ref{tab-prules}.  Then,
using (\extom\NM) to define \extNM, 
\begin{quote}
\begin{tabular}{l@{\qquad}r@{\ \ }c@{\ \ }l}
\textbf{(\unitcomp)} & \unitNM\ & = & \unitM\ \oo\ \unitN \\
\textbf{(\ompext)} & g \oNM\ f & = & pext g \oM\ f \\
\textbf{(\extcomp)} & \extNM\ & = & \extM\ \oo\ pext \\
\textbf{(\pextext)} & \pext\ f & = & \extNM\ f \oo\ \unitM \\
\textbf{(\Jos)} & \ext\M\ (\ext\NM\ f) & = & \ext\NM\ f \oo\ \join\M \\
\textbf{(\omoass\NM)} & (h \oNM\ g) \oo\ f & = & h \oNM\ (g \oo\ f) \\
\textbf{(\pextcong)} & pext f = pext g & $\Rightarrow$ & f = g \\
\textbf{(\klid\NM)} & \unitNM\ \oNM\ f & = & f \\
\textbf{(\krid\NM)} & f \oNM\ \unitNM\ & = & f \\
\textbf{(\kass\NM)} & h \oNM\ (g \oNM\ f) & = & (h \oNM\ g) \oNM\ f
\end{tabular}
\end{quote}
\end{theorem}

\begin{proof}

\begin{description}
\item[(\unitcomp)] By (\pextru) and (\pextlu), \\
  \textit{\unitNM\ } =  
 \textit{pext \unitNM\ \oo\ \unitN} =
 \textit{\unitM\ \oo\ \unitN} 

\item[(\ompext)] By (\pextfun), 
\textit{pext (g \oNM\ f) \oo\ \unitN\ = \\
(pext g \oM\ pext f) \oo\ \unitN}.
Using (\omoass\M) and (\pextru), 
this simplifies to \textit{g \oNM\ f = pext g \oM\ f}.

\item[(\extcomp)] By (\extom\M) and (\extom\NM) we need to show \\
\textit{g \oNM\ \id\ = pext g \oM\ \id}, which follows from (\ompext).
% \textit{\extNM\ g = pext g \oM\ f = \extM\ (pext g oo id)}

\item[(\pextext)] By (\extru), 
\textit{\pext\ f = \extM\ (pext f) \oo\ \unitM}, which, by \mbox{(\extcomp)},
equals \textit{\extNM\ f \oo\ \unitM}.

\item[(\Jos)] By Theorem~\ref{thm-ext-join-iff} it suffices to show
\textit{\ext\NM\ f = \ext\M\ (\ext\NM\ f \oo\ \unit\M)},
which follows from (\extcomp) and (\pextext).

\item[(\omoass\NM)] 
By (\ompext) we need to show
\textit{(pext h \oM\ g) \oo\ f = pext h \oM\ (g \oo\ f)},
which follows from (\omoass\M).

\item[(\pextcong)] If \textit{pext f = pext g} then 
\textit{pext f \oo\ \unitN\ = pext g \oo\ \unitN}.
Using \mbox{(\pextru)}, this simplifies to $f = g$.

\item[(\klid\NM,\krid\NM,\kass\NM)] 
In each case, by (\pextcong), 
it suffices to prove \pext(\lhs) = \pext(\rhs).
In each case, this may be proved using the fact that \pext\ is a functor,
ie, using (\pextfun) and (\pextlu).
That is, we use the identity and associativity rules for \unitM\ and \oM\ to 
prove the corresponding rules for \unitNM\ and \oNM.
\textit{
\begin{description}
\item[] \textnormal{for (\klid\NM):}
pext (\unitNM\ \oNM\ f) = pext \unitNM\ \oM\ pext f =  \\
  \mbox{} \qquad \qquad \unitM\ \oM\ pext f = pext f 
\item[] \textnormal{for (\krid\NM):}
pext (f \oNM\ \unitNM) = pext f \oM\ pext \unitNM\ = \\
  \mbox{} \qquad \qquad pext f \oM\ \unitM\ = pext f 
\item[] \textnormal{for (\kass\NM):} \\
pext (h \oNM\ (g \oNM\ f)) = pext h \oM\ (pext g \oM\ pext f) = \\
\mbox{} \hfill (pext h \oM\ pext g) \oM\ pext f = pext ((h \oNM\ g) \oNM\ f)  
\end{description}
}
\end{description}
\qed
\end{proof}

By proving (\klid\NM), (\krid\NM), (\kass\NM) and (\omoass\NM),
we have proved that $NM$ is a monad.
However, we note that it is also trivial to prove the rules of  
Table~\ref{tab-eowrules} for $NM$.
In fact, using (\extcomp) and (\unitcomp),
each rule for $NM$ follows from the same rule for $M$ 
and the corresponding rule from Table~\ref{tab-prules}.

At this point we have, by (\unitcomp) and (\extcomp), that
\begin{quote} \textit{
map\NM\ f = ext\NM\ (unit\NM\ \oo\ f) = \\ 
  \mbox{} \qquad ext\M\ (pext (unit\M\ \oo\ (unit\N\ \oo\ f))) =
  (ext\M\ \oo\ pext \oo\ kl\M\ \oo\ kl\N) f
} \end{quote} 
that is, \map\NM\ is the composition of four functors.

We may next ask which compound monads can be constructed from such a
function \pext, satisfying the rules of Table~\ref{tab-prules}.
%these three rules.
Taking as read the requirement that the monadic type is $(\alpha N) M$,
(which we will regard as implicit in the notation $NM$),
the previous theorem provides one necessary condition, (\unitcomp).
Another is can be got from (\extcomp), since it tells us
$\forall f. \exists g. \ext_{NM}\ f = \ext_M\ g$.
By Theorem~\ref{thm-ext-join-iff} this is equivalent to 
$\forall f. \ext_M\ (\ext_{NM}\ f) = \ext_{NM}\ f \circ \join_M$.

\begin{theorem} \label{thm-when-pext}
Let $M$ and $NM$ be monads, such that
\begin{quote}
\begin{tabular}{l@{\qquad}r@{\ \ }c@{\ \ }l}
\textbf{(\unitcomp)} & \unitNM\ & = & \unitM\ \oo\ \unitN \\
\textbf{(\Jos)} & \ext\M\ (\ext\NM\ f) & = & \ext\NM\ f \oo\ \join\M
\end{tabular}
\end{quote}
hold.
Then the function \pext, defined by 
$$\pext\ f = \ext_{NM}\ f \circ \unit_M \qquad \qquad (\pextext)$$
satisfies the rules of Table~\ref{tab-prules}, and
$NM$ is the compound monad defined by \pext.
\end{theorem}

\begin{proof}
In defining a monad using \pext, we used (\extcomp) as a definition
(see Theorem~\ref{thm-pext}).
To show that the monad defined by \pext\ is in fact $NM$, 
we therefore need to prove (\extcomp). 
By Theorem~\ref{thm-ext-join-iff}, \ref{ej1} $\Rightarrow$ \ref{ej2}, 
we have 
  \textit{\ext\NM\ f = \ext\M\ (\ext\NM\ f \oo\ \unit\M) =
   \ext\M\ (\pext\ f)}, as required.

We now show the \pext\ axioms of Table~\ref{tab-prules}.
In each case (\pextext) and 
the corresponding axiom of Table~\ref{tab-eowrules} are used.

\begin{description}
\item[(\pextru)] Using also (\unitcomp) we have \\
\textit{\pext\ f \oo\ \unit\N\ = \ext\NM\ f \oo\ \unit\M\ \oo\ \unit\N\ =
 \ext\NM\ f \oo\ \unit\NM\ = f}
\item[(\pextlu)] \textit{\pext\ \unit\NM\ = \ext\NM\ \unit\NM\ \oo\ \unit\M\ =
 \unit\M}
\item[(\pextfun)] ~ \\
\textit{
\begin{tabular}{rcl@{\quad\qquad}r}
\pext\ (g \oNM\ f) & = & \ext\NM\ (g \oNM\ f) \oo\ \unit\M\ & (\pextext) \\
 & = &  \ext\NM\ g \oo\ \ext\NM\ f \oo\ \unit\M\ & (\extfun\NM) \\
 & = &  \ext\M\ (\pext\ g) \oo\ \pext\ f & (\extcomp, \pextext) \\
 & = & \pext\ g \oM\ \pext\ f & (\omext\M)
\end{tabular} }
\end{description}
\qed
\end{proof}

\subsection{Relation to the \textit{prod} Construction of Jones \& Duponcheel}

We have, in Theorems \ref{thm-pext} and \ref{thm-when-pext},
shown that the compound monads which can be defined in terms of a function
\pext\ are precisely those satisfying (\unitcomp) and (\Jos).

Jones \& Duponcheel \cite{jones-composing} show how to define a compound 
monad using a function \prd, and show that the compound monads which can be
defined using \prd\ are precisely those satisfying (\unitcomp) and the
following rules.  Note that (\Jo) is the special case $f = \id$ of (\Jos).

\begin{center} \textit{
\begin{tabular}{rcl@{\qquad\qquad}r}
\map\NM\ f & = & \map\M\ (\map\N\ f) & (\mapcomp) \\
\ext\M\ \join\NM & = & \join\NM\ \oo\ \join\M & (\Jo)
\end{tabular} 
} \end{center}

In fact these two conditions are sufficient to imply (\Jos),
and so the \pext\ construction is applicable whenever the \prd\ construction
is.
Whether the converse is true is an open question.
Further, \prd\ can be obtained from \pext:
\begin{center} \textit{
\textit{\prd\ = \pext\ \id \qquad \qquad (\prdpext)}
} \end{center}

\begin{theorem} \label{thm-prod}
Assume that (\unitcomp), (\mapcomp) and (\Jo) hold for a compound monad $NM$.
Use (\pextext) to define \pext, and (\prdpext) to define \prd.
Then 
\begin{quote}
\begin{tabular}{l@{\qquad}r@{\ \ }c@{\ \ }l}
\textbf{(\Jos)} & \ext\M\ (\ext\NM\ f) & = & \ext\NM\ f \oo\ \join\M \\
\textbf{(\pext)} & \multicolumn{3}{l}
  {the rules of Table~\ref{tab-prules} 
  and the results of Theorem~\ref{thm-pext} hold} \\
\textbf{(\pexto)} & \pext\ (g \oo\ f) & = & \pext\ g \oo\ \map\N\ f \\
\textbf{(\pextpm)} & \pext\ f & = & \prd\ \oo\ \map\N\ f \\
\textbf{(\Pof)} & \pext\ (\ext\NM\ g) & = & \ext\NM\ g \oo\ \prd
\end{tabular}
\end{quote}
\end{theorem} 

\begin{proof}
\begin{description}
\item[(\Jos)] By Theorem~\ref{thm-ext-join-iff},
\ref{ej1} $\Rightarrow$ \ref{ej3}, 
we can assume, from (\Jo), that \\
\textit{\join\NM\ = \ext\M\ g}.
By Theorem~\ref{thm-ext-join-iff}, \ref{ej3} $\Rightarrow$ \ref{ej1}, 
for any given $f$,
it is enough to find $h$ such that \textit{\ext\NM\ f = \ext\M\ h}.

\textit{
\begin{tabular}{rcl@{\qquad\qquad}r}
\ext\NM\ f & = & \join\NM\ \oo\ \map\NM\ f & (\extjm\NM) \\
           & = & \ext\M\ g \oo\ \map\M\ (\map\N\ f) & (\mapcomp) \\
	   & = & \ext\M\ (g \oo\ \map\N\ f) & (\exto\M)
\end{tabular} }

\item[(\pext)] By Theorem~\ref{thm-when-pext} $NM$ can be defined using \pext.

\item[(\pexto)] The next line follows from (\extcomp) and (\mapcomp).

\hspace{-4pt}\textit{
\begin{tabular}{rcl@{}r}
\ext\NM\ g \oo\ \map\NM\ f 
  & = & \ext\M\ (\pext\ g) \oo\ \map\M\ (\map\N\ f) & \\
\ext\NM\ (g \oo\ f) & = & \ext\M\ (\pext\ g \oo\ \map\N\ f) &
  (\exto\NM, \exto\M) \\
\ext\M\ (\pext\ (g \oo\ f)) & = & \ext\M\ (\pext\ g \oo\ \map\N\ f) &
  (\extcomp) \\
\pext\ (g \oo\ f) & = & \pext\ g \oo\ \map\N\ f & (\extcong) 
\end{tabular} }

\item[(\pextpm)] By (\prdpext), 
this is the special case $g = \id$ of (\pexto).

\item[(\Pof)] ~

\textit{
\begin{tabular}{rcl@{\qquad}r}
\pext\ (g \oNM\ \id) & = & \pext\ g \oM\ \pext\ \id & (\pextfun) \\
\pext\ (g \oNM\ \id) & = & \ext\M\ (\pext\ g) \oo\ \prd & 
  (\omext\M, \prdpext) \\
\pext\ (\ext\NM\ g) & = & \ext\NM\ g \oo\ \prd & (\extom\NM, \extcomp) 
\end{tabular} }
\end{description}
\qed
\end{proof}

We can set $f = id$ in (\extcomp) and (\pextext),
and simplify using (\joinext) and (\prdpext),
to get \textit{\join\NM\ = ext\M\ \prd} and 
\textit{\prd\ = \join\NM\ \oo\ \unit\M},
which are used/proved in \cite[\S3.2,\S4.1]{jones-composing}.
This shows that the \prd\ and \pext\ constructions give the same compound
monad.

It is also straightforward to prove the results P(1) to P(4) of
\cite[\S3.2]{jones-composing}.
Using (\pextpm) and (\mapext\NM) or (\joinext\NM), P(1) and P(4) are
special cases of (\Pof) above.
By (\prdpext), P(2) is a special case of (\pextru), and 
by (\pextpm), P(3) is (\pextlu).

\subsection{Example: the Compound Exception Monad}
The exception (or error) monad is given by 
\begin{center}
\texttt{ datatype $\alpha$ E = Ok of $\alpha$ | Err of string }
\end{center}
with \textit{unit\E\ a = Ok a}.
% and \ext\ defined similarly to \pext\ below.

With $M$ an arbitrary monad we define the compound monad $\alpha E M$ by

\begin{center} \textit{
\begin{tabular}{rcl@{\qquad\qquad}r}
pext f (Ok a) & = & f a & (\pextOk) \\ 
pext f (Err msg) & = & unit\M\ (Err msg) & (\pextErr)
\end{tabular} 
} \end{center}
(Letting $M$ be the identity monad gives us the definition of \ext\E,
for then \pext\ is \ext\E).
We also define \unit\EM\ and \oEM\ by
(\unitcomp) and (\ompext).
Then we prove the \pext\ axioms (Table~\ref{tab-prules}) as follows.
(\pextru) is just (\pextOk).
Using the definitions just mentioned, we get (\pextlu) from
\begin{center} \textit{
pext unit\EM\ (Ok a) = unit\EM\ a = unit\M\ (Ok a) \\
pext unit\EM\ (Err msg) = unit\M\ (Err msg)
} \end{center}
and using these definitions and also (\omext\M) we get (\pextfun) from

\begin{center} \textit{
\begin{tabular}{rcl@{\qquad}r}
pext (g \oEM\ f) (Ok a) & = & (pext g \oM\ f) a & (\pextOk, \ompext) \\
  & = & ext\M\ (pext g) (f a) & (\omext\M) \\
& = & ext\M\ (pext g) (pext f (Ok a)) & (\pextOk) \\
& = & (pext g \oM\ pext f) (Ok a) & (\omext\M)
\end{tabular} 
} \end{center}

\begin{center} \textit{
\begin{tabular}{rcl@{\quad}r}
pext (g \oEM\ f) (Err msg) 
  & = & unit\M\ (Err msg) & (\pextErr) \\
  & = & pext g (Err msg) & (\pextErr) \\
& = & ext\M\ (pext g) (unit\M\ (Err msg)) & (\extru) \\
& = & ext\M\ (pext g) (pext f (Err msg)) & (\pextErr) \\
& = & (pext g \oM\ pext f) (Err msg) & (\omext\M) 
\end{tabular} 
} \end{center}

\subsection{Other Examples; Isabelle Proofs}
\subsubsection{Example: the Compound Writer Monad}

Let \Monoid\ be a type representing a monoid, where we use
0 for the identity value and + for the associative binary operation.
Then let $\alpha W = (\Monoid * \alpha)$
and $\alpha W M = (\alpha W) M$.
A function $f : \alpha \to \beta W$ represents a function from $\alpha$ to
$\beta$ which also produces some output $m$ of type \Monoid; 
when \ext\W\ $f$ acts on \textit{(acc, a)}, where \acc\ represents output
already accumulated, the output $m$ is added to that in \acc.
That is, if $f\ a = (m,b)$, then 
\textit{\ext\W\ f (\acc,a) = (\acc\ $+$ m, b)}.
Naturally, $\unit_W\ a = (0,a)$. % \textit{unit\W\ a = (0,a)}.

The compound writer monad is given by 
\begin{center} \textit{
\pext\ f (\acc,a) = \map\M\ ($\lambda$(m,b). (\acc\ $+$ m, b)) (f a) 
} \end{center}

That is, the addition of the new output $m$ to the accumulated output
\acc\ is done ``under the hood'' of the monad $M$.
This makes the proof of the axioms for \pext\ more difficult,
and we omit them.  
(Jones \& Duponcheel \cite[\S 6.5.1]{jones-composing} also omit
proofs for this monad).

\subsubsection{Example: the Compound Reader Monad}

This was discussed in \S\ref{sec-reader}.
We write the monad type as $\alpha N R$, where $R$ takes the place of $M$ in 
our general results.
Note that, here, the monad $R$ is fixed, while $N$ is arbitrary.
The \pext\ construction applies to this compound monad,
but to use it, we need to show 
\begin{enumerate}
\renewcommand\theenumi{(\roman{enumi})}
\renewcommand\labelenumi\theenumi
\item \label{rmon} that $R$ is a monad
\item \label{nmon} that $N$ is a monad
\item \label{pext} that the axioms for \pext, in Table~\ref{tab-prules}, hold
\end{enumerate}
Our treatment of compound monads using the \pext\ axioms requires, as such,
only \ref{rmon} and \ref{pext}, but we need \ref{nmon} to prove \ref{pext}.
These proofs are, however, not difficult, and are omitted.


\subsubsection{Isabelle Proofs}

The proofs in this paper and the proofs for the compound reader and writer
monads were performed using the theorem prover Isabelle,
and are accessible from the author's home page.

Jones \& Duponcheel, \cite[\S 6.4]{jones-composing},
discuss the compound list monad -- 
$\alpha$ \textit{list M} is a monad provided that
$M$ is a \emph{commutative} monad.
The proofs, which are given by Jones \& Duponcheel, are difficult.
We also have Isabelle proofs of the \pext\ axioms for the compound list monad.

\section{Conclusion} \label{sec-concl}

By focussing on the Kleisli category of a monad and the functors to and from it
we have provided simple proofs of some compound monad constructions.
This provided an interesting application of Wadler's parametricity theorem.
We have described a construction which applies to several compound monads
which is a functor \pext\ from the Kleisli category of the compound monad $NM$
into the Kleisli category of $M$, and which generalizes the \prd\
construction of Jones \& Duponcheel.
This also has facilitated proofs concerning some compound monads.

