\Section{Optimisation taxonomy}\sectionlabel{taxonomy}

We turn to validating effect-dependent optimisations, formulated as
\mail{} equations. This is done semantically, using
\theoremref{conservative restriction soundness and completeness}.  We
divide optimisations into \defterm{structural}, \defterm{local algebraic},
and \defterm{global algebraic} groups.  We validate versions of almost all the
optimisations in \Bentonetal{}, and also some others, not previously
considered in the semantics literature.  The only optimisations
considered by Benton et al.~that we do not treat deal with exception
handlers.

\defterm{Structural optimisations} reflect the general structure of
our models.  %
%
Let $\mailtypeParam$ be a \mail{} signature. Then a {structural
  optimisation} is one that is valid in all \mail{} $\mailtypeParam$-models.  %
%
\figureref{fig:structural} shows example schemes for such
optimisations.  Note that the $\beta$, $\eta$, and sequencing laws are
the standard \cbpv{} equational laws, found in the \cbpv{} literature
\cite{levy:cbpv-book,
  plotkin-pretnar:a-logic-for-algebraic-effects}. As the fragment of
the language they deal with and their denotational semantics are
identical to \cbpv{}, they are indeed true in all \mail{} models.
The equations for effect interaction are validated by straightforward
calculation using the monadic structure and the definition of the
free, product, and exponential algebras for a monad. Finally, the
equations for coercion follow from functoriality of the monad
hierarchy, from basic properties of strong monad morphisms, and from the
definition of effect operation preservation.  The structural
optimisations are the basic transformations in program optimisation,
and they include well-known optimisations, such as: constant unfolding
and propagation, code inlining, common subexpression elimination, and
others.

\begin{figure}
\Include{structural-optimisations}
\caption{\figurelabel{fig:structural}structural optimisations}
\end{figure}

\defterm{Local algebraic optimisations} originate from particular
equations in the Lawvere theory $\mL_{\e}$ associated to a given \mail{}  model. Each equation yields such an optimisation.
%
To derive these optimisations from the equations, one
follows Plotkin and Pretnar~\cite{plotkin-pretnar:a-logic-for-algebraic-effects}.  We just
give an example here. The global state theory for a finite set of
storable values $\StorVal = \set{\mval_1, \ldots, \mval_n}$ includes the
axiom scheme
%
\[\updateop_{\mval_i}\parent{\lookupop\parent{\tx_1, \ldots, \tx_n}}
= \updateop_{\mval_i}\parent{\tx_{\mval_i}}\]
%
The corresponding
algebraic optimisation is
%
\[\updateop_{\mValue}^{\mB}\parent{\lookupop\,\mM} = \updateop_{\mValue}^{\mB}\parent{\apply\mValue\mM}\]
Such transformations are the bread-and-butter of effectful program
optimisation.

\defterm{Global algebraic optimisations} follow from overall, global properties of the
theories.  Each appears in two forms, which we call
\defterm{utilitarian} and \defterm{pristine}.  %
The {utilitarian} form readily applies to program optimisation; the
{pristine} form is shorter and easier to validate, but perhaps less
useful.  For example, the utilitarian{} form of Discard is
%
{\[
\infrule[\e\subset\e']{\G \cinf[\e] \mM \of \sF[\e]\mA
  \qquad\qquad
  \G \cinf[\e'] \mN \of \mB
  }{
    \mModel\models{\sbind{\coerce[\e\subset\e']\mM}\mx\mA\mN = \mN}
  }
\]}
%
and its pristine{} form  is
%
{\[
\infrule{\G \cinf[\e] \mM \of \sF[\e]\mA
  }{
  \mModel\models{{\sbind\mM\mx\mA{\return\unitval}=\return\unitval}}
  }
\]
}%
%
The two forms can always be shown
equivalent using structural optimisations.
Instances of both appear in the work of Benton et al.

Validating the global algebraic optimisations denotationally reveals an intimate
connection\footnote{Alex Simpson, private communication.} to
\Fuhrmann's work on the structure of call-by-value
\cite{fuhrmann:structure-of-call-by-value,
  fuhrmann:varieties-of-effects}: each has a characterisation in
semantic terms.  For example, the Discard optimisation holds iff
$\mL_{\e}$ is an \defterm{affine} theory
\cite{kock:bilinearity-and-cartesian-closed-monads,
  jacobs:semantics-of-weakening-and-contraction,
  fuhrmann:structure-of-call-by-value}, that is, iff
$\unit_{\terminal}^{\e} \of \terminal \to \Monad\terminal$ is
an isomorphism.

There are also \defterm{algebraic} characterisations of these semantic
properties.  For example, a theory $\mL$ is affine iff for every
term $t$, ${t(\tx, \ldots, \tx) = \tx}$, that is, iff a
\defterm{global absorption law} holds. (Here, and below, we are displaying \emph{all} the variables of the terms at hand.) Such algebraic properties can be investigated
 using the equational presentation of the theory.  As an example, the theory for
environments $\EnvTheory$ and the semilattice
theory are affine.

\floatstyle{plain}%
\restylefloat{figure}%
\begin{figure}
\hspace{-3.5cm}
\Include{global-optimisations}
\caption{\figurelabel{fig:abstract}Global algebraic optimisations}
\end{figure}
\floatstyle{boxed}%
\restylefloat{figure}%
%
A summary of our results appears in \figureref{fig:abstract}.  In
every row, all the conditions are equivalent in any \mail{} model,
taking the condition in the first column as universally quantified
over all $\epsilon'$ such that $\e' \supset \e, \e_1, \e_2$. As
fully justifying these equivalences will require us to include $36$
proofs, we omit them.  Benton et al.~(\Fuhrmann~\cite{fuhrmann:structure-of-call-by-value,
  fuhrmann:varieties-of-effects}) considered call-by-value analogues
of the optimisations labelled by \BentonSpecialAnnotation{}
(respectively \FuhrSpecialAnnotation{}) in \figureref{fig:abstract},
albeit for particular combinations of effects (respectively for a
fixed monad); \Fuhrmann{} also showed the equivalence of the pristine
and utilitarian form
and the abstract side condition in his setting.


The abstract conditions in \figureref{fig:abstract} use the following
standard categorical notions.  The diagonal function
$\diagonalmap_{\mD} \of \mD \to \mD\times\mD$ is given by
$\diagonalmap(\md) \definedby \pair\md\md$. %
%% Let $\tTheory$ be an inequational theory. %
%% Given a continuous function $f \of \mDv \to \mD$, we can
%% \defterm{lift} it to a homomorphism $\tfreebij{\parent{\tunit\compose
%%     f}} \of \tfree\mDv \to \tfree\mD$.  We denote the underlying map
%% by ${\tMap f \of \carrier{\tfree\mDv} \to \carrier{\tfree\mD}}$. %
%% The \defterm{multiplication} $\mMonadBind{} \of
%% \carrier{\tfree{\carrier{\tfree\mD}}} \to \carrier{\tfree\mD}$ is the
%% underlying map of the homomorphism ${{\tfreebij{\id} \of
%%   \tfree{\carrier{\tfree\mD}} \to {\tfree\mD}}}$. %
%% The \defterm{(left) strength}, $\mStrength{} \of
%% \mDv\times\carrier{\tfree\mD} \to \carrier{\tfree{(\mDv\times\mD)}}$,
%% is given by
%% $\ilam{\pair\mdv\md}{\tfreebij{(\curry\tunit)}(\md)(\mdv)}$. %
%% Similarly we define the \defterm{right strength}, $\mStrength{\prime}
%% \of \carrier{\tfree\mDv}\times\mD \to
%% \carrier{\tfree{(\mDv\times\mD)}}$.
The two \defterm{double strength}
functions \( \mDoubleStrength{}, \mVarDoubleStrength \of
\Monad{\mV}\times\Monad\mVv \to
\Monad{(\mV\times\mVv)} \) are defined by
$\mDoubleStrength = \counit\compose \Monad{\strength'}
\compose \strength$ and by $\mVarDoubleStrength =
\counit\compose\Monad{\strength}\compose\strength'$.

The algebraic characterisations follow from the algebraic
understanding of the monadic structure.  Note how Copy corresponds to
a {global \defterm{idempotency} law}, and how Swap corresponds to
\defterm{commutativity}.  This algebraic presentation using laws is
malleable to manipulation. Slight variations on these two laws generate
the Weak Copy\footnote{Paul B. Levy, private communication.}, and Weak
and Isolated Swap optimisations, which are new in the formal methods
optimisation literature.  Thus, by understanding the semantic origins of
these optimisations in algebraic laws we were able to discover new
ones.
Also note the algebraic condition for Pure
Hoist.  It means that $\mL_{\e}$ is either inconsistent, or the
operations project one of their arguments without effect. %

\label{cbpv-justification:optimisations}
Note too the two hoisting optimisations and compare them to
the structural optimisations dealing with effect operations
(\figureref{fig:structural}).  The simplicity of the latter over the
former suggests that the complications arise from the process of
\emph{thunking} rather than abstracting over variables.  This clean
separation between thunks and abstraction also supports our use of
\cbpv{}.

To summarise, we formalised effect-dependent optimisation and
justified the conservative restriction model construction, in the
set-theoretic case, as a sound and complete model of type-and-effect
analysis. We then used our models to validate and classify existing
optimisations, discover new optimisations, and connect different
strands of the semantics literature.
