% APPENDIX

\renewcommand\theenumi{\roman{enumi}}
\renewcommand\labelenumi{(\theenumi)}

\section{Some examples using rules (\ref{krid}) to (\ref{omoIass})}
\label{app-ex}

In this section we give some examples of monads which are easily 
shown to be monads using rules (\ref{krid}) to (\ref{omoIass}).

The two examples in \S \ref{ex-comp-st} and \S \ref{ex-comp-rdr}
are (in different senses) compound monads.
In both cases $M$ is an arbitrary monad; 
we don't explicitly use the monad $N$,
but proceed directly to define the compound monad $N_M$.
The simple monad $N$ will be a special case of $N_M$,
which could be obtained by setting $M$ to be the identity monad 
(in which \unit, \ext, \map\ and \join\ are all the identity function).

\subsection{Example: the Continuation Monad} \label{ex-cont}

The continuation monad (eg, \cite[\S 3.1]{wadler-essence}) is given by 
$\alpha K = (\alpha \to \Ans) \to \Ans$,
where \Ans\ is a fixed type,
so $\alpha \to \beta K = \alpha \to (\beta \to \Ans) \to \Ans$.
We use the function \C, %(``switch arguments'')
of type $(\gamma \to \delta \to \Ans) \to (\delta \to \gamma \to \Ans)$,
defined by \mbox{\textit{C f x y = f y x}}.
Note that \textit{C (C f) = f}, so \C\ is 1-1, and
$\C\ x = \C\ y \Rightarrow x = y$.
Then we define \oK\ by
\textit{C (g \oK\ f) = C f \oo\ C g},
and \unitK\ by \textit{C \unitK\ = id}.

The \om\ rules are then easily proved.
For each rule \lhs\ = \rhs, as \C\ is 1-1,
it suffices to prove \C(\lhs) = \C(\rhs).
\textit{
\begin{description}
\item[] \textnormal{for (\ref{krid}):}
C (f \oK\ unit\K) = C unit\K\ \oo\ C f = id \oo\ C f = C f 
\item[] \textnormal{for (\ref{klid}):}
C (unit\K\ \oK\ f) = C f \oo\ C unit\K\ = C f \oo\ id = C f 
\item[] \textnormal{for (\ref{kass}):}
C (h \oK\ (g \oK\ f)) = (C f \oo\ C g) \oo\ C h = \\
\mbox{} \hfill C f \oo\ (C g \oo\ C h) = C ((h \oK\ g) \oK\ f)  
\end{description}
}

It is simple but tedious to confirm (\ref{omoIass}) directly.
We now check that this definition corresponds to the usual ones.
Using (\ref{extom}), we get 
\begin{itemize}
\item[] \textit{\unitK\ a c = C id a c = id c a = c a}\ , and
\item[] \textit{\extK\ g k c = (g \oK\ id) k c = C (C id \oo\ C g) k c = \\
 \mbox{} \qquad \qquad
 (C id \oo\ C g) c k = C id (C g c) k = id k (C g c) = 
 k ($\lambda$f. g f c)}
\end{itemize}
Both of these agree with the definitions in \cite[\S 3.1]{wadler-essence}.

\subsection{Example: the Compound State Monad} \label{ex-comp-st}
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 
$\alpha S = \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$.
(Note that because $\alpha S_M$ is neither 
$\alpha S M$ nor $\alpha M S$,
\S \ref{sec-pext} and following are 
\emph{not} relevant to this example, which perhaps should
not be called a ``compound monad'').
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{align*} 
\curry\ g\ x\ y & = g\ (x,y) &
\unc\ f\ (x,y) & = f\ x\ y
\end{align*} 
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{align*} 
\unc\ (g \oSM f) & = \unc\ g \oM \unc\ f \\[-0.5ex]
\unc\ \unitSM & = \unitM
\end{align*} 

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$.
\begin{description}
\mditem[for (\ref{krid}) and (\ref{klid}):] \\
$\unc\ (f \oSM \unitSM) =
  \unc\ f \oM \unc\ \unitSM = \unc\ f \oM \unitM = \unc\ f$
$\unc\ (\unitSM \oSM f) = 
  \unc\ \unitSM \oM \unc\ f = \unitM \oM \unc\ f = \unc\ f$ \\
\mditem[for (\ref{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 (\ref{omoIass}) directly.
We need only check that this definition corresponds to the usual ones.
Using (\ref{extom}), % 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{ex-comp-rdr}
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} (for $e : \Env$), of type
$(\gamma \to \Env \to \delta) \to (\gamma \to \delta)$.
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 (\ref{krid}) and (\ref{klid}):} \\
\ape\ (f \oRM\ \unitRM) =
\ape\ f \oM\ \ape\ \unitRM\ = \ape\ f \oM\ \unitM\ = \ape\ f \\
\ape\ (\unitRM\ \oRM\ f) = 
\ape\ \unitRM\ \oM\ \ape\ f = \unitM\ \oM\ \ape\ f = \ape\ f \\
\item[] \textnormal{for (\ref{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 (\ref{omoIass}) directly.
We need only check that this definition corresponds to the usual ones.
Using (\ref{extom}), % 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{Relation between our constructions and others previously described}
\label{app-jd}

In this section we compare our constructions with
those of Jones \& Duponcheel \cite{jones-composing},
and also with the distributive law for monads of Manes \cite{manes}.

Throughout this section we 
assume at least that $M$ and $N$ are premonads,
and that we have functions \unitNM\ and \mapNM\ for which
(\ref{UC}) and (\ref{MC}) hold.
We note that when $N$ and $M$ are premonads, 
then (\ref{UC}) and (\ref{MC}) give that $NM$ is a premonad
\cite[\S 3]{jones-composing}.

\subsection{Relation between the \textit{pext} construction and 
  the \textit{prod} construction of Jones \& Duponcheel} \label{app-pp}

In this subsection we further assume that $M$ is a monad.  
Under these assumptions 
Jones \& Duponcheel \cite[\S 3.2,\S 4.1]{jones-composing} 
show that the compound monads $NM$ which can be
defined using \prd\ and the four rules P(1) to P(4)
are precisely those satisfying (\ref{J1}).
%
\begin{align*} 
\prd \oo \mapN\ (\mapNM\ f) & = \mapNM\ f \oo \prd\ 
  \tag*{P(1)}  \\[-0.5ex]
\prd \oo \unitN\ & = id \tag*{P(2)}  \\[-0.5ex]
\prd \oo \mapN\ \unitNM\ & = \unitM \tag*{P(3)}  \\[-0.5ex]
\prd \oo \mapN\ \joinNM\ & = \joinNM \oo \prd \tag*{P(4)} 
\end{align*}

We relate \prd\ to \pext, and list other relevant equalities,
with an easy lemma relating them.
%
\setcounter{equation}{0}
\renewcommand\theequation{PP\arabic{equation}}
\begin{align}
\prd & = \pext\ \id \label{prdpext} \\[-0.5ex]
\pext\ f & = \prd \oo \mapN\ f \label{pextpm} \\[-0.5ex]
\pext\ (g \oo f) & = \pext\ g \oo \mapN\ f \tag{\ref{pexto}} \\
\pext\ f \oo \unitN & = f \tag{\ref{pextru'}}
\end{align}

\begin{lemma} \label{lem-pp}
\begin{enumerate}
\item \label{ppo}
  (\ref{pextpm}) holds iff (\ref{prdpext}) and (\ref{pexto}) hold.
\item (\ref{pextru'}) holds iff (\ref{pextru}) holds.
\item assuming (\ref{pextpm}), P(2) holds iff (\ref{pextru'}) holds.
\item assuming (\ref{pextpm}), P(3) is just (\ref{pextlu}).
\end{enumerate}
\end{lemma}

\begin{theorem} \label{thm-prod}
Assume that $NM$ is a compound monad, for which (\ref{J1}) holds.
Use (\ref{PE}) to define \pext, and (\ref{prdpext}) to define \prd.
Then (\ref{J1S}) holds, and (\ref{pextpm}), (\ref{pexto}) and
P(1) to P(4) hold.
\comment{
\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}
  {(\ref{pextru}) to (\ref{pextfun}) %the rules of Table~\ref{tab-prules} 
  and the results of Theorem~\ref{thm-pext-k} hold} \\
\textbf{(\pextru-N)} & \pext\ f \oo \unitN & = & f \\
\textbf{(\pexto)} & \pext\ (g \oo f) & = & \pext\ g \oo \map\N\ f \\
\textbf{(\pextpm)} & \pext\ f & = & \prd \oo \map\N\ f \\
\textbf{(\P14)} & \pext\ (\ext\NM\ g) & = & \ext\NM\ g \oo \prd
\end{tabular}
\end{quote}
}
\end{theorem} 

\begin{proof}
% \begin{description}
% \mditem[(\ref{J1S}):] 
By Lemma~\ref{lem-J1}, (\ref{J1S}) holds. 
%
We now have that Theorems \ref{thm-when-pext} and \ref{thm-pext-k} hold, and
% Using (\ref{PE}), the following gives (\ref{pexto}),
Lemma~\ref{lem-pko} gives (\ref{pexto}), from which (\ref{pextpm}) follows.
\comment{
\begin{align*}
\extNM\ (g \oo f) \oo \unitM 
  & = \extNM\ g \oo \mapNM\ f \oo \unitM \tag{\ref{exto}NM} \\[-0.5ex]
  & = \extNM\ g \oo \unitM \oo \mapN\ f \tag{\ref{MC}, \ref{MJ3}M} 
\end{align*}
}%
To prove P(1) and P(4), we use the following result.
\begin{align*}
\pext\ (\extNM\ g) & = \pext\ (g \oNM \id) \tag{\ref{extom}NM} \\[-0.5ex]
  & = g \oNM \pext\ \id \tag{\ref{extfun}K, \ref{omext}K} \\[-0.5ex]
  & = \extNM\ g \oo \prd \tag{\ref{omext}NM, \ref{prdpext}} 
\end{align*}
%
From this we use (\ref{pextpm}), and (\ref{mapext}NM) and (\ref{joinext}NM)
respectively, to get P(1) and P(4).
% Using (\ref{pextpm}), P(3) is (\ref{pextlu}),
% and using (\ref{prdpext}), P(2) is a case of (\ref{pextru'}).
% By (\ref{prdpext}), P(2) is a special case of (\ref{pextru'}), and 
% by (\ref{pextpm}), P(3) is (\ref{pextlu}).
Finally, Lemma~\ref{lem-pp} gives P(2) and P(3). \qed
\end{proof}

We note that our definition of \prd\ gives
$\prd\ = \pext\ \id\ = \extNM\ \id \oo \unitM\ = \joinNM \oo \unitM$
which is the definition used in \cite[\S4.1]{jones-composing}.
% This shows that the \prd\ and \pext\ constructions 
% give the same compound monad.

The following converse theorem is \cite[\S3.2]{jones-composing}.

\begin{theorem}
Let function \prd\ be given, and
define \joinNM\ by $\joinNM = \extM\ \prd$.
Let P(1) to P(4) be satisfied.
Then $NM$ is a monad, satisfying (\ref{J1}).
\end{theorem}

\begin{proof}
Define \pext\ using (\ref{pextpm}).
Then Lemma~\ref{lem-pp} gives (\ref{pexto}),
(\ref{pextru}) and (\ref{pextlu}).

To define \extNM,  
we first show the equivalence of two likely definitions.
\begin{align*}
\joinNM \oo \mapNM\ f &= \extM\ \prd \oo \mapM\ (\mapN\ f)
  \tag{\ref{MC}} \\[-0.5ex] 
  &= \extM\ (\prd \oo \mapN\ f) = \extM\ (\pext\ f)
  \tag{\ref{exto}M, \ref{pextpm}} 
\end{align*}
So we define \extNM\ so that (\ref{MJ8}NM) and (\ref{EC}) hold,
and define \oNM\ using (\ref{omext}NM), from which (\ref{extom}NM) follows.
% Now if we define $\extNM\ f = \joinNM \oo \mapNM\ f$ 
%
\begin{align*}
\mbox{(\ref{pextfun}):} \qquad
\pext\ & (g \oNM f) = \pext\ (\extNM\ g \oo f) \tag{\ref{omext}NM} \\[-0.5ex]
  & = \prd \oo \mapN\ (\joinNM \oo \mapNM\ g \oo f)
    \tag{\ref{pextpm}, \ref{MJ8}NM} \\[-0.5ex]
  & = \joinNM \oo \prd \oo \mapN\ (\mapNM\ g \oo f)
    \tag{\ref{MJ2}N, P(4)} \\[-0.5ex]
  & = \joinNM \oo \mapNM\ g \oo \prd \oo \mapN\ f
    \tag{\ref{MJ2}N, P(1)} \\[-0.5ex]
  & = \extNM\ g \oo \pext\ f \tag{\ref{MJ8}NM, \ref{pextpm}} \\[-0.5ex]
  & = \extM\ (\pext\ g) \oo \pext\ f = \pext\ g \oM \pext\ f
    \tag{\ref{EC}, \ref{omext}M} 
\end{align*}

\comment{ 
(\ref{pextfun}): Then, using (\ref{MJ8}NM), from P(1) and P(4) we easily get
$\prd \oo \mapN\ (\extNM\ f) = \extNM\ f \oo \prd$.
Using (\ref{pexto}) then gives 
$\pext\ (\extNM\ f \oo g) = \extNM\ f \oo \pext\ g$.
Then (\ref{PE}), (\ref{omext}NM) and (\ref{omext}M) give (\ref{pextfun}).
}

Thus Theorem~\ref{thm-pext-k} applies and so 
\extNM, \oNM\ and \unitNM\ are functions of a monad $NM$.
To show that \joinNM\ and \mapNM\ are the \join\ and \map\ functions of this
monad, we need (\ref{joinext}) and (\ref{mapext}) for $NM$.

Since (\ref{joinext}NM) is clear from (\ref{MJ8}NM),
it remains to show (\ref{mapext}NM).
\begin{align*}
\extNM\ (\unitNM \oo f) & = \extM\ (\pext\ \unitNM \oo \mapN\ f) 
    \tag{\ref{EC}, \ref{pexto}} \\[-0.5ex] 
  & = \extM\ (\unitM \oo \mapN\ f)  \tag{\ref{pextlu}} \\[-0.5ex] 
  & = \mapM\ (\mapN\ f) = \mapNM\ f \tag{\ref{mapext}M, \ref{MC}} 
\end{align*}

% Since we have shown (\ref{extru}) to (\ref{mapext}) for $NM$, $NM$ is a monad.
Finally, (\ref{J1}), and also (\ref{J1S}), follow from
Theorem~\ref{thm-ext-join-iff} for $M$, \ref{ej3} $\Rightarrow$ \ref{ej1}. 
\qed 
\end{proof}

\subsection{Relation between the \textit{dmap} construction and 
  the \textit{dorp} construction of Jones \& Duponcheel} \label{app-dd}

In this subsection, as well as assuming that
$M$ and $N$ are premonads and that (\ref{UC}) and (\ref{MC}) hold,
we further assume that $M$ is a monad.  
Under these assumptions 
Jones \& Duponcheel \cite[\S 3.3,\S 4.2]{jones-composing} 
show that the compound monads $NM$ which can be
defined using \dorp\ and the four rules D(1) to D(4)
are precisely those satisfying (\ref{J2}).
We relate \dorp\ to \dmap\ as shown.
%
\begin{align} 
\dorp \oo \mapNM\ (\mapM\ f) & = \mapNM\ f \oo \dorp\ \tag*{D(1)} \\[-0.5ex]
\dorp \oo \unitNM & = \mapM\ \unitN \tag*{D(2)} \\[-0.5ex]
\dorp \oo \mapNM\ \unitM & = \id \tag*{D(3)} \\[-0.5ex]
\dorp \oo \joinNM & = \joinNM \oo \mapNM\ \dorp\ \tag*{D(4)} \\[1ex]
\dorp & = \dmap\ \id \tag{DD1} \label{DD1} \\[-0.5ex]
\dmap\ f & = \dorp \oo \mapNM\ f \tag{DD2} \label{DD2} 
\end{align}
%
Note that, analogously to Lemma~\ref{lem-pp}(\ref{ppo}), 
(\ref{DD2}) holds iff (\ref{DD1}) and (\ref{G2}) hold.

\begin{theorem}
Assume that $NM$ is a compound monad for which (\ref{J2'}) holds.
Define \djoin\ by (\ref{G9}) or (\ref{DJ}),
and \dmap\ and \dunit\ by (\ref{G10}) and (\ref{DU}).
Then (\ref{DJ}) and (\ref{G1}) to (\ref{G12}) hold.
Further, if \dorp\ is defined by (\ref{DD1}), then 
(\ref{DD2}) and D(1) to D(4) hold.
\end{theorem}

\begin{proof}
(\ref{G11}) holds, using (\ref{MJ3}M).
The equivalence of (\ref{DJ}), that is,
$\djoin\ = \mapM\ \joinN$,
and (\ref{G9}) follows from Lemma~\ref{lem-J2}.
Then $\djoin \oo \dunit\ = \mapM\ \joinN \oo \mapM\ \unitN\ = \id$,
by (\ref{MJ2}M), (\ref{MJ5}N) and (\ref{MJ1}M),
that is, (\ref{G5}) holds.
  % \mapM\ (\joinN \oo \unitN) = \mapM\ \id\ = \id$
Thus the conditions of Theorem~\ref{thm-Grev} are satisfied,
so (\ref{G1}) to (\ref{G8}) also hold, 
as does, by Theorem~\ref{thm-G}, (\ref{G12}).

Now, using (\ref{DD1}), we get (\ref{DD2}) from (\ref{G2}).
Then D(3) is just (\ref{G1}), and D(4) follows from (\ref{G4}),
by (\ref{G8}) and (\ref{extjm}NM).
Using (\ref{DU}), (\ref{G3}) gives D(2).

We prove D(1) by
\begin{align*}
\dorp \oo \mapNM\ (\mapM\ f) & = \dmap\ (\mapM\ f) \tag{\ref{DD2}} \\[-0.5ex]
  & = \extNM\ (\dunit \oo \mapM\ f) \tag{\ref{G10}} \\[-0.5ex]
  & = \extNM\ (\mapNM\ f \oo \dunit) 
    \tag{\ref{MC}, \ref{MJ2}M, \ref{MJ3}N, \ref{DU}} \\[-0.5ex]
  & = \mapNM\ f \oo \extNM\ \dunit 
    \tag{\ref{mapext}NM, \ref{extass}NM} \\[-0.5ex]
  & = \mapNM\ f \oo \dorp \tag*{(\ref{G10}, \ref{DD1}) $\square$}
\end{align*}
\end{proof}

Note that our definition of \dorp\ gives
$\dorp\ = \dmap\ \id\ = \extNM\ \dunit$, which corresponds to 
the definition used in \cite[\S 4.2]{jones-composing}.

Jones \& Duponcheel \cite[\S 3.3]{jones-composing} 
also show how to define a compound monad from a function \dorp,
satifying four rules D(1) to D(4),
assuming that $M$ is a premonad and $N$ is a monad.
They use (\ref{UC}) and (\ref{MC}) as definitions, 
and defining \joinNM\ by
\begin{equation*}
\joinNM = \mapM\ \joinN \oo \dorp \tag{JD} \label{JD}
\end{equation*}
They show that in such a compound monad, (\ref{J2}) holds.
We can prove this theorem via rules (\ref{G1}) to (\ref{G8}) and 
Theorem~\ref{thm-G}.
However in doing so, we have to prove (\ref{MJ4}NM) on the way to 
proving (\ref{G4}) which is rather unsatisfying.

\begin{theorem} \cite[\S 3.3]{jones-composing} 
Let $N$ be a monad and $M$ a premonad. 
Define \unitNM\ and \mapNM\ by (\ref{UC}) and (\ref{MC}).
Define \djoin\ and \dunit\ by (\ref{DJ}) and (\ref{DU}).
Let the function \dorp\ satisfy D(1) to D(4),
and define \dmap\ by (\ref{DD2}).
Define \joinNM\ by (\ref{JD}).
Then $NM$ is a monad satisfying (\ref{G1}) to (\ref{G12}) and (\ref{J2}).
\end{theorem}

\begin{proof} (sketched: also proved in Isabelle).  
Firstly, note that $NM$ is a premonad.
From that fact, using (\ref{DD2}), we can get 
(\ref{DD1}) from (\ref{MJ1}NM),
(\ref{G2}) from (\ref{MJ2}NM),
(\ref{G3}) from (\ref{MJ3}NM) and D(2),
while (\ref{G1}) is just D(3).

(\ref{G5}): Use (\ref{DJ}), (\ref{DU}),
(\ref{MJ2}M), (\ref{MJ5}N) and (\ref{MJ1}M).

(\ref{G6}): Use
(\ref{DJ}), (\ref{UC}), (\ref{G2}), (\ref{G1}), (\ref{MC}),
(\ref{MJ2}M), (\ref{MJ6}N) and (\ref{MJ1}M).

We use (\ref{G8}) as a definition,
noting also that (\ref{MJ8}NM) holds, as
\begin{align*}
\joinNM \oo \mapNM\ f & = \mapM\ \joinN \oo \dorp \oo \mapNM\ f
    \tag{{JD}} \\[-0.5ex]
  & = \djoin \oo \dmap\ f
    \tag{\ref{DJ}, \ref{DD2}} 
\end{align*}

From (\ref{G8}) and (\ref{G1}) we get (\ref{G9}). 

\comment{
(\ref{G7}):
\begin{align}
\djoin \oo \dmap\ \djoin &= \mapM\ \joinN \oo \dmap\ (\mapM\ \joinN) 
    \tag{\ref{DJ}} \\[-0.5ex]
  &= \mapM\ \joinN \oo \mapNM\ \joinN \oo \dorp 
    \tag{\ref{DD2},D1} \\[-0.5ex]
  &= \mapM\ (\joinN \oo \joinN) \oo \dorp 
    \tag{\ref{MC}, \ref{MJ2}M, \ref{MJ7}N} \\[-0.5ex]
  &= \djoin \oo \joinNM\ 
    \tag{\ref{MJ2}M,{JD}} 
\end{align}
TO COMPLETE ie DO G4 
}

To prove (\ref{G4}) and (\ref{G7}) we derive initially
\begin{align*}
\djoin \oo \dmap\ \mapM\ g &= \mapM\ \joinN \oo \mapNM\ g \oo \dorp
    \tag{\ref{DJ}, \ref{DD2}, D(1)} \\[-0.5ex]
  &= \mapM\ (\joinN \oo \mapN\ g) \oo \dorp
    \tag{\ref{MC}, \ref{MJ2}M} \\[-0.5ex]
  &= \mapM\ (\extN\ g) \oo \dorp
    \tag{\ref{MJ8}N} 
\end{align*}

Then, to get (\ref{G7}), we set $g = \joinN$ in this to get,
on the right-hand side,
\begin{align*}
\mapM\ & (\extN\ \joinN) \oo \dorp = \mapM\ (\joinN \oo \joinN) \oo \dorp
    \tag{\ref{MJ7}N, \ref{MJ8}N} \\[-0.5ex]
  &= \djoin \oo \mapM\ \joinN \oo \dorp = \djoin \oo \joinNM\
    \tag{\ref{MJ2}M, \ref{DJ}, {JD}} 
\end{align*}
%
and we set $g = \mapN\ f$ in it to get, by a very similar argument, 
using (\ref{MJ4}N) instead of (\ref{MJ7}N),
$\djoin \oo \dmap\ \mapNM\ f = \mapNM\ f \oo \joinNM$.
Rewriting using (\ref{G8}) and (\ref{MJ8}NM), we have (\ref{MJ4}NM).
Thus the property of $h$ that 
$\joinNM \oo \mapNM\ h = h \oo \joinNM$
holds for $h = \dorp$, by D(4), and for $h = \mapNM\ f$, above.
So it is easy to see that this property holds for their composition,
$h = \dorp \oo \mapNM\ f$, which, again using (\ref{G8}) and (\ref{MJ8}NM),
gives us (\ref{G4}).

Thus Theorem~\ref{thm-G} applies.
As we now have both (\ref{G9}) and (\ref{DJ}), Lemma~\ref{lem-J2}
shows that (\ref{J2}) holds.
\qed
\end{proof}

\subsection{Relation between the \textit{kmap} construction and 
  the \textit{swap} construction of Jones \& Duponcheel} \label{app-ks}

Throughout this section we make the assumptions of \S \ref{app-pp}
and of \S \ref{app-dd}.
That is, we assume that $M$ and $N$ are monads, 
and that (\ref{UC}) and (\ref{MC}) hold.
Under these assumptions 
Jones \& Duponcheel \cite[\S 3.4,\S 4.3]{jones-composing} 
show that the compound monads $NM$ which can be
defined using \swap\ and the four rules S(1) to S(4)
(where \prd\ and \dorp\ are defined in terms of \swap\ as shown)
are precisely those satisfying (\ref{J1}) and (\ref{J2}).
%
\begin{align*} 
\swap \oo \mapN\ (\mapM\ f) & = \mapNM\ f \oo \swap\ \tag*{S(1)} \\[-0.5ex]
\swap \oo \unitN & = \mapM\ \unitN \tag*{S(2)} \\[-0.5ex]
\swap \oo \mapN\ \unitM & = \unitM \tag*{S(3)} \\[-0.5ex]
\prd \oo \mapN\ \dorp & = \dorp \oo \prd \tag*{S(4)} 
\end{align*}
%
\begin{align*}
\prd & = \mapM\ \joinN \oo \swap &
\dorp & = \extM\ \swap
\end{align*}
%
\setcounter{equation}{0}%
\renewcommand\theequation{KS\arabic{equation}}%
\begin{align} 
\label{SK} \swap & = \kmap\ \id \\[-0.5ex]
\label{kmapsm} \kmap\ f & = \swap \oo \mapN\ f \\[-0.5ex]
\tag{\ref{kmapo}} \kmap\ (g \oo f) & = \kmap\ g \oo \mapN\ f 
\end{align} 

Note that, analogously to Lemma~\ref{lem-pp}(\ref{ppo}), 
(\ref{kmapsm}) holds iff (\ref{SK}) and (\ref{kmapo}) hold.
%
\begin{theorem} \label{thm-swap}
With the assumptions and definitions of Theorem~\ref{thm-both},
further define \swap\ from \kmap\ by (\ref{SK}).
Then S(1) to S(4) hold.
\comment{
Then (\ref{kmapo}), (\ref{kmapsm}), and xx hold.
\begin{quote}
\begin{tabular}{l@{\qquad}r@{\ \ }c@{\ \ }l}
\textbf{(\kmapo)} & \kmap\ (g \oo f) & = & \kmap\ g \oo \mapN\ f \\
\textbf{(\kmapsm)} & \kmap\ f & = & \swap \oo \mapN\ f \\
\textbf{(\Jts)} & \extNM\ \unitM & = & \mapM\ \joinN \\
\textbf{(\kjoinuj)} & \kjoin & = & \unitM \oo \joinN \\
\textbf{(\extkmap)} & \extNM\ f & = & \extM\ (\mapM\ \joinN \oo \kmap\ f) \\
\textbf{(xx)} & \kmap\ f & = & \pext\ (\mapM\ \unitN \oo f) 
\end{tabular}
\end{quote}
}
\end{theorem} 

\begin{proof}
By Lemma~\ref{lem-J1}, Theorem~\ref{thm-when-pext} applies.
So by Lemma~\ref{lem-pko}, (\ref{kmapo}) and so (\ref{kmapsm}) hold.
So S(3) is just (\ref{KMJ1}).
Now by (\ref{mapext}K), (\ref{omext}M) and (\ref{DUK}),
$\kmap\ f = \pext\ (\unitNM \oM f) = \pext\ (\dunit \oo f)$,
so $\swap\ = \pext\ \dunit$ and, by (\ref{pextru'}),
$\swap \oo \unitN\ = \dunit$ and S(2) follows.

We show S(1), after simplifying it using (\ref{kmapsm}), as follows:
%
\begin{align*}
% \text{for S(1):} \quad
\kmap\ (\mapM\ f) &= \kmap\ ((\unitM \oo f) \oM id) 
    \tag{\ref{mapext}M, \ref{extom}M} \\[-0.5ex] 
  &= \kmap\ (\unitM \oo f) \oM \kmap\ \id \tag{\ref{KMJ2}} \\[-0.5ex] 
  &= (\kmap\ \unitM \oo \mapN\ f) \oM \swap\ 
    \tag{\ref{kmapo}, \ref{SK}} \\[-0.5ex] 
  &= \extM\ (\unitM \oo \mapN\ f) \oo \swap\ 
    \tag{\ref{MJ1}K, \ref{omext}M} \\[-0.5ex] 
  % &= \mapM\ (\mapN\ f) \oo \swap\ 
    % \tag{\ref{MJ1}K, \ref{omext}M, \ref{mapext}M} \\[-0.5ex] 
  &= \mapNM\ f \oo \swap \tag{\ref{mapext}M, \ref{MC}} 
\end{align*}
% S(1) follows from this by (\ref{kmapsm}).
%
Now, for S(4) we first use our definitions of \dorp\ and \prd.
By \eqref{DD1} and \eqref{DMK}, $\dorp\ = \extM\ (\kmap\ \id)$,
and by (\ref{mapext}K) let $\kmap\ \id$ be $\pext\ g$, so we have
% show $\pext\ \dorp = \dorp \oo \prd$ by
%
\begin{align*}
\prd \oo \mapM\ \dorp & = \pext\ (\extM\ (\kmap\ \id)) 
    \tag{\ref{pextpm}} \\[-0.5ex] 
  & = \pext\ (\pext\ g \oM \id) \tag{\ref{extom}M} \\[-0.5ex] 
  & = \pext\ g \oM \pext\ \id \tag{\ref{extass}K} \\[-0.5ex] 
  % & = \kmap\ \id \oM \prd = \extM\ (\kmap\ \id) \oo \prd
  & = \extM\ (\kmap\ \id) \oo \prd
    \tag{\ref{prdpext}, \ref{omext}M} 
\end{align*}

Finally, to show S(4) precisely as it is stated,
we need to check that the various definitions of \prd\ and \dorp\
are consistent.
By our definitions, 
\begin{align*}
\prd & = \pext\ \id\ = \kjoin \oM \kmap\ \id 
    \tag{\ref{prdpext}, \ref{MJ8}K} \\[-0.5ex] 
  & = \extM\ \kjoin \oo \swap = \mapM\ \joinN \oo \swap
    \tag{\ref{omext}M, \ref{SK}, \ref{DJK}, \ref{DJ}} \\[1ex]
\dorp & = \dmap\ \id\ = \extM\ (\kmap\ \id) = \extM\ \swap
    \tag{\ref{DD1}, \ref{DMK}, \ref{SK}} 
\end{align*}
so our definitions are consistent with those used above in stating S(4).
\qed
\comment{
\begin{description}
\mditem[(\kmapo)] By (\pexto) and (\omoass),
\textit{
\pext\ (\unitNM \oM (g \oo f)) = 
\pext\ (\unitNM \oM g) \oo \mapN\ f}.
That is, 
\textit{ \kmap\ (g \oo f) = \kmap\ g \oo \mapN\ f}.

\mditem[(\kmapsm)] By (\swapkmap), 
this is the special case $g = \id$ of (\kmapo).

\item[(\Jts)] 
By Theorem~\ref{thm-ext-join-iff}, \ref{ej1} $\Rightarrow$ \ref{ej2}, 
we need
\textit{\mapM\ \joinN \oo \unitNM\ = \unitM}: using (\ref{UC})
this is 

\textit{
\begin{tabular}{rcl@{\qquad}r}
\mapM\ \joinN \oo \unitM \oo \unitN & = & 
\unitM \oo \joinN \oo \unitN & (\textup{MJ3 for} M) \\
& = & \unitM & (\textup{MJ5 for} N) 
\end{tabular} }

\item[(\kjoinuj)] ~

\textit{
\begin{tabular}{rcl@{\qquad}r}
\kjoin &=& \pext\ \unitM\ = \extNM\ \unitM \oo \unitM & (\pextext) \\
  &=& \mapM\ \joinN \oo \unitM\ = \unitM \oo \joinN & (\Jts, 
  \textup{MJ3 for} M)
\end{tabular} }

\item[(\extkmap)] ~

\textit{
\begin{tabular}{rcl@{\qquad}r}
\extNM\ f &=& \extM\ (\pext\ f) = \extM\ (\kjoin \oM \kmap\ f) &
  (\extcomp, pext-kjm)\\
  &=& \extM\ (\mapM\ \joinN \oo \kmap\ f) & (\omext, \mapext)
\end{tabular} }


\end{description}
}
\end{proof}

We showed in the proof above that $\swap\ = \pext\ \dunit$ 
which is consistent with the definition of \swap\ used in 
\cite[\S4.3]{jones-composing}.

\comment{
We can set $f = id$ in (\extkmap) 
to get \textit{\joinNM\ = ext\M\ (\mapM\ \joinN \oo \swap)},
and also in (\kmappext), using (\ref{UC}), (\omext) and (\mapext), to get
\textit{\swap\ = \pext\ (\mapM\ \unitN)},
which are used/proved in \cite[\S3.4,\S4.3]{jones-composing}.
This shows that the \swap\ and \kmap\ constructions give the same compound
monad.

It is also straightforward to prove the results S(2) to S(4) of
\cite[\S3.4]{jones-composing}, and S(1) follows from (S1e) above.
Using \textit{\swap\ = \pext\ (\mapM\ \unitN)} (above), 
S(2) is just (\pextru-N), and by (\kmapsm), S(3) is (\ref{KMJ1}).
Tracing definitions of the function \dorp\ used in S(4) shows that 
S(4) is a special case of (\P14) above.
}

Conversely, from S(1) to S(4), (\ref{kmapsm}) and (\ref{KJ})
it is possible to prove the rules of (\ref{KMJ1}) to (\ref{KMJ7}) directly.
These proofs have been done in Isabelle, see \cite{prfs}, 
functor \verb|fromSwap|.
Alternatively, see Jones \& Duponcheel \cite[\S 3.4]{jones-composing} 
for proofs from S(1) to S(4) that $NM$ is a monad. 

Another interesting result is that both sides of S(4) equal 
$\swap \oNM \swap$. The key step to prove it is to modify the proof of S(4)
above, to give 
%
\begin{align*}
\prd \oo \mapM\ \dorp 
  & = \pext\ (\pext\ g \oM \id) \tag{as above} \\[-0.5ex] 
  & = \pext\ (\pext\ g) \oM \kmap\ \id \tag{\ref{exto}K} \\[-0.5ex] 
  & = \pext\ \swap \oM \swap = \swap \oNM \swap 
    \tag{\ref{SK}, \ref{omext}K} 
\end{align*}

\subsection{A distributive law for monads} \label{app-dl}
Manes \cite{manes} describes a ``distributive law'' for monads,
at Chapter~4, pages 311-2, Definition~3.6, and 
page~334, Exercise~6.
His natural transformation $\lambda$ is also the polymorphic function \swap. 
Translating his rules into our terminology, we have
%
\setcounter{equation}{0}
\renewcommand\theequation{DL\arabic{equation}}
\begin{align}
\swap \oo \unitN & = \mapM\ \unitN \label{DL1} \\[-0.5ex]
\mapM\ \joinN \oo \swap \oo \mapN\ \swap & = \swap \oo \joinN 
  \label{DL2} \\[-0.5ex]
\swap \oo \mapN\ \unitM & = \unitM \label{DL3} \\[-0.5ex]
\swap \oo \mapN\ \joinM & = \joinM \oo \mapM\ \swap \oo \swap \label{DL4} 
\end{align}

Of these, (\ref{DL1}) and (\ref{DL2}) are the diagrams in Definition~3.16, 
and (\ref{DL3}) and (\ref{DL4}) are the diagrams in Exercise~6 on page~334. 
He additionally specifies that \swap\ is a natural transformation.

\begin{theorem} \label{thm-dl}
With the assumptions and definitions of Theorem~\ref{thm-swap},
(\ref{DL1}) to (\ref{DL4}) hold and \swap\ is a natural transformation.
\end{theorem} 

\begin{proof}
From Theorem~\ref{thm-swap} we have S(1) to S(4).
That \swap\ is a natural transformation is just S(1),
and (\ref{DL1}) and (\ref{DL3}) are just S(2) and S(3).
We can translate (\ref{DL4}) to
$\kmap\ (\id \oM \id) = \kmap\ \id \oM \kmap\ \id$,
an instance of (\ref{MJ2}K).
To prove (\ref{DL2}),
we have, by Theorem~\ref{thm-ext-join-iff} for \KM,
\ref{ej3} $\Rightarrow$ \ref{ej1}, and (\ref{mapext}K), 
\begin{align*}
\pext\ (\kmap\ \id) & = \kmap\ \id \oM \kjoin 
     \\[-0.5ex]
  & = \kmap\ \id \oM \unitM \oo \joinN 
    \tag{\ref{KJ}, \ref{omoass}M} \\[-0.5ex]
  & = \swap \oo \joinN \tag{\ref{SK}, \ref{krid}M} 
\end{align*}
Now $\pext\ (\kmap\ \id) = \prd \oo \mapN\ \swap$
which is, by the expression for \prd\ in \S \ref{app-ks} above,
equal to the left-hand side of (\ref{DL2}).
\qed
\end{proof}

Conversely, from S(1) and (\ref{DL1}) to (\ref{DL4}), 
(\ref{kmapsm}) and (\ref{KJ})
it is possible to prove the rules of (\ref{KMJ1}) to (\ref{KMJ7}) directly.
These proofs have been done in Isabelle, see \cite{prfs},
functors \verb|fromSextDL| and \verb|fromSextF|.

\section{Examples of the Compound Monad Constructions}

\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
(\ref{UC}) and (\ref{ompext}).
Then we prove the \pext\ axioms (\ref{pextru}) to (\ref{pextfun}) as follows.
(\ref{pextru}) is just (\pextOk).
Using the definitions just mentioned, we get (\ref{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 (\ref{omext}M) we get (\ref{pextfun}) from

\begin{center} \textit{
\begin{tabular}{rcl@{\qquad}r}
pext (g \oEM\ f) (Ok a) & = & (pext g \oM f) a & (\pextOk, \ref{ompext}) \\
  & = & ext\M\ (pext g) (f a) & (\ref{omext}M) \\
& = & ext\M\ (pext g) (pext f (Ok a)) & (\pextOk) \\
& = & (pext g \oM pext f) (Ok a) & (\ref{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)) & (\ref{extru}) \\
& = & ext\M\ (pext g) (pext f (Err msg)) & (\pextErr) \\
& = & (pext g \oM pext f) (Err msg) & (\ref{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{ex-comp-rdr}.
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,
  (\ref{pextru}) to (\ref{pextfun}), 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 available at \cite{prfs}, or 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, and they give proofs of this.
We also have Isabelle proofs of the \pext\ axioms for the compound list monad.