
\documentclass{lecture}


\usepackage{amsmath}
\usepackage{latexsym}
\usepackage{amssymb}
%\usepackage{proof}
\usepackage{exptrees}

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{definition}{Definition}
\newtheorem{condition}{Condition}


\renewcommand\theenumi{(\alph{enumi})}
\renewcommand\labelenumi{\theenumi}
\renewcommand\theenumii{(\roman{enumii})}
\renewcommand\labelenumii{\theenumii}

\newcommand\comment[1]{} 
\newcommand\mditem[1][]{\item{\textmd{#1}}}
\newcommand{\mytilde}{\scriptstyle\sim}

\input{defs}
\title{ }

\begin{document}
\begin{slide}
  \begin{Heading}
Composition of Monads
  \end{Heading}

\begin{center}
\begin{tabular*}{\linewidth}{@{}l@{\extracolsep{\fill}}l@{}} 
\multicolumn{2}{c}{Jeremy E.\ Dawson}
\\ \\
Logic \& Computation Programme      & Automated Reasoning Group 	\\
National ICT Australia 		&  Computer Sciences Laboratory   \\
& Res.\ Sch.\ of Inf.\ Sci.\ and Eng.\  \\
& {Australian National University}                    \\
\texttt{Jeremy.Dawson@nicta.com.au} &
\texttt{http://rsise.anu.edu.au/{\small$\mytilde$}jeremy} 
\end{tabular*}
\end{center}

\end{slide}

\begin{slide}
  \begin{heading}
{Types of monad functions}
  \end{heading}

\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 \\[-0.5ex]
  % \tag{infix} 
\odot & : (\beta \to \gamma M) \to (\alpha \to \beta M) \to 
  (\alpha \to \gamma M) % \tag{infix} 
\end{align*}

  \begin{heading}
{Examples for the list monad}
  \end{heading}
let $g\ 1 = [1]$, $g\ 3 = [1,2,3]$, etc
\begin{align*}
\unit\ a & = [a] \\[-0.5ex]
\map\ f\ [x,y,z] & = [f\ x, f\ y, f\ z]
\\[-0.5ex]
\join\ [[u,v], [w], [x,y]] & = [u,v,w,x,y]
\\[-0.5ex]
\ext\ g\ [2,0,4] & = [1,2,1,2,3,4]
\end{align*}
\end{slide}

\begin{slide}
  \begin{heading}
{Relationships between monad functions}
  \end{heading}

\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*}

\end{slide}

\begin{slide}
  \begin{heading}
{Monad rules for \unit, \map\ and \join}
  \end{heading}
\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\ \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{MJ8} \\[1ex]
\ext\ (g \oo f) & = \ext\ g \oo \map\ f \label{exto}
\end{align}
\end{slide}

\begin{slide}
  \begin{heading}
{Examples of monad rules} 
  \end{heading}

\begin{align*}
\join \oo \unit & = \id\ \tag{\ref{MJ5}} \\
\join\ [[3,5,7]] & = [3,5,7] \\[1ex]
\join \oo \map\ \unit & = \id\ \tag{\ref{MJ6}} \\
\join\ [[3],[5],[7]] & = [3,5,7] 
\end{align*}%
\begin{align*}
\join \oo \map\ (\map\ f) & = \map\ f \oo \join\ \tag{\ref{MJ4}} 
\end{align*}
$$[[u,v], [w], [x,y]] \qquad
\begin{gathered} ~
[[u', v'], [w'], [x',y']] \\ [u,v, w, x,y] 
\end{gathered}
\qquad [u',v',w',x',y'] $$
\begin{align*}
\join \oo \map\ \join & = \join \oo \join\ \tag{\ref{MJ7}} 
\end{align*}%
$$[[[u,v], [w]], [[x], [y,z]] \qquad
\begin{gathered} ~
[[u,v,w], [x,y,z]] \\
[[u,v], [w], [x], [y,z]] 
\end{gathered}
\qquad [u,v,w,x,y,z] $$
\end{slide}

\begin{slide}
  \begin{heading}
{Monad rules for \unit, \ext\ and \om} 
  \end{heading}
\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}

\setcounter{equation}{0}
\renewcommand\theequation{E\arabic{equation}}
% Table~\ref{tab-eowrules} was rules (\ref{extru}) to (\ref{extfun})
\begin{eqnarray}
\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} \stepcounter{equation} % \stepcounter{equation}
g \om f & = & \ext\ g \oo f \label{omext}
\end{eqnarray}
\end{slide}

\begin{slide}
  \begin{heading}
A useful theorem
  \end{heading}
\begin{theorem} \label{thm-ext-join-iff}
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{theorem}
Refer monad rules (\ref{joinext}), (\ref{MJ7}), (\ref{mapext}) and  (\ref{MJ4})
\end{slide}

\begin{slide}
  \begin{heading}
Identity and associativity in the Kleisli category \KM
  \end{heading}
\begin{theorem} \label{thm-sres}
Assuming rules (\ref{extru}) to (\ref{extfun})
% and defining \join\ using (\ref{joinext}),
\begin{align}
\tag{\ref{omext}} g \om f & = \ext\ g \oo f \\
\tag{\ref{omoass}} (h \om g) \oo f & = h \om (g \oo f) \\
\tag{EI} \label{extcong} \ext\ f = \ext\ g & \Rightarrow f = g \\
\tag{\ref{krid}} f \om \unit & = f \\[-0.5ex]
\tag{\ref{klid}} \unit \om f & = f \\[-0.5ex]
\tag{\ref{kass}} h \om (g \om f) & = (h \om g) \om f 
\end{align}
\end{theorem}
the Kleisli category \KM: 
\textbf{objects} are types --- $\alpha$, $\beta$, etc \\[1ex]

\textbf{an arrow} from $\alpha$ to $\beta$ is a function of type 
$\alpha \to \beta M$ \\[1ex]
\textbf{identity arrow} on $\alpha$ is $\unit : \alpha \to \alpha M$ \\[1ex]
\textbf{composition} is 
$\odot : (\beta \to \gamma M) \to (\alpha \to \beta M) \to 
  (\alpha \to \gamma M) $, so \\
$g$ from $\beta$ to $\gamma$ and 
$f$ from $\alpha$ to $\beta$ compose to give
  $g \om f$, from $\alpha$ to $\gamma$ \\[1ex]

Rules (\ref{krid}) to (\ref{kass}) give the properties required for a category.

\end{slide}

\begin{slide}
  \begin{heading}
{Monad Rules Based on the Kleisli Category \KM} 
  \end{heading}
\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 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]
(h \om g) \oo f & = h \om (g \oo f) \label{omoass} 
\end{align}

\end{slide}

\begin{slide}
  \begin{heading}
{The State Monad} 
  \end{heading}
Let \State\ be a fixed type, eg, the program state.
Let $\alpha S = \State \to \alpha * \State$
\begin{gather*}\unit_S\ a\ s = (a, s) \\
% \ext_S\ f\ sa\ s = \text{let } (a, s') = sa\ s \text{ in } f\ a\ s' \\
(g \oS f)\ a\ s = \text{let } (b, s') = f\ a\ s \text{ in } g\ b\ s'
\end{gather*}
Proof tedious, but use $\unc$
(inverse is $\curry$, so both 1-1)
\begin{align*} 
\curry\ g\ x\ y & = g\ (x,y) &
\unc\ f\ (x,y) & = f\ x\ y
\end{align*} 
So for $f : \alpha \to \beta S$,
$\unc\ f : \alpha * \State \to \beta * \State$.
\begin{description}
\mditem[for (\ref{krid}) and (\ref{klid}):] \\
$\unc\ (f \oS \unitS) =
  \unc\ f \oo \unc\ \unitS = \unc\ f \oo \id = \unc\ f$
$\unc\ (\unitS \oS f) = 
  \unc\ \unitS \oo \unc\ f = \id \oo \unc\ f = \unc\ f$ \\
\mditem[for (\ref{kass}):]
$\unc\ (h \oS (g \oS f)) = \unc\ h \oo (\unc\ g \oo \unc\ f) = $ \\
\mbox{} \hfill
  $ (\unc\ h \oo \unc\ g) \oo \unc\ f = \unc\ ((h \oS g) \oS f)$  
\end{description}
\end{slide}

\begin{slide}
  \begin{heading}
{The Compound State Monad} 
  \end{heading}
Let $M$ be any monad. Define
$\alpha S_M = \State \to (\alpha * \State) M$.

We can define \oSM\ and \unitSM\ by
\begin{align*} 
\unc\ (g \oSM f) & = \unc\ g \oM \unc\ f \\
\unc\ \unitSM & = \unitM
\end{align*} 

Then the proofs are easy, using corresponding rules for monad $M$.

for (\ref{krid}) and (\ref{klid}): \\
{$\unc\ (f \oSM \unitSM) =
  \unc\ f \oM \unc\ \unitSM = \unc\ f \oM \unitM = \unc\ f$}  \\
$\unc\ (\unitSM \oSM f) = 
  \unc\ \unitSM \oM \unc\ f = \unitM \oM \unc\ f = \unc\ f$ 

for (\ref{kass}): \\
$\unc\ (h \oSM (g \oSM f)) = \unc\ h \oM (\unc\ g \oM \unc\ f) = $ \\
\mbox{} \hfill
  $ (\unc\ h \oM \unc\ g) \oM \unc\ f = \unc\ ((h \oSM g) \oSM f)$  

Other definitions more complicated, and proofs correspondingly so.
\end{slide}

\begin{slide}
  \begin{heading}
{A free theorem ??} 
  \end{heading}
Still need to prove (\ref{omoIass}),
$$(h \om id) \oo f = h \om f 
\qquad f : \alpha \to \beta M \qquad h : \beta \to \gamma M$$
Can we use Wadler's ``free theorems''?

Idea is that $h \om \_ : (\alpha \to \beta M) \to \alpha \to \gamma M$
is polymorphic in $\alpha$, so in applying $h \om f$ to $a : \alpha$,
can only apply $f$ to $a$, and then do something else, call it $g$.

That is, $h \om f = g \oo f$, so
$$(h \om \id) \oo f = (g \oo \id) \oo f = g \oo f = h \om f$$

Is this valid?
\end{slide}

\begin{slide}
  \begin{heading}
{Other Monads}
  \end{heading}

List monad: $\alpha L = \alpha\ \mbox{list}$ 

Reader monad: $\alpha R = \mbox{param} \to \alpha$

Writer monad: $\alpha W = \alpha \times \mbox{output}$

Error monad: $\alpha E = \alpha\ \mbox{option}$ \quad
  (SOME $a$ for success, NONE for failure)

These can form compound monads with an arbitrary monad $M$ in different ways:
$\alpha M R$, $\alpha W M$, $\alpha E M$

$\alpha E$ can represent termination of a program with a result, or
non-termination

$\alpha E L$ represents corresponding non-deterministic program operation 

$\alpha L E$ also represents such a program for considering
\emph{total correctness}: \\
if it \emph{may} fail to terminate then 
never mind what else it might do, it is a failure.

$\alpha L E$ is also a compound monad
\end{slide}

\begin{slide}
  \begin{heading}
{Compound Monads \textit{via} Partial Extension} 
  \end{heading}
compound monad type is $(\alpha N) M = \alpha N M$.
To define a compound monad $NM$, need 
% $$\extNM : (\alpha \to \beta N M) \to (\alpha N M \to \beta N M)$$
\extNM, ``extending'' a function $f$ 
from a ``smaller'' domain, $\alpha$, to a ``larger'' one, $\alpha N M$.

Consider 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*}

Then $\extNM\ f = \extM\ (\pext\ f)$.

Rules (\ref{pextru}) to (\ref{pextfun}) are enough to define $NM$.

About \oNM\ or \unitNM, assume only they have the right types.

Need not assume that $N$ is a monad.
%
\end{slide}

\begin{slide}
  \begin{heading}
{Monad rules for a compound monad using \pext} 
  \end{heading}
\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} 
% \stepcounter{equation} 
\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}
These are just the rules needed for a monad $N$
in \KM % ,  the Kleisli category of $M$.
\end{slide}

\begin{slide}
  \begin{heading}
{Correspondence between monad $N$ and monad $N$ in \KM} 
  \end{heading}

\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  
\end{align*}%
\begin{align*}
\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*}
\end{slide}

\begin{slide}
  \begin{heading}
{To show $NM$ is a monad, using the \pext\ rules} 
  \end{heading}
\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}
To show $NM$ is a monad, want
namely (\ref{krid}NM) to (\ref{omoIass}NM). 

But (\ref{krid}NM) to (\ref{kass}NM)  
same as (\ref{kridK}) to (\ref{kassK});
only (\ref{omoIass}NM) is different.

So need only (\ref{omoIass}NM); to get it, have
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{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*}

\end{slide}

\begin{slide}
  \begin{heading}
{What characterises such compound monads?} 
  \end{heading}
Such compound monads $NM$ satisfy
\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{pextcong} \pext\ f = \pext\ g & \Rightarrow f = g \\
\end{align}

Note, (\ref{J1S}) of the form of 
Theorem~\ref{thm-ext-join-iff}\ref{ej1}.

Conversely, if $M$ and $NM$ are monads, and 
(\ref{J1S}) holds,
then \oNM\ also defines a monad in \KM,
and, using (\ref{PE}) to define \pext, (\ref{EC}) holds.

Proof uses that (\ref{kridK}) to (\ref{kassK})
same as (\ref{krid}NM) to (\ref{kass}NM); \\
shows (\ref{omoIass}K) and (\ref{EC}) from (\ref{J1S}) using 
Theorem~\ref{thm-ext-join-iff}.
\end{slide}

\begin{slide}
  \begin{heading}
{A more general set of rules} 
  \end{heading}
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}
\end{slide}

\begin{slide}
  \begin{heading}
{These also give a monad $NM$} 
  \end{heading}

\begin{theorem} \label{thm-G}
Assume rules (\ref{G1}) to (\ref{G8}).
Then \extNM, \joinNM, \mapNM\ and \unitNM\ give a monad $NM$,
where also
\renewcommand\theequation{G\arabic{equation}}%
\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}

Conversely, for a compound monad $NM$, 
when is this construction applicable?
\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}
\end{slide}

\begin{slide}
  \begin{heading}
{When is the construction applicable?} 
  \end{heading}

How to use Theorem~\ref{thm-Grev}?  Assume (\ref{UC}).
\begin{align}
\unitNM\ f & = \unitM\ (\unitN\ f) \label{UC} \tag{UC} \\
\dunit & = \mapM\ \unitN \tag{DU} \label{DU} \\
\extNM\ \unitM \oo \mapM\ \unitN & = \id \label{G5'} \tag{\ref{G5}$'$} 
\end{align}
If (\ref{J1S}) and the \pext\ construction hold, then 
\emph{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: 
the proof uses $\extNM\ f = \extM (\pext\ f)$.
\comment{
set $f = \unitM$ in
\begin{gather*}
\extNM\ f \oo \mapM\ \unitN = \extM\ (\extNM\ f \oo \unitM) \oo \mapM\ \unitN \\
  = \extM\ (\extNM\ f \oo \unitM \oo \unitN) 
  = \extM\ (\extNM\ f \oo \unitNM) = \extM\ f
\end{gather*}
}

So Theorem~\ref{thm-Grev} applies.
\end{slide}

\begin{slide}
  \begin{heading}
{On the other hand \ldots} 
  \end{heading}
\begin{align}
\extNM\ (\mapM\ \joinN) & = \mapM\ \joinN \oo \joinNM 
  \label{J2'} \tag{J2$'$} 
\end{align}
Note (\ref{J2'}) is also of the form of Theorem~\ref{thm-ext-join-iff}\ref{ej1}.

If $N$ is a monad and $M$ a premonad, 
and (\ref{J2'}) holds, then 
$\extNM\ \unitM = \mapM\ \joinN$ (proved from Theorem~\ref{thm-ext-join-iff}).

In this case (\ref{G5})/(\ref{G5'}) also hold, 
by a seemingly \emph{different} proof.
\begin{gather*}
\extNM\ \unitM  \oo \mapM\ \unitN = \mapM\ \joinN \oo \mapM\ \unitN \\
 = \mapM\ (\joinN \oo \unitN) = \mapM\ \id = \id
\end{gather*}

So again Theorem~\ref{thm-Grev} applies.

Common feature: $\extNM\ \unitM$ is of the form $\extM\ f$,
so Theorem~\ref{thm-ext-join-iff} applies.
\end{slide}

\begin{slide}
  \begin{heading}
{When both (\ref{J1S}) and (\ref{J2'}) hold} 
  \end{heading}

If \emph{both} (\ref{J1S}) and (\ref{J2'}) hold, 
and \emph{both} $M$ and $N$ are monads, then 
we have a distributive law for the monads $M$, $N$ and $NM$.

\end{slide}



\end{document}


