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

Since the language of HOL is close to that of functional programming languages
we will present monads in a way that is closer to Wadler's treatment than that
of category theory.
%
Thus a monad involves functions of types 
(read $\leadsto$ as $\to$): 
\begin{align*}
\unit & : \alpha \leadsto \alpha M \\[-0.5ex]
\map & : (\alpha \leadsto \beta) \to (\alpha M \leadsto \beta M) \\[-0.5ex]
\join & : \alpha M M \leadsto \alpha M \\[-0.5ex]
\ext & : (\alpha \leadsto \beta M) \to (\alpha M \leadsto \beta M) \\[-0.5ex]
% \bind & : \alpha M \to (\alpha \to \beta M) \to \beta M \tag{infix} \\[-0.5ex]
\odot & : (\beta \leadsto \gamma M) \to (\alpha \leadsto \beta M) \to
  (\alpha \leadsto \gamma M) \tag{infix}
\end{align*}

To relate this to category theory,
the type constructor $M$ is the action of a functor on objects,
and \map\ is the action of a functor on arrows.
The polymorphic functions \unit\ and \join\ 
are the natural transformations $\eta$ and $\mu$;
the other functions will be mentioned later.  

We note here that in the case of the types of \map, \ext\ and \om,
when we generalise from the category of functions to a category of general
arrow type, the `$\leadsto$' symbols represent this general arrow type,
whereas the `$\to$' symbols continue to represent functions.
This is why we prefer to use \ext\ rather than \bind,
as in Wadler \cite{wadler-essence}, and in \cite{homeier},
in stating the monad rules:
% as functions,
$m\ \bind\ f = \ext\ f\ m$.

If a monad is defined in terms of \unit, \map\ and \join,
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}.
(\texttt{g\_umj\_monad\_exp})
\setcounter{equation}{0}
\renewcommand\theequation{\arabic{equation}}
\begin{align}
% 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\ & \mu \oo \eta M & = id M \label{MJ5} \\[-0.5ex]
\join \oo \map\ \unit & = \id\ & \mu \oo M \eta & = id M \label{MJ6} \\[-0.5ex]
\join \oo \map\ \join & = \join \oo \join & 
  \mu \oo M\mu & = \mu \oo \mu M \label{MJ7} \\[1ex]
\ext\ f & =\join \oo \map\ f \label{extjm} % \\[1ex]
% \ext\ (g \oo f) & = \ext\ g \oo \map\ f \label{exto}
\end{align}

Here rules (\ref{MJ1}) and (\ref{MJ2}) express that \map\ is the action on
arrows of a functor, (\ref{MJ3}) and (\ref{MJ4}) express that 
$\eta$ and $\mu$ are natural transformations, and (\ref{MJ5}) to (\ref{MJ7})
are the three identities given in 
Manes \cite[Chapter~1, Definition~3.17]{manes}.
We also give these latter in common category theory notation. 
Note the use of $\mu M$ and $\eta M$, composition of a natural transformation
with a functor: while this is not reflected in the form of the axioms as found
in \cite{wadler-essence}, it can be seen in the type annotations of the
respective terms in \HOLw, as shown.  Note that most of the type annotations
have been edited out!

\begin{verbatim}
comp (join [:'a:]) (unit [:'a 'M:]) = id [:'a 'M:] 
comp (join [:'a:]) (map (unit [:'a:])) = id [:'a 'M:]
comp (join [:'a:]) (map (join [:'a:])) =
                    comp (join [:'a:]) (join [:'a 'M:])
\end{verbatim}

Then (\ref{extjm}) defines \ext\ in terms of \join\ and \map.
% This rule in particular is one which we will frequently use without specific
% comment.
% At this point it is convenient to note the useful rule (\ref{exto}),
% which clearly follows from (\ref{extjm}) 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{extfun}),
which are given by Moggi \cite{moggi}.
This is the ``extension form'' presentation of an algebraic theory of
Manes \cite[Chapter~1, \S 3, Exercise~12]{manes}.
(\texttt{Komonad\_thm})
%
% We prefer the use of \ext\ to \bind\ since, in the type of \ext\ shown above,
% the first and last occurrences of $\rightarrow$ can be seen as examples of
% arrows in a more general category; in fact, as detailed later,
% \ext\ is the action on arrows of a functor.
%
\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]
\ext\ (g \om f) & = \ext\ g \oo \ext\ f \label{extfun} \\[1ex]
% \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} \\
g \om f & = \ext\ g \oo f \label{omext} \\[-0.5ex]
\ext\ g & = g \om id \label{extom} \tag{\ref{omext}$'$} 
\end{align}

If a monad is defined by giving \unit, \map\ and \join,
satisfying the rules (\ref{MJ1}) to (\ref{MJ7}), and if
\ext\ and \om\ are defined by (\ref{extjm}) and (\ref{omext}), then
rules (\ref{extru}) % , (\ref{extlu}), (\ref{extfun}), (\ref{joinext}) and 
to (\ref{mapext}) hold.
Conversely, if a monad is defined by giving \unit, \ext\ and \om,
satisfying rules (\ref{extru}), (\ref{extlu}) and (\ref{extfun})
then (\ref{omext}) holds,
and if \join\ and \map\ are defined by (\ref{joinext}) and (\ref{mapext}),
then the rules (\ref{MJ1}) to (\ref{extjm}) hold.
% We can express this sort of result as a single equivalence:
We can express this as a equivalence:

\begin{theorem}[\texttt{g\_umj\_iff\_Kdomonad}] \label{t-e3-umj7}
% \begin{theorem}
(\ref{MJ1}) to (\ref{extjm}) and (\ref{omext}) 
$\Leftrightarrow$ (\ref{extru}) to (\ref{mapext})
\end{theorem}

The \HOLw\ proof of Theorem~\ref{t-e3-umj7} was an application of a
theorem involving compound monads, see Appendix~\ref{a-dmap} for details.

% (Wadler states the analogous result for the formulation
% of rules (\ref{extru}), (\ref{extlu}) and (\ref{extass}) in terms of \bind.)

% Instead of assuming
% (\ref{extru}), (\ref{extlu}) and (\ref{extass}),
% and using (\ref{omext}) as a definition,
% we can assume (\ref{extru}), (\ref{extlu}) and (\ref{extfun}),
% and \emph{prove} (\ref{omext}) from (\ref{extru}) and (\ref{extfun}).

\comment{ OMIT STUFF ABOUT A RULES 
REPLACED BY PARA FOLLOWING, AND RELOCATE extom RULE
Expressing the above in terms of $\odot$ rather than $\ext$, we get
%
\setcounter{equation}{0}
\renewcommand\theequation{A\arabic{equation}}
\begin{align}
% \label{tab-assrules} was rules (\ref{krid}) to (\ref{omoIass})
f \om \unit & = f \label{krid} \\[-0.5ex]
\unit \om f & = f \label{klid} \\[-0.5ex]
h \om (g \om f) & = (h \om g) \om f \label{kass} \\[-0.5ex]
(h \om g) \oo f & = h \om (g \oo f) \label{omoass} \\
% (h \om id) \oo f & = h \om f \label{omoIass} \\[1ex]
% h \om (\unit \oo f) & = h \oo f \label{omouass} \tag{\ref{omoIass}$'$} \\[1ex]
\ext\ g & = g \om id \label{extom} % \\[1ex]
\end{align}

Rules (\ref{krid}) to (\ref{omoass})
% (\ref{kass}) and any of (\ref{omoIass}), (\ref{omouass}) or (\ref{omoass})
are necessary and sufficient to characterise a monad.
% and in fact (\ref{omoass}) can be replaced by a weaker version where
% $g = id$ (\ref{omoIass}), or one where $g = \unit$ (\ref{omouass}).
%
In fact it is easy to show (\ref{omoass}) directly from either
of its special cases $g = \id$ or $g = \unitM$,
% (\ref{omoIass}) or (\ref{omouass})
using the associativity of $\oo$ or $\om$ respectively.
Using the case $g = \unitM$ gives, in effect, the
``clone form'' presentation of an algebraic theory of
Manes \cite[Chapter~1, Definition~3.2]{manes}.
END OF OMITTED STUFF ABOUT A RULES }

Now from (\ref{extru}) we get $\ext\ f = \ext\ g \Rightarrow f = g$,
whence (\ref{extlu}) and (\ref{extfun}) give that \om\ is associative,
and has the identity \unit.
Thus % , by (\ref{krid}) to (\ref{kass}),
there is a category, whose objects are types,
whose arrows from $\alpha$ to $\beta$ are arrows (functions) of ``type'' 
$\alpha \leadsto \beta M$, and whose identity and composition 
are \unitM\ and $\odot$ (\texttt{Komonad\_IMP\_Kcat}).
This is the \emph{Kleisli} category, \KM, of the monad $M$.
We use $\alpha \leadsto_M \beta = \alpha \leadsto \beta M $
to represent the ``types'' of its arrows.
Then, by (\ref{extlu}) and (\ref{extfun}), \ext\ is the action on arrows
of a functor from the Kleisli category \KM\ into the original category
$\mathcal C$ (\texttt{Komonad\_IMP\_ext\_f});
its action on objects is just the type constructor $M$.
 
The use of a general arrow type in our \HOLw\ development 
enables us to express results about the Kleisli category.

We define the Kleisli arrow so that 
$(A, M, \alpha, \beta)\ \Kleisli = \alpha \leadsto_M \beta$.
Recall that this is syntactic sugar for a curried type operator,
$\beta (\alpha (M (A\ \Kleisli)))$.
We partially apply it,
so $M (A\ \Kleisli)$ is the arrow type operator in the Kleisli category \KM,
and the theorem \texttt{Komonad\_IMP\_Kcat} was entered as shown below,
and the type of the arrow composition in \KM\ is then 
\texttt{('A, 'M) Kleisli o\_arrow}.
 
% val _ = type_abbrev ("Kleisli", Type `: \'A 'M 'a 'b. ('a, 'b 'M) 'A`) ;

\begin{verbatim}
Komonad_IMP_Kcat : |- category [:'A:] (id, comp) ==>
    Komonad (id, comp) (unit, ext, kcomp) ==>
    category [: ('A, 'M) Kleisli :] (unit, kcomp)
\end{verbatim}

The relationship between adjoint functors and monads is well known:
every pair of adjoint functors $F$ and $G$ gives a monad, whose action on
objects is $G \oo F$, whose \unit\ ($\eta$) is just $\eta$ (!), 
% and whose \join\ is $G \epsilon F$
and where $\ext\ f$ is $G (f^\sharp)$
(\texttt{g\_adjf1\_IMP\_Kmonad}).
In doing the \HOLw\ proofs we noticed that
this result does not even require that $\eta$ be a natural
transformation.
% noticing this led us to the further work
% on minimal presentations of adjoint pairs described in \S\ref{s-adjf}.
Every monad is obtainable from a pair of adjoint functors,
via (inter alia) 
% normally in several ways.  One way is via
the Kleisli category, the adjoint functors being \ext\ and
% the functor which takes arrow $f : \alpha \leadsto \beta$ to 
% $\unit \oo f : \alpha \leadsto_M \beta$ (\texttt{Komonad\_IMP\_uof}).
the functor which is the identity on objects,
and takes arrow $f$ to $\unit \oo f$. % (\texttt{Komonad\_IMP\_uof}).
% that these are adjoint functors, from
% (\texttt{Kmonad\_IMP\_adjf}, \texttt{Kmonad\_IMP\_unit\_nt}).

% in Appendix
% \begin{verbatim}
% g_adjf1_IMP_Kmonad :
  % |- category (idC,compC) /\ g_functor (idD,compD) (idC,compC) G /\
           % g_adjf1 (idC,compC) G eta sharp ==>
        % Kmonad (idC,compC) (eta,(\:'a 'b. G o sharp))
% \end{verbatim}

We proved some of these results in \HOLw, 
as detailed in Appendix~\ref{a-monads}. 
We record a lemma which we find particularly useful later.

\begin{lemma} \label{thm-ext-join-iff}
% If \join\ is defined using (\ref{joinext}),
In a monad the following are equivalent
\begin{enumerate}
\renewcommand\theenumi{(\roman{enumi})}
\renewcommand\labelenumi\theenumi
\item \label{ej1} \textit{ext g = g \oo\ join}
\item \label{ej2} \textit{g = ext (g \oo\ unit)}
\item \label{ej3} there exists $f$ such that \textit{g = ext f}
\item \label{ej4} for all $h$, \textit{ext (g \oo\ h) = g \oo\ ext h}
\end{enumerate}
\end{lemma}



