\section{Compound Monad Constructions}
\label{sec-cmc}

If type constructors $M$ and $N$, with associated functions, are 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 constructions for compound monads
and discuss the rules that need to be satisfied in each case.

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

Let $M$ be a monad, and consider compound monads
where the compound monad type is $(\alpha N) M$,
which we will just write as $\alpha N M$.
To define a compound monad $NM$, we will need a function \extNM,
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 
\pext\ which does part of this job:
\begin{align*}
\extNM & : (\alpha \to \beta N M) \to (\alpha N M \to \beta N M) \\
\pext & : (\alpha \to \beta N M) \to (\alpha N \to \beta N M) 
\end{align*}
Rules (\ref{pextru}) to (\ref{pextfun}) are sufficient to define
a compound monad using such a function \pext.
We assume nothing about the functions \oNM\ or \unitNM,
except that they have the appropriate types.
We need not assume that $N$ is a monad, although in many examples
rules (\ref{pextru}) to (\ref{pextfun}) are proved to hold for any monad $M$,
when setting $M$ to the identity monad gives a monad $N$.
%
\comment{
\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 \oM\ \unitNM & = & f & (\pextru) \\
pext \unitNM & = & \unitM & (\pextlu) \\
pext (g \oNM\ f) & = & pext g \oM\ pext f & (\pextfun) \\[2ex]
\kjoin & = & \pext\ \unitM & (kjoin-pext) \\ 
\kmap\ f & = & \pext\ (\unitNM\ \oM\ f) & (kmap-pext)  
\end{tabular}
} \end{center} 
\end{table}
}
%
\setcounter{equation}{0}
\renewcommand\theequation{E\arabic{equation}K}
\begin{eqnarray} % \label{tab-prules} was (\ref{pextru}) to (\ref{pextfun})
\label{pextru} \pext\ f \oM \unitNM & = & f \\[-0.5ex]
\label{pextlu} \pext\ \unitNM & = & \unitM \\[-0.5ex]
\label{pextfun} \pext\ (g \oNM f) & = & \pext\ g \oM \pext\ f \\[1ex]
% \stepcounter{equation} not when using (E3a)
\label{kjoin-pext} \kjoin & = & \pext\ \unitM \\ [-0.5ex]
\label{kmap-pext} \kmap\ f & = & \pext\ (\unitNM \oM f) \\[1ex] 
\label{ompext} g \oNM f & = & \pext\ g \oM f 
\end{eqnarray}

By comparing (\ref{pextru}) to (\ref{pextfun}) with
(\ref{extru}) to (\ref{extfun})
we see that we have the three rules needed for a monad $N$
{in \KM, the Kleisli category of $M$}.
We will refer to this monad as \NKM.
Thus the treatment of a single monad described in 
\S\ref{sec-intro}, \S\ref{sec-monrules}
and \S\ref{sec-mrkleisli} applies to this monad.
We define the counterparts of \map\ and \join, calling them \kmap\ and \kjoin:
note how rules (\ref{kjoin-pext}) and (\ref{kmap-pext}) 
correspond to (\ref{joinext}) and (\ref{mapext}).
As in \S\ref{sec-monrules}, we deduce (\ref{ompext}), giving 
\oNM\ in tems of \pext.
The various functions and theorems involved have counterparts 
of which examples are tabulated below, % Table~\ref{tab-corresp},
where the left-hand side shows the standard
treatment (set out as for a monad $N$),
and the right-hand side shows the monad \NKM\ in \KM.
% 
\begin{align*}
id &: \alpha \to \alpha  & \unitM &: \alpha \to \alpha M  \\[-0.5ex]
\unitN &: \alpha \to \alpha N  & \unitNM &: \alpha \to \alpha N M  \\[-0.5ex]
\mapN &: (\alpha \to \beta) \to \alpha N \to \beta N  &
\kmap &: (\alpha \to \beta M) \to \alpha N \to \beta N M  \\[-0.5ex]
\joinN &: \alpha N N \to \alpha N  & 
\kjoin &: \alpha N N \to \alpha N M  \\[-0.5ex]
\extN &: (\alpha \to \beta N) \to \alpha N \to \beta N  &  
\pext &: (\alpha \to \beta N M) \to \alpha N \to \beta N M  \\[-0.5ex]
\extN\ g &= g \oN \id & \pext\ g &= g \oNM \unitM \\[-0.5ex]
g \oN f &= \extN\ g \oo f & g \oNM f &= \pext\ g \oM f \\[-0.5ex]
\joinN &= \extN\ id & 
\kjoin &= \pext\ \unitM \\[-0.5ex] 
\mapN\ f &= \extN\ (\unitN \oo f) & 
\kmap\ f &= \pext\ (\unitNM \oM f) \\[-0.5ex] 
\extN\ f &= \joinN \oo \mapN\ f & 
\pext\ f &= \kjoin \oM \kmap\ f \\[-0.5ex] 
h \oN f &= (h \oN id) \oo f &
h \oNM f &= (h \oNM \unitM) \oM f % \\[-0.5ex] 
\end{align*}

We will refer to the rules and results about this monad 
by putting ``K'' after the names used in \S \ref{sec-intro} and \S
\ref{sec-single}.
We also obtain rules (\ref{KMJ1}) to (\ref{KMJ8})
which are the counterparts of (\ref{MJ1}) to (\ref{MJ8}).
Then, just as in \S\ref{sec-intro}, these seven rules,
with \pext\ and \oNM\ defined from \kjoin\ and \kmap\
by (\ref{MJ8}K) and (\ref{omext}K),
are sufficient to show rules (\ref{pextru}) to (\ref{pextfun})
and the converse definitions of \kjoin\ and \kmap\ in terms of \pext,
(\ref{kjoin-pext}) and (\ref{kmap-pext}).

This monad \NKM\ in \KM, the Kleisli category for $M$,
gives rise to a further Kleisli category,
which we may describe as the Kleisli category for \NKM\ in \KM.
%the Kleisli category for $M$.
Its identity is \unitNM\ and its composition function is \oNM.
Note also that the two rules (\ref{pextlu}) and (\ref{pextfun})
express the fact that \pext\ is (the action on arrows of) a functor,
from this compound Kleisli category to \KM. %the Kleisli category for $M$.
%
\comment{
\begin{table}%[!hbt]
\caption{Correspondence between presentation of a monad $N$ in \T\ and in \KM}
\label{tab-corresp}
\begin{center} \textit{
\begin{tabular}{rcl@{}rcl}
id &:& $\alpha \to \alpha $ & \unitM &:& $\alpha \to \alpha M $ \\
\unitN &:& $\alpha \to \alpha N $ & \unitNM &:& $\alpha \to \alpha N M $ \\
\mapN &:& $(\alpha \to \beta) \to \alpha N \to \beta N $ &
\kmap &:& $(\alpha \to \beta M) \to \alpha N \to \beta N M $ \\
\joinN &:& $\alpha N N \to \alpha N $ & 
\kjoin &:& $\alpha N N \to \alpha N M $ \\
\extN &:& $(\alpha \to \beta N) \to \alpha N \to \beta N $ &  
\pext &:& $(\alpha \to \beta N M) \to \alpha N \to \beta N M $ \\
\extN\ g &=& g \oN\ \id & \pext\ g &=& g \oNM\ \unitM \\
g \oN\ f &=& \extN\ g \oo\ f & g \oNM\ f &=& \pext\ g \oM\ f \\
\joinN & = & \extN\ id & 
\kjoin & = & \pext\ \unitM \\ 
\mapN\ f & = & \extN\ (\unitN\ \oo\ f) & 
\kmap\ f & = & \pext\ (\unitNM\ \oM\ f) \\ 
\extN\ f & = & \joinN\ \oo\ \mapN\ f & 
\pext\ f & = & \kjoin\ \oM\ \kmap\ f \\ 
h \oN\ f & = & (h \oN\ id) \oo\ f &
h \oNM\ f & = & (h \oNM\ \unitM) \oM\ f % \\ 
% h \oN\ (g \oo\ f) & = & (h \oN\ g) \oo\ f &
% h \oNM\ (g \oM\ f) & = & (h \oNM\ g) \oM\ f \\ 
% &&&&& 
\end{tabular}
} \end{center} 
\end{table}
}
%
\comment{
\begin{table}%[!hbt]
\caption{Kleisli category monad rules for \unitNM, \kmap\ and \kjoin}
\label{tab-kmjrules}
\begin{center} \textit{
\begin{tabular}{rcl@{\qquad\qquad}r}
kmap \unitM\ & = &  \unitM\ & \textup{(KMJ1)} \\
kmap f \oM\ kmap g & = &  kmap (f \oM\ g) & \textup{(KMJ2)} \\
\unitNM\ \oM\ f & = &  kmap f \oM\ \unitNM\ & \textup{(KMJ3)} \\
kjoin \oM\ kmap (kmap f) & = &  kmap f \oM\ kjoin  & \textup{(KMJ4)} \\
kjoin \oM\ \unitNM\ & = &  \unitM\ & \textup{(KMJ5)} \\
kjoin \oM\ kmap \unitNM\ & = &  \unitM & \textup{(KMJ6)} \\
kjoin \oM\ kmap kjoin & = &  kjoin \oM\ kjoin  & \textup{(KMJ7)} \\[2ex]
pext f & = & kjoin \oM\ kmap f & (pext-kjm) 
\end{tabular}
} \end{center} 
\end{table}
}%
%
\setcounter{equation}{0}%
\renewcommand\theequation{\arabic{equation}K}%
\begin{eqnarray} % \label{tab-kmjrules} was (\ref{KMJ1}) to (\ref{KMJ8})
\kmap\ \unitM & = &  \unitM \label{KMJ1} \\[-0.5ex]
\kmap\ f \oM \kmap\ g & = &  \kmap\ (f \oM g) \label{KMJ2} \\[-0.5ex]
\unitNM \oM f & = &  \kmap\ f \oM \unitNM \label{KMJ3} \\[-0.5ex]
\kjoin \oM \kmap\ (\kmap\ f) & = &  \kmap\ f \oM \kjoin
  \label{KMJ4} \\[-0.5ex]
\kjoin \oM \unitNM & = &  \unitM \label{KMJ5} \\[-0.5ex]
\kjoin \oM \kmap\ \unitNM & = &  \unitM \label{KMJ6} \\[-0.5ex]
\kjoin \oM \kmap\ \kjoin & = &  \kjoin \oM \kjoin\  \label{KMJ7} \\[1ex]
pext f & = & kjoin \oM \kmap\ f \label{pext-kjm} \label{KMJ8} 
\end{eqnarray}%
%
This monad can also be characterised by four rules analogous to 
(\ref{krid}) to (\ref{omoIass}):
that is, the rules (\ref{krid}K) to (\ref{omoIass}K).
We also show (\ref{extom}K) and (\ref{omoass}K).
%
\setcounter{saveeqn}{\value{equation}}
\setcounter{equation}{0}
\renewcommand\theequation{A\arabic{equation}K}
\begin{align} 
% \label{tab-assNMrules} was (\ref{kridK}) to (\ref{oNMoMouass})
f \oNM \unitNM & = f \label{kridK} \\[-0.5ex]
\unitNM \oNM f & = f \label{klidK} \\[-0.5ex]
h \oNM (g \oNM f) & = (h \oNM g) \oNM f \label{kassK} \\[-0.5ex]
(h \oNM \unitM) \oM f & = h \oNM f 
  \label{oNMoMouass} \\[1ex] 
\pext\ g & = g \oNM \unitM \\
(h \oNM g) \oM f & = h \oNM (g \oM f) 
\end{align}
%
\comment{
\begin{table}%[!hbt]
\caption{Identity and associativity rules for $NM$} 
\label{tab-assNMrules}
\begin{center} \textit{
\begin{tabular}{rcl@{\qquad\qquad}r}
\unitNM\ \oNM\ f & = & f & (\klid\NM) \\
f \oNM\ \unitNM & = & f & (\krid\NM) \\
h \oNM\ (g \oNM\ f) & = & (h \oNM\ g) \oNM\ f & (\kass\NM) \\[2ex]
(h \oNM\ \unitM) \oM\ f & = & h \oNM\ f & (\oNMoMouass) \\ 
(h \oNM\ id) \oo\ f & = & h \oNM\ f & (\omoIass\NM) \\
(h \oM\ id) \oo\ f & = & h \oM\ f & (\omoIass\M) 
\end{tabular}
} \end{center} 
\end{table}
}%
%
Now, to show that $NM$ is a compound monad, we also need to show 
four rules analogous to (\ref{krid}) to (\ref{omoIass}),
namely (\ref{krid}NM) to (\ref{omoIass}NM).
Of these, the first three, (\ref{krid}NM) to (\ref{kass}NM),  
are the same as (\ref{kridK}) to (\ref{kassK});
only (\ref{omoIass}NM) is different.
So to show that $NM$ (defined by \unitNM\ and \oNM) is a monad, 
we need only show (\ref{omoIass}NM), and to do this we have available
both (\ref{oNMoMouass}) and (\ref{omoIass}M).
\begin{align}
(h \oNM id) \oo f & = h \oNM f \tag{\ref{omoIass}NM} \\[-0.5ex]
(h \oM id) \oo f & = h \oM f \tag{\ref{omoIass}M}
\end{align}

\begin{theorem} \label{thm-pext-k}
Assume that $M$ is a monad and that functions \pext, \oNM and \unitNM\ 
of the appropriate types are given,
satisfying rules (\ref{pextru}) to (\ref{pextfun}).
Then \oNM\ and \unitNM\ define a monad, and,
using (\ref{extom}NM) to define \extNM, 
\begin{align}
% \label{ompext} g \oNM\ f & = \pext\ g \oM\ f \\
\label{EC} \extNM\ f & = \extM\ (\pext\ f) \tag{EC} \\
\label{PE} \pext\ f & = \extNM\ f \oo \unitM \tag{PE} \\
\label{J1S} \extM\ (\extNM\ f) & = \extNM\ f \oo \joinM \tag{J1S} 
% \label{pextcong} \pext\ f = \pext\ g & \Rightarrow f = g \\
\end{align}
\end{theorem}

\begin{proof}
Rules (\ref{pextru}) to (\ref{pextfun}) establish that \pext, \oNM\ and \unitNM\
define a monad in \KM, and so rules
(\ref{kridK}) to (\ref{oNMoMouass}) are satisfied. 
Since $M$ is a monad, (\ref{omoIass}M) holds, and so we use (\ref{omoIass}M)
and (\ref{oNMoMouass}) to show (\ref{omoIass}NM) as follows:
%
\begin{align*}
(h \oNM id) \oo f &= ((h \oNM \unitM) \oM id) \oo f 
    \tag{\ref{omoIass}K} \\[-0.5ex]
  &= (h \oNM \unitM) \oM f = h \oNM f
    \tag{\ref{omoIass}M, \ref{omoIass}K}
\end{align*}

\begin{description}

\mditem[(\ref{EC}):]
By (\ref{extom}M) and (\ref{extom}NM) this is (\ref{omext}K). 

\mditem[(\ref{PE}):] By (\ref{omext}NM) this is (\ref{extom}K). 

\mditem[(\ref{J1S}):] 
By Theorem~\ref{thm-ext-join-iff} for $M$, \ref{ej3} $\Rightarrow$ \ref{ej1}, 
this follows from (\ref{EC}).
\qed
\end{description}
\end{proof}

In Theorem~\ref{thm-pext-k} we proved
rules (\ref{krid}) to (\ref{omoIass}) for $NM$,
so proving that $NM$ is a monad.
However, we note that it is also trivial to prove rules 
(\ref{extru}) to (\ref{extfun}) for $NM$.
In fact, using (\ref{EC}),
each rule for $NM$ follows from the same rule for $M$ 
and the corresponding rule from among (\ref{pextru}) to (\ref{pextfun}).

\comment{
At this point we have, by (\UC) 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 rules (\ref{pextru}) to (\ref{pextfun}).
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 a necessary condition, 
namely that (\ref{J1S}) holds.
In fact, this condition is also sufficient.
% since (\extcomp) 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
% \textbf{(\UC)} & \unitNM\ & = & \unitM\ \oo\ \unitN \\
% \textbf{(\J1S)} & \ext\M\ (\ext\NM\ f) & = & \ext\NM\ f \oo\ \join\M
(\ref{J1S}) (see Theorem~\ref{thm-pext-k}) holds.
Then \oNM\ also defines a monad in the category \KM,
and, using (\ref{PE}) to define \pext, (\ref{EC}) holds.
\end{theorem}

\begin{proof}
We need to show that \oNM\ satisfies
the four rules (\ref{krid}K) to (\ref{omoIass}K).
Now (\ref{krid}K) to (\ref{kass}K) are the same as
(\ref{krid}NM) to (\ref{kass}NM), which hold as $NM$ is a monad. 
% We have the first three since $NM$ is a monad, so we need only the fourth,
So we need only (\ref{omoIass}K),
which we show follows from (\ref{J1S}).
\begin{align*}
(h \oNM \unitM) \oM f & = \extM\ (\extNM\ h \oo \unitM) \oo f 
    \tag{\ref{omext}NM, \ref{omext}M} \\[-0.5ex]
  & = \extM\ (\extNM\ h) \oo \mapM\ \unitM \oo f 
    \tag{\ref{exto}M} \\[-0.5ex]
  & = \extNM\ h \oo \joinM \oo \mapM\ \unitM \oo f 
    \tag{\ref{J1S}} \\[-0.5ex]
  & = \extNM\ h \oo f = h \oNM f \tag{\ref{MJ6}M, \ref{omext}NM} 
\end{align*}
\comment{
We need to show 
\textit{(h \oNM\ \unitM) \oM\ f = h \oNM\ f},
that is 
\textit{\extM\ (\extNM\ h \oo\ \unitM) \oo\ f = \extNM\ h \oo\ f},
where the left-hand side is
\textit{\extM\ (\extNM\ h) \oo\ \mapM\ \unitM\ \oo\ f}
so the result follows from (\ref{J1S}) and (\ref{MJ6}).
}

Then $NM$ is a monad in which \pext\ is defined by (\ref{extom}K);
but, by (\ref{omext}NM), this is equivalent to (\ref{PE}).
Then (\ref{EC}) follows from Theorem~\ref{thm-pext-k}
(alternatively, from (\ref{J1S}) by Theorem~\ref{thm-ext-join-iff} for $M$,
\ref{ej1} $\Rightarrow$ \ref{ej2}).  
\qed
\end{proof}

This shows that, given a monad $M$, that the compound monads $NM$ 
obtainable using the construction via a monad $N$ in \KM\ are precisely
the monads $NM$ such that (\ref{J1S}) is satisfied.


\subsection{Relation to the \textit{prod} construction of Jones \& Duponcheel}
\label{sec-jdprod}

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

Jones \& Duponcheel \cite{jones-composing} consider only 
compound monads which satisfy (\ref{UC}) and (\ref{MC}).
Note that, as shown in \cite[\S 3]{jones-composing},
when $M$ and $N$ are premonads and (\ref{UC}) and (\ref{MC})
hold, then $NM$ is a premonad.
Assuming that $M$ is a monad and that $N$ is a premonad,
they show how to define a compound monad given a function \prd,
satisfying four rules P(1) to P(4) (see Appendix~\ref{app-pp}),
and show that the compound monads $NM$ which can be
defined using \prd\ are precisely those satisfying (\ref{J1})
(which is the case $f = \id$ of (\ref{J1S})).
In fact (\ref{MC}) and (\ref{J1}) are sufficient to imply (\ref{J1S}).
%
\begin{align}
\unitNM\ f & = \unitM\ (\unitN\ f) \label{UC} \tag{UC} \\
\mapNM\ f & = \mapM\ (\mapN\ f) \label{MC} \tag{MC} \\
\extM\ \joinNM & = \joinNM \oo \joinM \label{J1} \tag{J1}
\end{align} 

\begin{lemma} \label{lem-J1}
If $M$ and $NM$ are monads,
then (\ref{MC}) and (\ref{J1}) imply (\ref{J1S}).
\end{lemma}

\begin{proof}
By Theorem~\ref{thm-ext-join-iff} for $M$, \ref{ej1} $\Rightarrow$ \ref{ej3}, 
we can assume, from (\ref{J1}), that $\joinNM = \extM\ 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 $\extNM\ f = \extM\ h$.
%
\begin{align*}
\extNM\ f & = \joinNM \oo \mapNM\ f \tag{\ref{extjm}NM} \\[-0.5ex]
           & = \extM\ g \oo \mapM\ (\mapN\ f) \tag{\ref{MC}} \\[-0.5ex]
	   & = \extM\ (g \oo \mapN\ f) \tag*{(\ref{exto}M) $\square$}
\end{align*}
\end{proof}

Thus the \pext\ construction is applicable whenever the \prd\ construction is,
and the converse is true if we can assume that 
(\ref{UC}) and (\ref{MC}) hold.
% It would perhaps be a rather strange compound monad in which 
% they did not hold.
We give another useful lemma.

\begin{lemma} \label{lem-pko}
Assume $NM$ is constructed as in \S \ref{sec-pext}. 
If (\ref{MC}) holds, then 
\begin{align*}
\pext\ (g \oo f) & = \pext\ g \oo \mapN\ f \label{pexto} \tag{PO} \\[-0.5ex]
\kmap\ (g \oo f) & = \kmap\ g \oo \mapN\ f \label{kmapo} \tag{KO} 
\end{align*} 
and if (\ref{UC}) holds, then 
\begin{align*}
\pext\ f \oo \unitN & = f \label{pextru'} \tag{\ref{pextru}$'$} \\[-0.5ex]
\extNM\ f \oo \mapM\ \unitN & = \extM\ f \tag{\ref{extru}D} 
\end{align*} 
\end{lemma}
\begin{proof}
Using (\ref{PE}), the following gives (\ref{pexto}).
\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} 
\\[2ex]
& \mbox{(\ref{kmapo}): }&
\kmap\ (g \oo f) & = \pext\ (\unitNM \oM g \oo f)
    \tag{\ref{mapext}K, \ref{omoass}M} \\[-0.5ex]
  &&& = \pext\ (\unitNM \oM g) \oo \mapN\ f \tag{\ref{pexto}} \\[-0.5ex]
  &&& = \kmap\ g \oo \mapN\ f \tag*{(\ref{mapext}K)}
\\[2ex]
& \mbox{(\ref{pextru'}): }&
\pext\ f \oo \unitM & = \pext\ f \oM (\unitM \oo \unitN)
    \tag{\ref{omouass}M} \\[-0.5ex]
  &&& = \pext\ f \oM \unitNM = f \tag{\ref{UC}, \ref{pextru}} 
\end{align*}
\vspace{-5ex}%
\begin{align*}
& \mbox{(\ref{extru}D): } &
\extNM\ f & \oo \mapM\ \unitN = \extM\ (\pext\ f) \oo \mapM\ \unitN
    \tag{\ref{EC}} \\[-0.5ex]
  &&& = \extM\ (\pext\ f \oo  \unitN) = \extM\ f
    \tag*{(\ref{exto}M, \ref{pextru'}) $\square$} 
\end{align*}
\end{proof}

Then the relationships between \prd\ and \pext\ are given by these equalities,
which are equivalent when (\ref{pexto}) and (\ref{MJ1}N) hold.
See Appendix \S\ref{app-pp} for details.
\begin{align*}
\prd & = \pext\ \id &
\pext\ f & = \prd \oo \mapN\ f  
\end{align*}

\subsection{A generalisation of earlier axiom systems}
\label{sec-gen}
We now present a generalisation of the system of axioms
(\ref{MJ1}) to (\ref{MJ8}), and their equivalence to
(\ref{extru}) to (\ref{mapext}).
This was motivated by the construction by Jones \& Duponcheel
\cite[\S 3.3]{jones-composing}
using their function \dorp\ (see \S \ref{sec-jddorp}).

We found that the rules (\ref{G1}) to (\ref{G8}),
which are analogous to rules (\ref{MJ1}) to (\ref{MJ8}),
% shown in Table~\ref{tab-drules}
are sufficient to establish that $NM$ is a monad,
without assuming that either $N$ or $M$ is even a premonad.
In these rules, we make no assumptions about the functions
we call \extNM, \joinNM, \mapNM, \unitNM\ or \unitM. 

These rules also use three more functions of the following types:
\begin{align*}
\dunit & \ :\ \alpha M \to \alpha N M \\[-0.5ex]
\dmap & \ :\ (\alpha \to \beta M) \to (\alpha N M \to \beta N M) \\[-0.5ex]
\djoin & \ :\ \alpha N N M \to \alpha N M 
\end{align*}%
%
\setcounter{equation}{0}%
\renewcommand\theequation{G\arabic{equation}}%
\begin{align} % \label{tab-drules} was (\ref{G1}) to (\ref{G8})
\dmap\ \unitM &= \id \label{G1} \\[-0.5ex]
\dmap\ (f \oo h) &= \dmap\ f \oo \mapNM\ h \label{G2} \\[-0.5ex]
\dmap\ f \oo \unitNM &= \dunit \oo f \label{G3} \\[-0.5ex]
\djoin \oo \dmap\ (\dmap\ f) &= \dmap\ f \oo \joinNM 
  \label{G4} \\[-0.5ex]
\djoin \oo \dunit &= \id \label{G5} \\[-0.5ex]
\djoin \oo \dmap\ \unitNM &= \id \label{G6} \\[-0.5ex]
\djoin \oo \dmap\ \djoin &= 
  \djoin \oo \joinNM \label{G7} \\[1ex]
\extNM\ f &= \djoin \oo \dmap\ f \label{G8}
\end{align}

\begin{theorem} \label{thm-G}
Assume rules (\ref{G1}) to (\ref{G8}).
Then \extNM, \joinNM, \mapNM\ and \unitNM\ give a monad $NM$,
where also
\begin{eqnarray}
\djoin & = & \extNM\ \unitM \label{G9} \\[-0.5ex]
\dmap\ f & = & \extNM\ (\dunit \oo f) \label{G10} \\[-0.5ex]
\unitNM & = & \dunit \oo \unitM \label{G11} \\[-0.5ex]
\mapNM\ f & = & \dmap\ (\unitM \oo f) \label{G12} 
\end{eqnarray}
\end{theorem}

\begin{proof}
We prove rules (\ref{extru}), (\ref{extlu}), (\ref{extass}),
(\ref{joinext}) and (\ref{mapext}) for $NM$;
this proof corresponds almost step-by-step to the proof 
of these rules from (\ref{MJ1}) to (\ref{MJ8}). %Briefly: 
\begin{description}
\mditem[(\ref{extru}NM):] use (\ref{G8}), (\ref{G3}) and (\ref{G5}). 

\mditem[(\ref{extlu}NM):] use (\ref{G8}) and (\ref{G6}). 

\mditem[(\ref{joinext}NM):] use (\ref{G8}), (\ref{G4}) and (\ref{G1}). 

\mditem[(\ref{exto}NM):] use (\ref{G8}) and (\ref{G2}). 

\mditem[(\ref{extjm}NM):] use (\ref{joinext}NM) and (\ref{exto}NM).

% \mditem[(\ref{MJ6}NM):] use (\ref{extjm}NM) and (\ref{extlu}NM).

\mditem[(\ref{mapext}NM):] use (\ref{exto}NM) and (\ref{extlu}NM).

\mditem[(\ref{G9}):] use (\ref{G8}) and (\ref{G1}). 

\mditem[(\ref{G11}):] use (\ref{G3}) and (\ref{G1}). 

\mditem[(\ref{G12}):] use (\ref{G2}) and (\ref{G1}). 
\end{description}
%
\comment{
The proof of the converse definition
(\ref{G10}) is more tricky --- it starts by using
(\ref{G3}), (\ref{exto}NM), (\ref{G8}), (\ref{G4}) and (\ref{MJ6}NM).
}%
%
\begin{align} 
\mbox{(\ref{G10}): } 
\extNM\ (\dunit \oo f) & = \extNM\ (\dmap\ f \oo \unitNM) 
  \tag{\ref{G3}} \\[-0.5ex]
 & = \extNM\ (\dmap\ f) \oo \mapNM\ \unitNM\ \tag{\ref{exto}NM} \\[-0.5ex]
 & = \dmap\ f \oo \joinNM \oo \mapNM\ \unitNM\ \ 
   \tag{\ref{G8}, \ref{G4}} \\[-0.5ex]
% & = \dmap\ f \oo \extNM\ \unitNM\ = \dmap\ f \tag{\ref{MJ8}NM, \ref{extlu}NM} 
 & = \dmap\ f \tag{\ref{MJ8}NM, \ref{extlu}NM} 
\end{align}%
%
\begin{align*} 
\mbox{(\ref{extass}NM): } \qquad 
\extNM & ~ (\extNM\ g \oo f) \notag \\[-0.5ex]
  & = \djoin \oo \dmap\ (\djoin \oo \dmap\ g \oo f)
    \tag{\ref{G8}} \\[-0.5ex]
  % & = \djoin \oo \dmap\ \djoin \oo \mapNM\ (\dmap\ g \oo f)
    % \tag{\ref{G2}} \\[-0.5ex]
  & = \djoin \oo \joinNM \oo \mapNM\ (\dmap\ g \oo f) \quad
    \tag{\ref{G2}, \ref{G7}} \\[-0.5ex]
  % & = \djoin \oo \extNM\ (\dmap\ g \oo f)
    % \tag{\ref{MJ8}NM} \\[-0.5ex]
  & = \djoin \oo \djoin \oo \dmap\ (\dmap\ g \oo f)
    \tag{\ref{MJ8}NM, \ref{G8}} \\[-0.5ex]
  % & = \djoin \oo \djoin \oo \dmap\ (\dmap\ g) \oo \mapNM\ f
    % \tag{\ref{G2}} \\[-0.5ex]
  & = \djoin \oo \dmap\ g \oo \joinNM \oo \mapNM\ f
    \tag{\ref{G2}, \ref{G4}} \\[-0.5ex]
  & = \extNM\ g \oo \extNM\ f 
    \tag*{(\ref{G8}, \ref{MJ8}NM) $\square$} 
\end{align*}
\end{proof}

The following converse result tells us when a monad $NM$ can be defined in this
way.  Note that we are still not assuming that $M$ or $N$ is a monad.

\begin{theorem} \label{thm-Grev}
Assume that $NM$ is a monad.
Also assume that rules (\ref{G5}) and (\ref{G9}) to (\ref{G11}) hold.
Then the remaining rules among (\ref{G1}) to (\ref{G8}) hold.
\end{theorem}

\begin{proof}
\begin{description}
\item[\textmd{(\ref{G1})}:] use (\ref{G10}), (\ref{G11}) and (\ref{extlu}NM). 

\item[\textmd{(\ref{G2})}:] use (\ref{G10}) and (\ref{exto}NM). 

\item[\textmd{(\ref{G3})}:] use (\ref{G10}) and (\ref{extru}NM). 

\item[\textmd{(\ref{G8})}:] use (\ref{G9}), (\ref{G10}),
  (\ref{extass}NM) and (\ref{G5}). 

\item[\textmd{(\ref{G6})}:] use (\ref{G8}) and (\ref{extlu}NM). 

\item[\textmd{(\ref{G4})/(\ref{G7})}:] use (\ref{G8}), 
  Theorem~\ref{thm-ext-join-iff} for $NM$, \ref{ej3} $\Rightarrow$ \ref{ej1}, 
  and (\ref{G10})/(\ref{G9}). 
\qed
\end{description}
\end{proof}

Given a monad $NM$, we consider when it can be constructed using
Theorem~\ref{thm-G}.
First we note that if $NM$ is constructed as in \S \ref{sec-pext},
and (\ref{UC}) holds,
then we can define functions \dunit, \dmap\ and \djoin\
by (\ref{DU}), (\ref{G10}) and (\ref{G9}). 
Then (\ref{G11}) holds by (\ref{MJ3}M),
and (\ref{G5}) becomes (\ref{G5'}) which holds by (\ref{extru}D)
(see Lemma~\ref{lem-pko}) and (\ref{extlu}M).
Thus Theorem~\ref{thm-Grev} holds.
\begin{gather*}
\dunit = \mapM\ \unitN \tag{\ref{DU}}  \\
\extNM\ \unitM \oo \mapM\ \unitN = \id \label{G5'} \tag{\ref{G5}$'$}
\end{gather*}

\subsection{Relation to the \textit{dorp} construction of Jones \& Duponcheel}
\label{sec-jddorp}

Jones \& Duponcheel \cite{jones-composing} 
also show how to define a compound monad using a function \dorp,
satisfying four rules D(1) to D(4) (see Appendix~\ref{app-dd}),
and, assuming (\ref{UC}) and (\ref{MC})
and that $M$ is a premonad and $N$ is a monad,
show that the compound monads which can be
defined using \dorp\ are precisely those satisfying (\ref{J2}).
% Since, in many of the results of \cite{jones-composing}
% the relationship of \joinNM\ to \dorp\ is similar to that of 
% \prd\ to \swap, we tried, without success,
% to apply some of the previous results to \dorp.
We show corresponding results about when a compound monad
can be constructed using (\ref{G1}) to (\ref{G8}).
%
\begin{align}
\joinNM \oo \mapNM\ (\mapM\ \joinN) & = \mapM\ \joinN \oo \joinNM 
  \label{J2} \tag{J2} \\[-0.5ex]
\extNM\ (\mapM\ \joinN) & = \mapM\ \joinN \oo \joinNM 
  \label{J2'} \tag{J2$'$}
\end{align}

We first relate (\ref{J2}) to the conditions of Theorem~\ref{thm-Grev}.

\begin{lemma} \label{lem-J2}
Assume that $NM$ is a monad,
that $M$ is a premonad and $N$ is a monad, and that (\ref{UC}) holds.
Then (\ref{J2}) (equivalently, (\ref{J2'})) holds if and only if
$\extNM\ \unitM = \mapM\ \joinN$.
\end{lemma} 

\begin{proof}
$\Leftarrow$: by Theorem~\ref{thm-ext-join-iff} for $NM$,
  \ref{ej3} $\Rightarrow$ \ref{ej1}.

$\Rightarrow$: by applying Theorem~\ref{thm-ext-join-iff},
  \ref{ej1} $\Rightarrow$ \ref{ej2}, to (\ref{J2'}), gives
\begin{align*}
\mapM\ \joinN & = \extNM\ (\mapM\ \joinN \oo \unitNM) \\[-0.5ex]
  & = \extNM\ (\mapM\ \joinN \oo \unitM \oo \unitN) 
    \tag{\ref{UC}} \\[-0.5ex]
  & = \extNM\ (\unitM \oo \joinN \oo \unitN) 
    \tag{\ref{MJ3}M} \\[-0.5ex]
  & = \extNM\ \unitM \tag*{(\ref{MJ6}N) $\square$}
\end{align*}
\end{proof}

With the assumptions of Lemma~\ref{lem-J2}, 
and assuming that (\ref{J2}) holds,
we can define functions \dunit, \dmap\ and \djoin\
by (\ref{DU}), (\ref{G10}) and (\ref{DJ}), then 
(\ref{G9}), (\ref{G11}) and (\ref{G5}) hold,
so Theorem~\ref{thm-Grev} applies.
%
\begin{align*}
\djoin & = \mapM\ \joinN \tag{DJ} \label{DJ} \\[-0.5ex]
\dunit & = \mapM\ \unitN \tag{DU} \label{DU} 
\end{align*}

Note that we have shown that \emph{either} (\ref{J1}) \emph{or} (\ref{J2})
can be used to show that Theorem~\ref{thm-Grev} holds,
and so $NM$ can be constructed using Theorem~\ref{thm-G}.
This is related to the interesting fact that the equality
(\ref{G5'})
can be proved using \emph{either} (\ref{J1}) \emph{or} (\ref{J2}),
as it follows easily from (\ref{extru}D) or from Lemma~\ref{lem-J2}.

Finally, if we can define a compound monad $NM$ satisfying
(\ref{G1}) to (\ref{G8}) by using (\ref{DJ}) to define \djoin,
then (\ref{G9}) holds by Theorem~\ref{thm-G}, and so (\ref{J2}) holds.

\comment{
\begin{theorem}
Assume that $NM$ is a monad,
that $M$ is a premonad and $N$ is a monad,
and that (\ref{UC}) holds.
Then $NM$ can be constructed using functions \djoin, \dmap\ and \dunit,
and rules (\ref{G1}) to (\ref{G8}), if and only if (\ref{J2}) holds.  
\end{theorem}
}
We can define the function \dorp\
of Jones \& Duponcheel \cite{jones-composing} 
in terms of \dmap\ and vice versa, as follows,
and get the results relating to D(1) to D(4).
See Appendix \S\ref{app-dd} for details.
%
\begin{align*}
\dorp & =\ \dmap\ \id &
\dmap\ f & =\ \dorp \oo \mapNM\ f
\end{align*}

\subsection{When both constructions apply}
\label{sec-both}

We collect some results involving both \S \ref{sec-pext} and \S \ref{sec-gen}.
Note particularly that not all the results require all the assumptions of the
theorem.

\begin{theorem} \label{thm-both}
Assume that $NM$, $M$ and $N$ are monads,
and that (\ref{UC}), (\ref{MC}), (\ref{J1}) and (\ref{J2}) hold.
Define \djoin\ by (\ref{G9}) or (\ref{DJ}),
\dmap\ by (\ref{G10}), \dunit\ by (\ref{DU}),
\pext\ by (\ref{extom}K) or (\ref{PE}), \kjoin\ by (\ref{joinext}K)
and \kmap\ by (\ref{mapext}K). 
Then
\begin{align*}
\dunit & = \extM\ \unitNM \label{DUK} \tag{DUK} \\[-0.5ex]
\djoin & = \extM\ \kjoin \label{DJK} \tag{DJK} \\[-0.5ex]
\dmap\ f & = \extM\ (\kmap\ f) \label{DMK} \tag{DMK} \\[-0.5ex]
\kjoin & = \unitM \oo \joinN \label{KJ} \tag{KJ}
\end{align*}
\end{theorem}

\begin{proof} Note that, by Lemma~\ref{lem-J2}, any two of 
(\ref{J2}), (\ref{G9}) and (\ref{DJ}) imply the third,
and that, by (\ref{omext}NM), (\ref{extom}K) holds iff (\ref{PE}) holds.
By Lemma~\ref{lem-J1}, (\ref{J1S}) holds, and so 
Theorem~\ref{thm-when-pext} applies and (\ref{EC}) holds.

~ 

\noindent \quad
{(\ref{DUK}): \quad Use (\ref{DU}), (\ref{UC}) and (\ref{mapext}M).}

\noindent \quad
{(\ref{DJK}): \quad Use (\ref{G9}), (\ref{EC}) and (\ref{joinext}K).}
%
\begin{align*}
& \mbox{(\ref{DMK}): } &
\extM\ (\kmap\ f) & = \extM\ (\pext\ (\unitNM \oM f))
    \tag{\ref{mapext}K} \\[-0.5ex]
  &&& = \extM\ (\pext\ (\dunit \oo f))
    \tag{\ref{omext}M, \ref{DUK}} \\[-0.5ex]
  &&& = \extNM\ (\dunit \oo f) = \dmap\ f && &&
    \tag{\ref{EC}, \ref{G10}} 
\end{align*}
\vspace{-4ex}
\begin{align*}
& \mbox{(\ref{KJ}): } &&&
\kjoin & = \extM\ \kjoin \oo \unitM\ = \djoin \oo \unitM &&
    \tag{\ref{extru}M, \ref{DJK}} \\[-0.5ex]
  &&&&& = \mapM\ \joinN \oo \unitM = \unitM \oo \joinN &&
    \tag*{(\ref{DJ}, \ref{MJ3}M) $\square$} 
\end{align*}
\end{proof}
%

\comment{
\begin{align*}
\extNM\ \unitM \oo \mapM\ \unitN & = \extM\ (\pext\ \unitM \oo \unitN)
    \tag{\ref{EC}, \ref{exto}M} \\[-0.5ex]
  & = \extM\ \unitM = \id
    \tag{\ref{pextru'}, \ref{extlu}M} \\[1ex]
\end{align*}
\begin{align*}
\extNM\ \unitM & \oo \mapM\ \unitN = \mapM\ \joinN \oo \mapM\ \unitN
    \tag{Lemma~\ref{lem-J2}} \\[-0.5ex]
  & = \mapM\ (\joinN \oo \unitN) = \mapM\ \id = \id
    \tag{\ref{MJ2}M, \ref{MJ5}N, \ref{MJ1}M} 
\end{align*}
}

\subsection{Relation to the \textit{swap} construction of Jones \& Duponcheel}
\label{sec-jdswap}

Jones \& Duponcheel \cite{jones-composing} 
also show how to define a compound monad using a function \swap,
satisfying four rules S(1) to S(4), (see Appendix~\ref{app-ks}),
and, assuming (\ref{UC}) and (\ref{MC}) and that $M$ and $N$ are monads,
show that a compound monad can be
defined using \swap\ iff it satisfies (\ref{J1}) and (\ref{J2}).
% (or its equivalent, (\ref{J2'})).

Given a compound monad $NM$ satisfying (\ref{J1}) and (\ref{J2}),
Lemma~\ref{lem-J1} gives (\ref{J1S}),
and hence, by Theorem~\ref{thm-when-pext}, $NM$ can be defined using 
\kjoin\ and \kmap.
Then, defining $\swap = \kmap\ \id$ we can prove 
S(1) to S(4) of \cite{jones-composing}.
% (which give properties of \swap),
% without assuming either (\ref{J2}) or that $N$ is a monad.

% As noted above, we have, in Theorems \ref{thm-pext-k} and \ref{thm-when-pext},
% shown that the compound monads which can be defined using
% \kjoin\ and \kmap\ are those satisfying (\ref{J1S}).
% Note that for this we have not assumed that $N$ is even a premonad.
% So far, our only assumptions about $N$ are (\ref{UC}) and (\ref{MC}).

Conversely, given monads $M$ and $N$ and a function \swap,
we can define \kmap\ in terms of \swap\ as below, 
but to define the monad $NM$
we also need to define \kjoin, which we can do using (\ref{KJ}).

The relationships between \swap\ and \kmap\ are given by these equalities,
which are equivalent when (\ref{kmapo}) and (\ref{MJ1}N) hold.
See Appendix \S\ref{app-ks} for more details.
\begin{align*}
\swap & = \kmap\ \id & \kmap\ f & = \swap \oo \mapN\ f 
\end{align*}

\subsection{Relation to the distributive law for monads} 
\label{sec-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. 
Further details are in Appendix \S\ref{app-dl}.

\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 \KM, the Kleisli category of $M$, and we have shown how this is simply
a monad in \KM.
Under further conditions, this construction is 
is equivalent to the \prd\ construction of 
Jones \& Duponcheel \cite{jones-composing}.
We have shown how the ``map'' function of the monad in \KM\ is similarly 
related to the \swap\ construction of \cite{jones-composing}.
We developed a set of axioms generalising those of a monad to 
describe a way of constructing a compound monad which is similarly
related to the \dorp\ construction of \cite{jones-composing}.
% This also has facilitated proofs concerning some compound monads.

\subsubsection{Acknowledgements}
I thank unnamed referees for drawing my attention to the work
of Manes on a distributive law for monads,
and for alterting me to the semantic issues which need to be addressed
before regarding Conjectures \ref{thm-param} and \ref{thm-par-cor} as theorems.