\section{Introduction}

Monads are convenient for structuring functional programs.
For example, an algorithm requiring use of a mutable state may be coded in a
purely functional style using the \emph{state} monad, or
an algorithm involving some non-deterministic steps may be 
conveniently coded using the \emph{list} monad.
Wadler \cite{wadler-essence} shows in particular how it is easy to change a
program to introduce these features if it is written in a monadic style.
However, to code (equally conveniently) a program involving both these aspects 
requires a monad which somehow combines both the state and the list monads.

A monad consists of a type constructor and several functions 
(of appropriate types), which must satisfy certain rules.
There are several equivalent formulations of these rules.
Once we have defined the type constructor for a compound monad, 
it is necessary to prove the rules for the compound monad,
as they do not follow automatically from the rules for the 
individual monads.
It is important to establish that the rules hold,
since to use a type constructor wrongly thought to be a monad can lead to 
incorrect programs -- two ways of coding a function, which are thought to be
equivalent, may be different.
Yet the constructions can be complex, leading to errors in proofs,
for example see \cite[\S 6.4.2]{jones-composing}.

A monad is a category theoretic notion, and we focus on
sets of rules relating to the Kleisli category of a monad, 
and show how these facilitate proofs of the monad rules
for some compound monads.

In the rest of this section we introduce monads and the
category theory that we use in the rest of the paper.
In section~\ref{sec-single} we give several sets of rules,
and prove some useful results about monads.
In section~\ref{sec-comp} we give two examples of compound monads, 
showing how it is particularly easy to establish one of 
the sets of monad rules for them.
In section~\ref{sec-pext} we introduce a new function \pext\ which is useful
in defining a compound monad, 
and we set out the rules which \pext\ must satisfy.
These rules are easily understood in terms of \pext\ being a functor. 
We consider the class of compound monads which can be defined using
\pext\ and these rules, and show that it contains the compound monads
which can be defined using 
Jones \& Duponcheel's \prd\ construction \cite{jones-composing}.
Section~\ref{sec-concl} concludes.

\subsection{Monads} \label{s-monads}

A \emph{monad} is a type constructor $M$ (which we write postfix)
together with functions of the types
given in Table~\ref{tab-mftypes}, which must satisfy certain rules.
Where several monads are involved, we may use subscripts to avoid ambiguity,
both in the names of these functions and the names of monad rules.

\begin{table}%[!hbt]
\caption{Types of monad functions} \label{tab-mftypes}
\begin{eqnarray*}
\unit & : & \alpha \to \alpha M \\
\map & : & (\alpha \to \beta) \to (\alpha M \to \beta M) \\
\join & : & \alpha M M \to \alpha M \\
\ext & : & (\alpha \to \beta M) \to (\alpha M \to \beta M) \\
\bind & : & \alpha M \to (\alpha \to \beta M) \to \beta M 
  \qquad \qquad \mbox{(infix)} \\
\odot & : & (\beta \to \gamma M) \to (\alpha \to \beta M) \to 
  (\alpha M \to \gamma M) \qquad \mbox{(infix)} \\
\end{eqnarray*}
\end{table}

This set of functions is not minimal, they are related by the rules
in Table~\ref{tab-mfrels}.
Note that \id\ and \oo\ denote the identity function and function composition
respectively, and that \bind\ and \om\ are written in infix notation.
(Infix operators have a lower precedence than function application).

\begin{table}%[!hbt]
\caption{Relationships between monad functions}
\label{tab-mfrels}
\begin{center} \textit{
\begin{tabular}{rcl@{\qquad\qquad}r}
m bind f & = & ext f m & (\bindext) \\
ext f & = & join \oo\ map f & (\extjm) \\
join & = & ext id & (\joinext) \\
map f & = & ext (unit \oo\ f) & (\mapext) \\
g \om\ f & = & ext g \oo\ f & (\omext) \\
ext g & = & g \om\ id & (\extom)
\end{tabular}
} \end{center} 
\end{table}

For $M$ and the functions to qualify as a monad, a set of rules must be
satisfied.  Several sets of rules have been given.
Firstly, when the functions \unit, \map\ and \join\ are given, 
the seven rules in Table~\ref{tab-mjrules} must be satisfied.

\begin{table}%[!hbt]
\caption{Monad rules for \unit, \map\ and \join}
\label{tab-mjrules}
\begin{center} \textit{
\begin{tabular}{rcl@{\qquad\qquad}r}
map id & = &  id & \textup{(MJ1)} \\
map f \oo\ map g & = &  map (f \oo\ g) & \textup{(MJ2)} \\
unit \oo\ f & = &  map f \oo\ unit & \textup{(MJ3)} \\
join \oo\ map (map f) & = &  map f \oo\ join  & \textup{(MJ4)} \\
join \oo\ unit & = &  id & \textup{(MJ5)} \\
join \oo\ map unit & = &  id & \textup{(MJ6)} \\
join \oo\ map join & = &  join \oo\ join  & \textup{(MJ7)} 
\end{tabular}
} \end{center} 
\end{table}

Alternatively, a monad can be defined in terms of 
\unit\ and \ext.
Wadler \cite{wadler-essence} gives analogues (in terms of \bind) of 
the three rules in Table~\ref{tab-eorules}.

\begin{table}%[!hbt]
\caption{Monad rules for \unit\ and \ext} 
\label{tab-eorules}
\begin{center} \textit{
\begin{tabular}{rcl@{\qquad\qquad}r}
ext f \oo\ unit & = & f & (\extru) \\
ext unit & = & id & (\extru) \\
ext (ext g \oo\ f) & = & ext g \oo\ ext f & (\extass) 
% ext (g \om\ f) & = & ext g \oo\ ext f & (\extfun) 
\end{tabular}
} \end{center} 
\end{table}

If a monad is defined by giving \unit, \map\ and \join,
satisfying the seven rules of Table~\ref{tab-mjrules}, and if 
\ext\ is defined by (\extjm), then the three rules of Table~\ref{tab-eorules}
and (\mapext) and (\joinext) hold.
Conversely, 
if a monad is defined by giving \unit\ and \ext,
satisfying the seven rules of Table~\ref{tab-eorules}, and if 
\map\ and \join\ are defined by (\mapext) and (\joinext),
then the seven rules of Table~\ref{tab-mjrules} and (\extjm) hold.
(Wadler states the analogous result for the formulation of the three rules in
terms of \bind.)


\subsection{Some Category Theory} \label{s-cat}

A \emph{category} consists of a collection of \emph{objects}
and a collection of \emph{arrows}.
Each arrow $f$ has a \emph{source} object $s(f)$ and a 
\emph{target} object $t(f)$.  Two arrows $f$ and $g$, such that
$t(f) = s(g)$, can be composed to give another arrow
which we write $g \circ f$,
with source $s(f)$ and target $t(g)$.
Composition of arrows is associative.
For each object $\alpha$ there is an \emph{identity} arrow $\id_\alpha$,
such that $\id_\alpha \circ f = f = f \circ \id_\alpha$.
See \cite{maclane-categories} for more details.

Clearly then, if we let the objects be types (eg, $\alpha$, $\beta$),
and the arrows functions (eg $f : \alpha \to \beta$), we have a category,
where $s(f) = \alpha$ and $t(f) = \beta$.

A \emph{functor} from one category to another (or to the same category)
is a mapping $\theta$ which takes objects to objects and arrows to arrows, 
and preserves 
\begin{itemize}
\item the sources and targets of arrows, ie $s(\theta f) = \theta (s(f))$ and
   $t(\theta f) = \theta (t(f))$ 
\item composition of arrows, ie $\theta (g \circ f) = \theta g \circ \theta f$ 
\item identity arrows, ie $\theta (\id_\alpha) = \id_{\theta(\alpha)}$
\end{itemize}
If $M$ and \map\ satisfy the type information in 
Table~\ref{tab-mftypes} and the rules (MJ1) and (MJ2), then 
$M$ and \map\ give a functor $\theta$
from the category of types and functions to itself,
where $\theta (\alpha) = \alpha M$ and $\theta (f) = \map\ f$.

However there is another interesting category associated with a monad,
namely the \emph{Kleisli} category
(see \cite[ChVI,\S 5]{maclane-categories}).
We describe it in functional programming terms.
Its objects are the types (eg, $\alpha$, $\beta$), but an arrow
with source $\alpha$ and target $\beta$ is a function \emph{of type}
$\alpha \to \beta M$.
The identity for object $\alpha$ is the function $\unit : \alpha \to \alpha M$,
and composition is the function \om\ (which is of the required type, and 
may be called ``monadic composition'').
There is a functor from the ``ordinary'' category of
types and functions to the Kleisli category.
We call it \kl\ (``Kleisli lift'') and define it
% (and note that it has the right type):
\begin{center} \textit{
\begin{tabular}{rcl@{\qquad\qquad}r}
kl & : & $(\alpha \to \beta) \to (\alpha \to \beta M)$ \\
kl f & = & unit \oo\ f
\end{tabular}
} \end{center} 
The function \ext\ is a functor from the Kleisli category to the 
``ordinary'' category, and we may note that the rule (\mapext)
tells us that the composition of the functors
\ext\ and \kl\ is the functor \map.