\section{Axioms for a Single Monad} \label{sec-single} \subsection{A Weaker Set of Monad Rules} First, in Table~\ref{tab-eowrules}, we give a set of monad rules which is similar to those in Table~\ref{tab-eorules}, but note that we have replaced (\extass) by (\extfun). Note also that the two rules (\extlu) and (\extfun) express the fact that \ext\ is a functor. This set of rules is weaker than those in Table~\ref{tab-eorules} in that if we add to them the additional requirement \textit{g \om\ f = ext g \oo\ f} then we get the rules of Table~\ref{tab-eorules}. \begin{table}%[!hbt] \caption{Monad rules for \unit, \ext\ and \om} \label{tab-eowrules} \begin{center} \textit{ \begin{tabular}{rcl@{\qquad\qquad}r} ext f \oo\ unit & = & f & (\extru) \\ ext unit & = & id & (\extlu) \\ ext (g \om\ f) & = & ext g \oo\ ext f & (\extfun) \end{tabular} } \end{center} \end{table} In fact we can prove \textit{g \om\ f = ext g \oo\ f}, identity and associativity in the Kleisli category, and some other useful results, from the rules of Table~\ref{tab-eowrules}. \begin{theorem} Assuming the rules of Table~\ref{tab-eowrules}, and defining \map\ and \join\ using (\mapext) and (\joinext) (Table~\ref{tab-mfrels}), \begin{quote} \begin{tabular}{l@{\qquad}r@{\ \ }c@{\ \ }l} \textbf{(\omext)} & g \om\ f & = & ext g \oo\ f \\ \textbf{(\extcong)} & ext f = ext g & $\Rightarrow$ & f = g \\ \textbf{(\omoass)} & (h \om\ g) \oo\ f & = & h \om\ (g \oo\ f) \\ \textbf{(\klid)} & unit \om\ f & = & f \\ \textbf{(\krid)} & f \om\ unit & = & f \\ \textbf{(\kass)} & h \om\ (g \om\ f) & = & (h \om\ g) \om\ f \\ \textbf{(\exto)} & ext (g \oo\ f) & = & ext g \oo\ map f \end{tabular} \end{quote} \end{theorem} \begin{proof} \begin{description} \item[(\omext)] By (\extfun), \textit{ext (g \om\ f) \oo\ unit = ext g \oo\ ext f \oo\ unit}. Using (\extru), this simplifies to \textit{g \om\ f = ext g \oo\ f}. % \begin{center} \textit{ % \begin{tabular}{rcl@{\qquad\qquad}r} % ext (h \om\ f) \oo\ unit & = & ext h \oo\ ext f \oo\ unit & \extfun \\ % h \om\ f & = & ext h \oo\ f & \extru,\extru % \end{tabular} % } \end{center} \item[(\extcong)] If \textit{ext f = ext g} then \textit{ext f \oo\ unit = ext g \oo\ unit}. Using (\extru), this simplifies to $f = g$. % \begin{center} \textit{ % ext f = ext g $\Rightarrow$ ext f \oo\ unit = ext g \oo\ unit % $\Rightarrow$ f = g % } \end{center} \item[(\omoass)] Using (\omext), both sides are equal to \textit{ext h \oo\ g \oo\ f}. \item[(\klid,\krid,\kass)] One proof of these would proceed by rewriting these, using (\omext) and (\extfun), to eliminate all uses of \om. Then they follow from (\extlu), (\extru) and the associativity of \oo\ (since both sides of (\kass) become \textit{ext h \oo\ ext g \oo\ f}). But another proof which better reflects our focus on categories and functors is to observe that in each case, by (\extcong), it suffices to prove \ext(lhs) = \ext(rhs). In each case, this may be proved using the fact that \ext\ is a functor, ie, using (\extfun) and (\extlu). That is, we use the identity and associativity rules for \id\ and \oo\ to prove the corresponding rules for \unit\ and \om. \textit{ \begin{description} \item[] \textnormal{for (\klid):} ext (unit \om\ f) = ext unit \oo\ ext f = id \oo\ ext f = ext f \item[] \textnormal{for (\krid):} ext (f \om\ unit) = ext f \oo\ ext unit = ext f \oo\ id = ext f \item[] \textnormal{for (\kass):} ext (h \om\ (g \om\ f)) = ext h \oo\ (ext g \oo\ ext f) = \\ \mbox{} \hfill (ext h \oo\ ext g) \oo\ ext f = ext ((h \om\ g) \om\ f) \end{description} } \item[(\exto)] ~ \textit{ \begin{tabular}{rcl@{\qquad\qquad}r} ext (g \oo\ f) & = & ext ((g \om\ unit) \oo\ f) & (\krid) \\ & = & ext (g \om\ (unit \oo\ f) & (\omoass) \\ & = & ext g \oo\ ext (unit \oo\ f) & (\extfun) \\ & = & ext g \oo\ map f & (\mapext) \end{tabular} } \end{description} \qed \end{proof} At this point, note that (\extom) (Table~\ref{tab-mfrels}) follows trivially from (\omext), as does (\extjm) from (\exto) and (\joinext). The following theorem is useful later. \begin{theorem} \label{thm-ext-join-iff} 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{theorem} \begin{proof} \begin{description} \comment{ now superfluous \item[\ref{ej3} $\Rightarrow$ \ref{ej1}] Assume \ref{ej3}. Then \textit{ \begin{tabular}{@{\qquad}rcl@{\qquad\qquad}r} ext (f \om\ id) & = & ext f \oo\ ext id & (\extfun) \\ ext (ext f) & = & ext f \oo\ join & (\extom, \joinext) \\ ext g & = & g \oo\ join & \end{tabular} } end of comment } \item[\ref{ej1} $\Rightarrow$ \ref{ej2}] Assume \ref{ej1}. Then \textit{ \begin{tabular}{rcl@{\qquad\qquad}r} ext g \oo\ map unit & = & g \oo\ join \oo\ map unit & \\ ext (g \oo\ unit) & = & g \oo\ ext unit = g & (\exto, \extjm, \extlu) \end{tabular} } \item[\ref{ej2} $\Rightarrow$ \ref{ej3}] is obvious. \item[\ref{ej4} $\Rightarrow$ \ref{ej1}] Set \textit{h = id} and use (\joinext). \item[\ref{ej4} $\Rightarrow$ \ref{ej2}] Set \textit{h = unit} and use (\extlu). \item[\ref{ej3} $\Rightarrow$ \ref{ej4}] When \textit{g = ext f}, \ref{ej4} is just (\extfun). \end{description} \qed \end{proof} Finally, we include a proof that \kl\ is a functor \cite[ChVI,\S 5]{maclane-categories}. \begin{theorem} \kl\ is a functor. \end{theorem} \begin{proof} Clearly \kl\ preserves identity: \textit{kl id = unit \oo\ id = unit}. For composition: \begin{center} \textit{ \begin{tabular}{rcl@{\qquad\qquad}r} kl g \om\ kl f & = & (unit \oo\ g) \om\ (unit \oo\ f) & \\ & = & ((unit \oo\ g) \om\ unit) \oo\ f & (\omoass) \\ & = & (unit \oo\ g) \oo\ f = kl (g \oo\ f) & (\krid) \end{tabular} } \end{center} \qed \end{proof} With (\omext), and Table~\ref{tab-eowrules}, we now have the monad rules of Table~\ref{tab-eorules}, and can therefore assume all the results of Tables \ref{tab-mfrels} and \ref{tab-mjrules} (Wadler\cite[\S 2.10]{wadler-essence}). However it is now easy to outline proofs of the rules in Table~\ref{tab-mjrules}. Using (\extjm), (MJ6) is just (\extlu). Using (\extjm), then (\mapext) and (\joinext) respectively, (MJ4) and (MJ7) are special cases of Theorem~\ref{thm-ext-join-iff}, \ref{ej3} $\Rightarrow$ \ref{ej1}. Using (\mapext) and (\joinext) respectively, (MJ3) and (MJ5) are cases of (\extru). Finally, as noted earlier, (\mapext) shows that \textit{map = ext \oo\ kl}. As \ext\ and \kl\ are functors, so is \map, which gives us (MJ1) and (MJ2). \subsection{Monad Rules Based on the Kleisli Category} We have proved the three rules, (\klid), (\krid) and (\kass), which reflect that the Kleisli category is indeed a category. We may ask whether these are sufficient to establish a monad. If we could assume also (\omext), then it would be easy to show the three rules of Table~\ref{tab-eowrules}. However, if we are (hoping to) define a monad in terms of these rules, and in terms of the functions \unit\ and \om, then we can take (\extom) as a definition, but that does not give us (\omext). If we add a fourth rule, (\omoIass) (see Table~\ref{tab-assrules}), governing \om, then that is sufficient. For, clearly, (\omoIass) and (\extom) imply (\omext). Note that (\omoIass) is the special case $g = \id$ of (\omoass), and is therefore true in any monad. Therefore we have the following theorem. \begin{theorem} The rules given in Table~\ref{tab-assrules}, with the definitions (\extom), (\mapext) and (\joinext), give a monad. \end{theorem} \begin{table}%[!hbt] \caption{Monad rules for \unit\ and \om} \label{tab-assrules} \begin{center} \textit{ \begin{tabular}{rcl@{\qquad\qquad}r} unit \om\ f & = & f & (\klid) \\ f \om\ unit & = & f & (\krid) \\ h \om\ (g \om\ f) & = & (h \om\ g) \om\ f & (\kass) \\ (h \om\ id) \oo\ f & = & h \om\ f & (\omoIass) \end{tabular} } \end{center} \end{table} \subsection{A Free Theorem} We may ask whether the fourth rule in Table~\ref{tab-assrules} is really necessary. Indeed, in some examples (later) it is the only one of the four whose proof is not quite trivial. It turns out that in any real example it is a ``free theorem'' (Wadler \cite{wadler-free}). First, we state a more general theorem. \begin{theorem} \label{thm-param} If $\theta : (\alpha \to \beta) \to (\alpha \to \gamma)$ is a function which is polymorphic in $\alpha$, then \begin{enumerate} \renewcommand\theenumi{(\roman{enumi})} \renewcommand\labelenumi\theenumi \item \label{par1} there exists $h : \beta \to \gamma$ such that (for all $f : \alpha \to \beta$) $\theta f = h \circ f$ \item \label{par2} for all $f : \alpha \to \alpha'$ and $g : \alpha' \to \beta$, $\theta\ (g \circ f) = \theta\ g \circ f$ \end{enumerate} \end{theorem} The result \ref{par1} may be explained intuitively as follows. Since $\theta$ is polymorphic in $\alpha$, the coding of the function $\theta$ cannot use any information about the type $\alpha$. That is, although an argument $a : \alpha$ to the function $\theta f$ may be an integer, binary tree of strings, or whatever, $\theta$ (on its own) can only treat $a$ as a ``black box''. So the only thing that $\theta f$ can do with $a$ (other than ignore it) is to apply $f$ to it. Wadler \cite{wadler-free} shows how to use Reynold's abstraction theorem for the polymorphic lambda calculus to formally obtain results of this nature, and our proof follows his approach. In particular, we write the proof as though types were sets. \begin{proof} Clearly the two parts are equivalent ($h$ being $\theta\ \id$). We prove \ref{par2}. Wadler's general result is $\theta \sim \theta$, where $\sim$ denotes the relation appropriate to the type of the terms related, which, for $\theta$, is $\forall \alpha. (\alpha \to \beta) \to (\alpha \to \gamma)$. This means that for all $\alpha, \alpha'$ and relation $\sim\ \subseteq \alpha \times \alpha'$, for all $k : \alpha \to \beta$, $k' : \alpha' \to \beta$, $a : \alpha$ and $a' : \alpha'$, whenever $k \sim k'$ and $a \sim a'$, then $\theta\ k\ a \sim \theta\ k'\ a'$. Now $k \sim k'$ means whenever $x \sim x'$, for $x : \alpha$ and $x' : \alpha'$, then $k\ x \sim k'\ x'$. We choose the relation $\sim\ \subseteq \alpha \times \alpha'$ to be $a \sim a' \iff a' = f \ a$; the relations on (fixed) types $\beta$ and $\gamma$ are the identity. So we can simplify the above. We get $k \sim k'$ iff, for all $x : \alpha$, $k\ x = k'\ (f\ x)$, that is, $k = k' \circ f$. Then, letting $k' = g$ and $k = g \circ f$, we have $k \sim k'$. So for all $a : \alpha$, we can let $a' = f \ a$, so $a \sim a'$ and $\theta\ k\ a \sim \theta\ k'\ a'$, that is, $\theta\ (g \circ f)\ a = \theta\ g\ (f\ a)$. Therefore, $\theta\ (g \circ f) = \theta\ g \circ f$. \qed \end{proof} \begin{corollary} Assuming that $\mbox{\om} : (\beta \to \gamma M) \to (\alpha \to \beta M) \to (\alpha \to \gamma M)$ is polymorphic in $\alpha$, the rule (\omoass) holds. \end{corollary} \begin{proof} Given $h : \beta \to \gamma M$, define $\theta\ g \equiv h \odot g$. Then Theorem~\ref{thm-param}\ref{par2} gives \\ \textit{h \om\ (g \oo\ f) = (h \om\ g) \oo\ f}, as required. \qed \end{proof} \subsection{Example: the Continuation Monad} The continuation monad (eg, \cite[\S 3.1]{wadler-essence}) is given by $\alpha K = (\alpha \to \Ans) \to \Ans$, where \Ans\ is a fixed type, so $\alpha \to \beta K = \alpha \to (\beta \to \Ans) \to \Ans$. We use the function \C, %(``switch arguments'') defined by \textit{C f x y = f y x}. Note that \textit{C (C f) = f}, so \C\ is 1-1, and $\C\ x = \C\ y \Rightarrow x = y$. Then we define \oK\ by \textit{C (g \oK\ f) = C f \oo\ C g}, and \unitK\ by \textit{C \unitK\ = id}. The \om\ rules are then easily proved. For each rule \lhs\ = \rhs, as \C\ is 1-1, it suffices to prove \C(\lhs) = \C(\rhs). \textit{ \begin{description} \item[] \textnormal{for (\klid):} C (unit\K\ \oK\ f) = C f \oo\ C unit\K\ = C f \oo\ id = C f \item[] \textnormal{for (\krid):} C (f \oK\ unit\K) = C unit\K\ \oo\ C f = id \oo\ C f = C f \item[] \textnormal{for (\kass):} C (h \oK\ (g \oK\ f)) = (C f \oo\ C g) \oo\ C h = \\ \mbox{} \hfill C f \oo\ (C g \oo\ C h) = C ((h \oK\ g) \oK\ f) \end{description} } It is simple but tedious to confirm (\omoIass\K) directly. We now check that this definition corresponds to the usual ones. Using (\extom\K), we get \begin{itemize} \item[] \textit{\unitK\ a c = C id a c = id c a = c a}\ , and \item[] \textit{\extK\ g k c = (g \oK\ id) k c = C (C id \oo\ C g) k c = \\ \mbox{} \qquad \qquad (C id \oo\ C g) c k = C id (C g c) k = id k (C g c) = k ($\lambda$f. g f c)} \end{itemize} Both of these agree with the definitions in \cite[\S 3.1]{wadler-essence}.