~ohad-kammar/ohads-thesis/trunk

\Section{Generic effects}\sectionlabel{generic effects}
Plotkin and
Power~\cite{plotkin-power:algebraic-operations-and-generic-effects}
noted there is another common way to model effects:
\begin{definition}[generic effects]
Let $\Monad$ be a monad over $\ValCat$, and $\Ar$,$\Pa$ be
$\ValCat$-objects.  A \defterm{generic effect of type
  $\arity\Ar\Pa$} is a $\ValCat$-morphism $\mgen \of \Pa\to\Monad\Ar$.
\end{definition}

\begin{example}\examplelabel{generic-effects-example}
  The global state monad has the following two generic effects:
  \[
  \begin{array}{l@{\mspace{125mu}}*{4}{l@{\ }}@{\qquad}*{4}{l@{\ }}}
  &\derefop &\multicolumn{3}{@{}l@{\ }}{\of \StorVal               }&  \setop &\multicolumn{2}{@{}l@{\ }}{\of\arity\terminal\StorVal}       \\
  &\derefop &\of \terminal &\to    & \GlobalStateMonad\StorVal   &  \setop &\of \StorVal  &\to    & \GlobalStateMonad\terminal        \\
  &\derefop &\of \unitval  &\mapsto& \lam{\mval}{\pair\mval\mval}&  \setop &\of \mval_0   &\mapsto& \lam{\mval}{\pair{\mval_0}\unitval}\\
  \multicolumn{9}{l}{
  \text{
    \makebox[\textwidth][l]{\hspace{-.45cm}
  Similarly, the environment and overwrite monads have analogous
  generic effects:}}}\\
    &\derefop &\multicolumn{3}{@{}l@{\ }}{\of \StorVal             }&  \setop &\multicolumn{2}{@{}l@{\ }}{\of \arity\terminal\StorVal} \\
    &\derefop &\of \terminal &\to     & \EnvMonad\StorVal        &  \setop &\of \StorVal  &\to    & \OverwriteMonad\terminal      \\
    &\derefop &\of \unitval  &\mapsto & \lam{\mval}{\mval}       &  \setop &\of \mval_0   &\mapsto& \pair{\inj2{\mval_0}}\unitval
  \end{array}
  \]
  \unhangdisplay[1]
\end{example}

Plotkin and
Power~\cite{plotkin-power:algebraic-operations-and-generic-effects}
noted the following bijection between algebraic operations and
generic effects. While they discussed it in the monadic setting, we
generalise the connection to arbitrary resolutions.

\begin{theorem}\theoremlabel{operations-vs-effects}
  Let $\F \leftadjointto \U \of \CompCat \to \ValCat$ be a resolution
  of a strong monad $\Monad$, and $\Ar$, $\Pa$ be $\ValCat$-objects
  such that all exponentials $(\U\placeholder)^{\Ar}$,
  $(\U\placeholder)^{\Pa}$ exist.  Algebraic operations $\mop \of
  \arity\Ar\Pa$ and generic effects $\mgen \of \arity\Ar\Pa$ are in
  bijection via
  \begin{align*}
    \generic \mop &\definedby
    \Pa
    \xto{\prodmorphism{\ilam\Ar{\unit\compose\proj2}}\Pa}
    \parent{\Monad\Ar}^{\Ar}\times\Pa
    \xto{\mop_{\F\Ar}\times\Pa}
    \parent{\Monad\Ar}^{\Pa}\times\Pa
    \xto{\eval}
    \Monad\Ar
    %
    \\
    %
    \operation \mgen\mC &\definedby
    \ilam\Pa{\parent{
        \parent{\U\mC}^{\Ar}\times\Pa
        \xto{\parent{\U\mC}^{\Ar}\times\mgen}
        \parent{\U\mC}^{\Ar}\times\Monad\Ar
        \xto{\lifting\eval}
        \U\mC
    }}
  \end{align*}
\end{theorem}

\begin{example}\examplelabel{operation vs generic example}
In Examples~\exampleref*{monad morphism example} and
\exampleref*{generic-effects-example} we saw, respectively, an algebraic operation
and a generic effect for the environment monad
$\EnvMonad\mV = \mV^{\StorVal}$:
\[\begin{array}{*{3}{l@{\ }}}
  \lookupop_{{\Algebra[\mXv]}} &\of
  \lam\mval{\malg_{\mval}} &\mapsto
  \lam\unitval{\algebra[{\Algebra[\mXv]}][\lam\mval{\malg_{\mval}}]}
  \\
  \derefop &\of \unitval  p&\mapsto  \lam{\mval}{\mval}
\end{array}
\]
Calculating the corresponding generic effect and algebraic operations yields:
\[\begin{array}{*{3}{l@{\ }}}
  \generic\lookupop &\of \unitval
  &\xmapsto{\prodmorphism{\ilam\Ar{\unit\compose\proj2}}\Pa}
  \pair{\unit}{\unitval}
  \xmapsto{\lookupop_{\F_{\Environment}}\times\Pa}
  \pair{\lam\unitval{\monmult\compose\unit_{\F}}}{\unitval}
  \xmapsto{\eval} \lam{\mval}{\mval}
  \\
  \operation\derefop{{\Algebra[\mXv]}} &\of
  \lam\mval{\my_{\mval}}
  &\mapsto \lam\unitval{
    {\lifting\eval}(\lam\mval\my_{\mval}, \lam{\hat\mval}{\hat\mval})
  }
    =
    \lam\unitval{\algebra[{\Algebra[\mXv]}][\lam{\mval}{\eval(\lam{\hat\mval}{\my_{\hat\mval}},{\mval})}]}
    =
    \lam\unitval{\algebra[{\Algebra[\mXv]}][\lam{\mval}{\my_{\mval}}]}
\end{array}\]
Therefore, $\generic\lookupop = \derefop$ and $\lookupop = \operation\derefop{}$.

Similar calculations show, for the overwrite monad
$\OverwriteMonad \mV = (\terminal + \StorVal)\times\mV$, we have
$\generic\updateop = \setop$ and $\updateop = \operation\setop{}$.
\end{example}


\begin{proof}%
  The following calculations show that:
  \begin{inparaenum}[(1)]
    \item $\operation\mgen{}$ is an algebraic operation, i.e., $\operation\placeholder{}$ is well-defined;
    \item ${\operation{\generic\mop}{} = \mop}$; and
    \item $\generic{\operation{\mgen}{}} = \mgen$.
  \end{inparaenum}
  These calculations become clearer through string diagrams
  (see, for example, Baez and Stay~\cite{baez-stay:rosetta-stone}).
  However, we keep to commuting diagrams to avoid the overhead imposed by additional notation.

  \begin{enumerate}
  \item For all $f \of \mG \times \mVx \to \U\mC$, we have
    \inlinediagram{proof-algebraic-operations-and-generic-effects-01}
    By appeal to uniqueness from the universal property of exponentials,
    we deduce:
    \inlinediagram{algebraic-operation-definition-02}
    Hence $\operation\mgen{}$ is an algebraic operation.
  \item\label{reusable proof part} Let $\diagonalmap \of \Pa \to \Pa\times\Pa$ be the diagonal
    morphism.  For every $\mC \inObj \CompCat$, we have:
    \inlinediagram{proof-algebraic-operations-and-generic-effects-02}
    where ($*$) follows by universality from the following diagram
    \inlinediagram{proof-algebraic-operations-and-generic-effects-03}
    Therefore, by universality of exponentials,
    $\operation{\generic\mop}{} = \mop$.

  \item Finally, the following diagram shows that
    $\generic{\operation\mgen{}} = \mgen$:
    \inlinediagram{proof-algebraic-operations-and-generic-effects-04}
    \nobreak
  \end{enumerate}
  \vspace{-1cm}
\end{proof}

A close inspection of \theoremref{operations-vs-effects}'s proof
shows that every algebraic operation $\mop \of \arity\Ar\Pa$ is uniquely
determined by the component $\mop_{\F\Ar}$:
\begin{corollary}\corollarylabel{operation-determined-by-free-component}
  Let $\F\leftadjointto \U$ be a resolution of a strong monad
  $\Monad$, and $\Ar$,$\Pa$ be objects such that all exponentials
  $\parent{\U\placeholder}^{\Ar}$,  $\parent{\U\placeholder}^{\Pa}$
  exist.
  For every morphism $g \of
    \parent{\Monad\Ar}^{\Ar}\to\parent{\Monad\Ar}^{\Pa}$ satisfying
    \inlinediagram{algebraic-operation-definition-03} there exists a
    unique algebraic operation $\mop \of \arity\Ar\Pa$ such that
    $\mop_{\F\Ar} = g$.
\end{corollary}

\begin{proof}%
  For uniqueness, note that $\generic\mop$ is completely determined by
  $\mop_{\F\Ar}$, which satisfies the required condition.  Therefore,
  by \theoremref{operations-vs-effects}, $\mop$ is determined uniquely
  by $g$.  For
  existence, given any such $g$, define a generic effect by
  \[
  \mgen \definedby
  \Pa
  \xto{\prodmorphism{\ilam\Ar{\unit\compose\proj2}}\Pa}
  \parent{\Monad\Ar}^{\Ar}\times\Pa
  \xto{g\times\Pa}
  \parent{\Monad\Ar}^{\Pa}\times\Pa
  \xto{\eval}
  \Monad\Ar
  \]
  By \theoremref{operations-vs-effects}, $\mop\definedby
  \operation\mgen{}$ is an algebraic operation. Part~(\ref{reusable
    proof part}) of the proof remains valid if we replace
  $\mop_{\F\Ar}$ by $g$, and $\generic\mop$ by $\mgen$,
  showing that $\mop_{\F\Ar} = g$.
\end{proof}

Thus, algebraic operations are independent of the particular choice of
a resolution of the monad, as $\mop_{\F\Ar}$ depends solely on the monadic
structure.
\begin{corollary}
  Let $\F_1\leftadjointto \U_1$, $\F_2\leftadjointto \U_2$ be resolutions for a strong monad
  $\Monad$, and $\Ar$,$\Pa$ be objects such that all exponentials
  $\parent{\U_i\placeholder}^{\Ar}$,
  $\parent{\U_i\placeholder}^{\Pa}$
  exist for $i=1,2$.
  Algebraic operations $\mop^1\of\arity\Pa\Ar$ for
  $\F_1\leftadjointto\U_1$ and algebraic operations $\mop^2\of\arity\Pa\Ar$ for
  $\F_2\leftadjointto\U_2$ are in bijection via the equation
  \(
  \mop^1_{\F\Ar} = \mop^2_{\F\Ar}
  \).
\end{corollary}
\begin{proof}%
  The condition in
  \corollaryref{operation-determined-by-free-component} involves only
  the monadic structure, which coincides for the two resolutions.
\end{proof}

Therefore, our definition for algebraic operations captures precisely
Plotkin and Power's notion of algebraic
operations~\cite{plotkin-power:algebraic-operations-and-generic-effects},
but is applicable to resolutions other than the Kleisli and Eilenberg-Moore resolutions.
In the sequel we will therefore speak of algebraic operations for a
monad without referring to a particular resolution of that monad.

\begin{definition}
  Let $\MonadMorphism\of\Monad\to\hat\Monad$ be a strong monad
  morphism, and $\mgen, \mgenv \of \arity\Ar\Pa$ be two generic
  effects for $\Monad, \hat\Monad$ respectively.
  We say that \defterm{$\MonadMorphism$ maps $\mgen$ to $\mgenv$}
  if
  \inlinediagram{generic-operation-preservation-00}
\end{definition}

\begin{example}\examplelabel{generic monad morphism example}
  In \exampleref{generic-effects-example} we encountered the lookup
  and update effects for the environment and global state monad:
    \[
  \begin{array}{l@{\mspace{125mu}}*{4}{l@{\ }}@{\qquad}*{4}{l@{\ }}}
  &\derefop^{\GlobalState[]} &\of \unitval  &\mapsto& \lam{\mval}{\pair\mval\mval}&  \setop^{\GlobalState[]} &\of \mval_0   &\mapsto& \lam{\mval}{\pair{\mval_0}\unitval}\\
  &\derefop^{\Environment[]} &\of \unitval  &\mapsto & \lam{\mval}{\mval}       &  \setop^{\Overwrite[]} &\of \mval_0   &\mapsto& \pair{\inj2{\mval_0}}\unitval
  \end{array}
  \]
  Recall the two monad morphisms from \exampleref{monad
    morphism example}:
\[
\begin{array}{*{2}{r@{\ }l@{\ }l}}
m_{\Environment[]} &\of \EnvMonad\mV &\to \GlobalStateMonad\mV                            & m_{\Overwrite[]} \of &\OverwriteMonad\mV &\to \GlobalStateMonad\mV
\\
m_{\Environment[]} &\of \lam\mval{\mv_{\mval}} &\mapsto \lam\mval{\pair{\mval}{\mv_{\mval}}} & m_{\Overwrite[]} \of &\pair{\inj1\unitval}{\mv} &\mapsto \lam\mval{\pair\mval\mv} \\
  &                         &                                            &       &\pair{\inj2\mval_0}\mv    &\mapsto \lam\mval{\pair{\mval_0}\mv}
\end{array}
\]
Straightforward calculation shows that $m_{\Environment[]}$ maps
$\derefop^{\Environment[]}$ to $\derefop^{\GlobalState[]}$, and that
$m_{\Overwrite[]}$ maps $\setop^{{\Overwrite[]}}$ to
$\setop^{\GlobalState[]}$.
\end{example}

The bijection between
generic effects and algebraic operations preserves the relation
of being mapped by a monad morphism:
\begin{theorem}\theoremlabel{operations-vs-effects-and-mapping}
  Let $\mop, \mopv \of \arity\Ar\Pa$ be algebraic operations for
  any resolutions $\F\leftadjointto\U$, $\F'\leftadjointto\U'$
  of any strong monads $\Monad$, $\Monadv$, respectively,
  and $\MonadMorphism \of \Monad\to\Monadv$ a strong monad
  morphism.
  Then $\MonadMorphism$ maps $\mop$ to $\mopv$ if and only if
  $\MonadMorphism$ maps $\generic\mop$ to $\generic{\mopv}$.
\end{theorem}

\begin{proof}%
First, assume $\MonadMorphism$ maps $\mop$ to $\mopv$. We have
\inlinediagram{proof-mapping-preservation-01}
where ($*$) follows, by the universal property of exponentials, from
\inlinediagram{proof-mapping-preservation-02}

Conversely, assume $\mgen\definedby \generic\mop$ is mapped to
$\mgenv \definedby \generic{\mopv}$. We then have, for every
object $\mVx$:
\inlinediagram{proof-mapping-preservation-03}
Therefore, by the universal property of exponentials, we have:
\inlinediagram{operation-preservation-02}
and $\MonadMorphism$ maps $\mop$ to $\mopv$.
\end{proof}

If $\MonadMorphism$ maps $\mgen$ to $\mgenv$, then
$\mgen$ is uniquely determined by $\MonadMorphism$ and $\mgen$:
$\mgenv = \MonadMorphism\compose \mgen$.
Theorems~\theoremref*{operations-vs-effects} and
$\theoremref*{operations-vs-effects-and-mapping}$
let us transfer this observation to algebraic operations:
\begin{corollary}\corollarylabel{unique algebraic operation via monad morphism}
  Let $\F\leftadjointto\U$, $\F'\leftadjointto\U'$ be any two
  resolutions of any pair of strong monads $\Monad$, $\Monadv$, and
  ${\MonadMorphism \of \Monad \to \Monadv}$ a strong monad morphism.
  For every algebraic operation ${\mop \of \arity\Ar\Pa}$ of
  $\F\leftadjointto\U$, there exists a unique algebraic operation
  $\mopv\of\arity\Ar\Pa$ of $\F'\leftadjointto\U'$ such that
  $\MonadMorphism$ maps $\mop$ to $\mopv$.
\end{corollary}

\begin{proof}%
  If $\mopv, \mopw \of \arity\Ar\Pa$ are two algebraic
  operations such that $\MonadMorphism$ maps $\mop$ to both $\mopv$
  and $\mopw$, then, by
  \theoremref{operations-vs-effects-and-mapping},
  $\MonadMorphism$ maps $\generic{\mop}$ to both $\generic{\mopv}$
  and $\generic{\mopw}$.  Necessarily,
  $\generic{\mopv} = \generic{\mopw}$.  By
  \theoremref{operations-vs-effects} we deduce that $\mopv =
  \mopw$.
  %
  For existence, by fiat, $\MonadMorphism$ maps $\generic\mop$
  to $\mgenv \definedby \MonadMorphism\compose\generic\mop$.
  \theoremref{operations-vs-effects-and-mapping} implies
  $\MonadMorphism$ maps $\mop$ to $\operation{\mgenv}{}$.
\end{proof}

\begin{example}
  To demonstrate this corollary, recall we found a strong
  monad morphism $\MonadMorphism \of \EnvMonad \to
  \GlobalState$ that maps the algebraic operation for look-up of
  $\EnvMonad$ to that of $\GlobalStateMonad$
  (\exampleref{monad morphism example}), and the generic effect for
  look-up of $\EnvMonad$ to that of $\GlobalStateMonad$
  (\exampleref{generic monad morphism example}).  Finally, recall
  that the generic effect for look-up corresponds to the algebraic
  operation for lookup (\exampleref{operation vs generic example}).
  Therefore, by \corollaryref{unique algebraic operation via monad
    morphism}, the generic effect corresponding to the lookup algebraic
  operation for the global state monad \emph{is} the lookup generic effect
  presented in \exampleref{generic-effects-example}.
\end{example}