\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.
We note that when the conditions are satisfied for both constructions to be 
applicable, then we have the distributive law for monads described by 
Manes \cite{manes} and Barr \& Wells \cite{bwttt}: see \S \ref{sec-dl}.
In this case the monads are ``compatible'' \cite[\S 9.2]{bwttt},
and our results show how some of the conditions given in \cite{bwttt}
for this are redundant.

\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{E1D} \extNM\ f \oo \mapM\ \unitN & = \extM\ f \tag{\ref{extru}D} 
% \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}).
% 
% \mditem[(\ref{E1D}):] 
% By (\ref{PE}) and (\ref{extru}NM), $\pext\ f \oo \unitN = f$.
% Thus, by (\ref{EC}) and (\ref{exto}M),
% $\extNM\ f \oo \mapM\ \unitN = \extM\ (\pext\ f \oo \unitN) = \extM\ f$.
\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 two necessary conditions, 
% namely that (\ref{J1S}) and (\ref{E1D}) hold.
% In fact, these conditions, which are equivalent, are also sufficient.
% since (\extcomp) tells us
the previous theorem provides a necessary condition, 
namely that (\ref{J1S}) holds.
In fact, this condition is also sufficient.
% $\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 
(\ref{J1S}) (see Theorem~\ref{thm-pext-k}) holds.
% \textbf{(\UC)} & \unitNM\ & = & \unitM\ \oo\ \unitN \\
% \textbf{(\J1S)} & \ext\M\ (\ext\NM\ f) & = & \ext\NM\ f \oo\ \join\M
% either (\ref{J1S}) or (\ref{E1D}) (see Theorem~\ref{thm-pext-k}) hold.
Then 
% both (\ref{J1S}) and (\ref{E1D}) hold, and
\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})
(equivalently, (\ref{J1'})),
which is the case $f = \id$ of (\ref{J1S}).
In fact (\ref{MC}) and (\ref{J1}) are sufficient to imply (\ref{J1S}).
We also give a condition (\ref{E1D}),
which is also implied by (\ref{MC}) and its case $f = \id$,
and which, assuming (\ref{UC}), is equivalent to (\ref{J1S}).
The proof of (\ref{J1S}) from (\ref{E1D}) is thanks to an observation by 
Michael Barr (see \S \ref{sec-dl}).
%
\begin{gather}
\unitNM\ f = \unitM\ (\unitN\ f) \label{UC} \tag{UC} \\[-0.5ex]
\mapNM\ f = \mapM\ (\mapN\ f) \label{MC} \tag{MC} \\
\joinM \oo \mapM\ \joinNM = \joinNM \oo \joinM \label{J1} \tag{J1} \\[-0.5ex]
\extM\ \joinNM = \joinNM \oo \joinM \label{J1'} \tag{J1$'$} \\
\label{E1D} \extNM\ f \oo \mapM\ \unitN = \extM\ f \tag{\ref{extru}D} \\
\label{E1DI} \joinNM\ \oo \mapM\ \unitN = \joinM\ \tag{\ref{extru}DI} 
\end{gather} 

\begin{lemma} \label{lem-J1}
If $M$ and $NM$ are monads, then
\begin{enumerate}
\renewcommand\theenumi{(\roman{enumi})}
\renewcommand\labelenumi\theenumi
\item (\ref{MC}) and (\ref{J1}) imply (\ref{J1S})
\item (\ref{MC}) and (\ref{E1DI}) imply (\ref{E1D})
\item assuming (\ref{UC}), (\ref{J1S}) and (\ref{E1D}) are equivalent.
\end{enumerate}
\end{lemma}

\begin{proof}
\begin{enumerate}
\renewcommand\theenumi{(\roman{enumi})}
\renewcommand\labelenumi\theenumi
\item \label{lem-J1-S}
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}
\end{align*}
\item \label{lem-J1-DI} Assuming (\ref{E1DI}),
\begin{align*} \!\! %avoids a bad break
\extNM\ f \oo \mapM\ \unitN & = \joinNM \oo \mapNM\ f \oo \mapM\ \unitN 
 \tag{\ref{extjm}NM} \\[-0.5ex]
   & = \joinNM \oo \mapM\ (\mapN\ f \oo \unitN) 
     \tag{\ref{MC}, \ref{MJ2}M} \\[-0.5ex]
   & = \joinNM \oo \mapM\ \unitN \oo \mapM\ f 
     \tag{\ref{MJ3}N, \ref{MJ2}M} \\[-0.5ex]
   & = \joinM \oo \mapM\ f = \extM\ f 
     \tag{\ref{E1DI}, \ref{joinext}M} 
\end{align*}

\item \label{lem-J1-E1D}
% First we show that (\ref{J1S}) and (\ref{E1D}) are equivalent.
Let (\ref{J1S}) hold; we show (\ref{E1D}).
Using Theorem~\ref{thm-ext-join-iff} for $NM$, 
\ref{ej1} $\Rightarrow$ \ref{ej2}, 
\begin{align*} \!\! \!\! \!\! \!\! \!\! \!\! %avoids a bad break
\extNM\ f \oo \mapM\ \unitN & = 
\extM\ (\extNM\ f \oo \unitM) \oo \mapM\ \unitN \\[-0.5ex]
  &= \extM\ (\extNM\ f \oo \unitM \oo \unitN) \tag{\ref{exto}M} \\[-0.5ex]
  &= \extM\ (\extNM\ f \oo \unitNM) = \extM\ f \tag{\ref{UC}, \ref{extru}NM}
\end{align*}

Now, suppose that (\ref{E1D}) holds; we show (\ref{J1S}). 
\begin{align*}
\extM (\extNM\ f) &= 
\extNM\ (\extNM\ f) \oo \mapM\ \unitN \tag{\ref{E1D}} \\[-0.5ex]
  &= \extNM\ f \oo \extNM\ \id\ \oo \mapM\ \unitN \tag{\ref{extass}NM}
  \\[-0.5ex]
  &= \extNM\ f \oo \extM\ \id\ = \extNM\ f \oo \joinM 
    \tag{\ref{E1D}, \ref{joinext}M}
    % \tag*{(\ref{E1D}, \ref{joinext}M) $\square$}
\end{align*}
\end{enumerate}
\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 \unitN & = \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{Lifting monad $N$ to \KM}
By a \emph{lifting} of one monad to another (maybe in different categories)
we understand a functor $F$ which is also a functor between their Kleisli
categories.
We consider whether the monad \NKM\ in the Kleisli category \KM\ is
a lifting of the monad $N$.
This would require
\begin{align*}
F\ \id & = \unitM \tag{LI} \label{LI} \\[-0.5ex]
F\ (g \oo f) & = F\ g \oM F\ f \tag{LO} \label{LO} \\
F\ \unitN & = \unitNM \tag{LU} \label{LU} \\[-0.5ex]
F\ (g \oN f) & = F\ g \oNM F\ f \tag{LA} \label{LA}  
\end{align*}
Instead of \eqref{LA}, we may use \eqref{LE}, or \eqref{LM} and \eqref{LJ}.
\begin{align*}
F\ (\extN\ f) & = \pext\ f \tag{LE} \label{LE} \\ 
F\ (\mapN\ f) & = \kmap\ f \tag{LM} \label{LM} \\[-0.5ex]
F\ \joinN & = \kjoin \tag{LJ} \label{LJ}  
\end{align*}
%
Assuming \eqref{UC}, $F = \kl$, where $\kl\ f = \unitM \oo f$ 
satisfies \eqref{LI}, \eqref{LO} and \eqref{LU}.

With $F = \kl$, note that
\eqref{LJ} is just \eqref{KJ} of Theorem~\ref{thm-both},
and, indeed, \kl\ is a lifting if and only if
\eqref{J2} (see \S \ref{sec-jddorp}) holds.

\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})
(equivalently, (\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}.
The same holds of (\ref{DJK}) (see \S \ref{sec-both}).

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 consider the situation when both the constructions of 
\S \ref{sec-pext} and \S \ref{sec-gen} apply,
that is when both (\ref{J1}) and (\ref{J2}) hold.
In this case, we have a distributive law for monads: see \S \ref{sec-dl}.
We collect some results involving both constructions.
Note particularly that not all the results require all the assumptions of the
theorem. 
Indeed, it can be seen that if \djoin\ is defined by (\ref{G9}),
then (\ref{DJK}) has two proofs, as given,
one relying on (\ref{J1}) and one on (\ref{J2}).

\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{lem-J1-S}, (\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$} \\
& \mbox{(\ref{KJ}): } &
\kjoin & = \pext\ \unitM = \extNM\ \unitM \oo \unitM &&
    \tag{\ref{joinext}K, \ref{PE}} \\[-0.5ex]
  &&& = \mapM\ \joinN \oo \unitM = \unitM \oo \joinN &&
    \tag*{(Lemma~\ref{lem-J2}, \ref{MJ3}M)} 
\end{align*}
\noindent \quad
{(\ref{DJK}): \quad Use (\ref{DJ}), (\ref{mapext}M) and (\ref{KJ})}
\qed \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}\ref{lem-J1-S} 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.
This is also described by Barr \& Wells in \cite{bwttt}, \S 9.2.
Under the conditions of Theorem~\ref{thm-both}, 
the compound monad is based on a distributive law.
The distributive law, (ie, the natural transformation $\lambda$
of \cite{manes} and \cite{bwttt}) is the polymorphic function \swap. 
Further details are in Appendix \S\ref{app-dl}.  

When $NM$, $M$ and $N$ are monads, assuming that (\ref{MC}) holds,
Barr \& Wells give conditions (C1) to (C5) for $NM$ to be ``compatible'' with 
$N$ and $M$.
These are in effect the conditions of Theorem~\ref{thm-both},
though some of their conditions are redundant.
Of their five conditions, 
condition (C1) is (in effect) (\ref{UC}). 
Condition (C5) is (\ref{J2}),
and Lemma~\ref{lem-J2} shows that it is equivalent to (C2).

Condition (C3) is \eqref{E1DI}, that is, the case $f = \id$ of (\ref{E1D}),
and condition (C4) is (\ref{J1}), that is, the case $f = \id$ of (\ref{J1S}).
These also are equivalent:
by Lemma~\ref{lem-J1}, \ref{lem-J1-DI} and \ref{lem-J1-S} these are 
equivalent to (\ref{E1D}) and (\ref{J1S}) respectively,
which are equivalent by Lemma~\ref{lem-J1}\ref{lem-J1-E1D}.

Barr \& Wells give these conditions in category theory notation,
which reveals a duality between (C2),(C5) 
on the one hand, and (C3),(C4) on the other.
We note how (C4) and (C5), that is, (\ref{J1}) and (\ref{J2}),
are dual in this sense.
Jones \& Duponcheel draw attention to a relation between (\ref{J1}) and
(\ref{J2}), which is that they are each, in effect, of the form of 
\ref{ej1} of Theorem~\ref{thm-ext-join-iff}.
This relation seems quite distinct from their duality.

As Michael Barr has observed, the same duality should hold between the proofs 
(C2) $\Leftrightarrow$ (C5) and (C3) $\Leftrightarrow$ (C4),
when these are written out in
the category theory notation (the proof (C3) $\Rightarrow$ (C4) is thanks to
this observation).
See Appendix~\S\ref{app-dl} for these proofs.

\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 and of Barr \& Wells on a distributive law for monads,
and for alterting me to the semantic issues involved in
Propositions \ref{thm-param} and \ref{thm-par-cor}.