\section{Introduction} \label{sec-intro}

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.
Moggi \cite{moggi} shows how to describe computational activity in terms of
monads.
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.
and in Appendix~\ref{app-ex} we give examples of the easy use of some
of these rules to certain compound monads. 
In section~\ref{sec-cmc} we describe two constructions which are useful 
in defining a compound monad, 
and we set out the rules which must be satisfied in each case.
We show how one of these constructions amounts to defining a monad in
the Kliesli category of another monad.
In Appendix~\ref{app-jd} we show how the constructions of 
Jones \& Duponcheel \cite{jones-composing} are cases of ours.
Section~\ref{sec-concl} concludes.

The results of this paper have been proved using the theorem prover
Isabelle/HOL.
The proofs are at 
\url{http://users.rsise.anu.edu.au/~jeremy/isabelle/monad/}.
While most of the proofs are not difficult, much of the work involved
showing the equivalence of different sets of axioms.
In this regard the ``book-keeping'' aspect of using a theorem prover,
to keep track of which results are being assumed, and which proved,
at a particular point, was of great value.

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

A \emph{monad} is a type constructor $M$ (which we write postfix)
together with functions of the types given below, % in Table~\ref{tab-mftypes},
which must satisfy certain rules.
If we loosely say ``$M$ is a monad'', this refers also to associated
functions which will be either clear from the context, 
or have the names used below.
Where several monads are involved, we may use subscripts to avoid ambiguity
in the names of these functions.
For the names of monad rules we write (for example) (\ref{extlu}N)
to mean rule (\ref{extlu}) for the monad $N$, that is,
$\extN\ \unitN\ = \id$.  
%
% \begin{table}%[!hbt]
% \caption{Types of monad functions} \label{tab-mftypes}
\begin{align*}
\unit & : \alpha \to \alpha M \\[-0.5ex]
\map & : (\alpha \to \beta) \to (\alpha M \to \beta M) \\[-0.5ex]
\join & : \alpha M M \to \alpha M \\[-0.5ex]
\ext & : (\alpha \to \beta M) \to (\alpha M \to \beta M) \\[-0.5ex]
\bind & : \alpha M \to (\alpha \to \beta M) \to \beta M 
  \tag{infix} \\[-0.5ex]
\odot & : (\beta \to \gamma M) \to (\alpha \to \beta M) \to 
  (\alpha \to \gamma M) \tag{infix} 
\end{align*}
% \end{table}

This set of functions is not minimal, they are related by the rules
% in Table~\ref{tab-mfrels}.
shown below.
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).
%
\comment{
\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}
}
%
\begin{eqnarray*}
m\ \bind\ f & = & \ext\ f\ m\ \\[-0.5ex] % & (\bindext) \\
\ext\ f & = & \join \oo \map\ f\ \\[-0.5ex] % & (\extjm) \\
\join & = & \ext\ \id \\[-0.5ex] % & (\joinext) \\
\map\ f & = & \ext\ (\unit \oo f) \\[-0.5ex] % & (\mapext) \\
g \om f & = & \ext\ g \oo f\ \\[-0.5ex] % & (\omext) \\
\ext\ g & = & g \om \id  % & (\extom)
\end{eqnarray*}

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, 
% and \ext\ and \odot\ defined using rules (\ref{extjm}) and (\ref{omext}) 
% the seven rules in Table~\ref{tab-mjrules} must be satisfied.
rules (\ref{MJ1}) to (\ref{MJ7}) must be satisfied.
This is the ``monoid form'' presentation of an algebraic theory of 
Manes \cite[Chapter~1, Definition~3.17]{manes}.
A \emph{premonad} satisfies rules (\ref{MJ1}) to (\ref{MJ3}).
%
\comment{
\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}
}
%
\setcounter{equation}{0}
\renewcommand\theequation{\arabic{equation}}
\begin{eqnarray}
% seven rules in Table~\ref{tab-mjrules} now rules (\ref{MJ1}) to (\ref{MJ7}) 
\map\ \id & = &  \id\ \label{MJ1} \\[-0.5ex]
\map\ f \oo \map\ g & = &  \map\ (f \oo g) \label{MJ2} \\[-0.5ex]
\unit \oo f & = &  \map\ f \oo \unit\ \label{MJ3} \\[-0.5ex]
\join \oo \map\ (\map\ f) & = &  \map\ f \oo \join\  \label{MJ4} \\[-0.5ex]
\join \oo \unit & = &  \id\ \label{MJ5} \\[-0.5ex]
\join \oo \map\ \unit & = &  \id\ \label{MJ6} \\[-0.5ex]
\join \oo \map\ \join & = &  \join \oo \join\  \label{MJ7} \\[1ex]
\ext\ f & = & \join \oo \map\ f \label{extjm} \label{MJ8} \\[1ex]
\ext\ (g \oo f) & = & \ext\ g \oo \map\ f \label{exto}
\end{eqnarray}

Then (\ref{MJ8}) defines \ext\ in terms of \join\ and \map.
At this point it is convenient to note rule (\ref{exto}), 
which clearly follows from (\ref{MJ8}) and (\ref{MJ2}).

Alternatively, a monad can be defined in terms of 
\unit\ and \ext.
Wadler \cite{wadler-essence} shows the equivalence to
analogues (in terms of \bind) of 
% the three rules in Table~\ref{tab-eorules},
rules (\ref{extru}), (\ref{extlu}) and (\ref{extass}),
which are given by Moggi \cite{moggi}.
This is also the ``extension form'' presentation of an algebraic theory of 
Manes \cite[Chapter~1, \S 3, Exercise~12]{manes}.
%
\setcounter{equation}{0}
\renewcommand\theequation{E\arabic{equation}}
\begin{align}
% \label{tab-eorules} was rules (\ref{extru}), (\ref{extlu}) and (\ref{extass}),
\ext\ f \oo \unit & = f \label{extru} \\[-0.5ex]
\ext\ \unit & = \id\ \label{extlu} \\[-0.5ex]
\stepcounter{equation}
\ext\ (\ext\ g \oo f) & = \ext\ g \oo \ext\ f 
 \tag{\ref{extfun}$'$} \label{extass} \\[1ex]
\join & = \ext\ \id \label{joinext} \\[-0.5ex] 
\map\ f & = \ext\ (\unit \oo f) \label{mapext} 
\end{align}

\comment{
\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 & (\extlu) \\
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 rules (\ref{MJ1}) to (\ref{MJ7}), and if 
\ext\ is defined by (\ref{extjm}), then 
rules (\ref{extru}), (\ref{extlu}), (\ref{extass}),
(\ref{joinext}) and (\ref{mapext}) hold.
Conversely, if a monad is defined by giving \unit\ and \ext,
satisfying rules (\ref{extru}), (\ref{extlu}) and (\ref{extass}),
and if \join\ and \map\ are defined by (\ref{joinext}) and (\ref{mapext}),
then the rules (\ref{MJ1}) to (\ref{extjm}) hold.
(Wadler states the analogous result for the formulation 
of rules (\ref{extru}), (\ref{extlu}) and (\ref{extass}) in terms of \bind.) 


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

Monads have been known (sometimes under different names) as part of
category theory before their use in describing computations,
eg \cite{maclane-categories,manes}.
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, such as $f : \alpha \to \beta$,
we have a category \T, 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 
\S \ref{s-monads} % Table~\ref{tab-mftypes}
and the rules (\ref{MJ1}) and (\ref{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$.
(By an abuse of terminology we will often refer to the action of a function on
arrows, such as \map, or \ext\ or \kl\ below, as a ``functor'').

However there is another interesting category associated with a monad,
namely the \emph{Kleisli} category \KM\
(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 {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 \T\ of
types and functions to the Kleisli category \KM.
We call it \kl\ (``Kleisli lift'') and define its action (on arrows) by
% (and note that it has the right type):
\begin{align*} 
& \kl\  :\  (\alpha \to \beta) \to (\alpha \to \beta M) \\
& \kl\ f \ = \ \unit \oo f
\end{align*} 
The function \ext\ is a functor from \KM\ to \T\
(on objects, the functor takes a type $\alpha$ to the type $\alpha\ M$),
and we may note that the rule (\ref{mapext})
tells us that the composition of the functors
\ext\ and \kl\ is the functor \map.
See \cite[ChVI, \S 5, Theorem~1]{maclane-categories} for these results.