\Chapter{Introduction}{It took me all night\\To get hold of the right introduction}{Queen}

Pure functional programs are amenable to equational reasoning that
can be used for program optimisation~\cite{santos:thesis}. Practical
programs are \emph{not} pure, involving \emph{computational effects}
such as memory and file access. Unfortunately, computational effects
violate the validity of equational reasoning. However, not every
possible equational transformation is violated by every computational
effect. Code fragments restricted to a smaller set of effects may be
amenable to some of the equational transformations pure code
satisfies. \emph{Gifford-style type-and-effect
  systems}~\cite{lucassen-gifford:polymorphic-effect-systems} are a
light-weight static analysis for annotating each code fragment with
a set of effects it may cause. These effect-annotations provide a
basis for effect-dependent optimisation~\cite{tolmach:hierarchy,
  benton-kennedy-russell:compiling-standard-ml-to-java-bytecodes}.

This thesis concerns the semantic validity of such effect-dependent
optimisations. The \emph{denotational approach} to semantics provides
a natural setting for validating such equational optimisations using
\emph{denotational equivalence.}
Moggi~\cite{moggi:computational-lambda-calculus-and-monads,
  moggi:notions-of-computation-and-monads} established that
collections of effects denote \emph{monads}. Based on his
observation, Tolmach~\cite{tolmach:hierarchy} and Benton et
al.~\cite{benton-kennedy-russell:compiling-standard-ml-to-java-bytecodes}
independently validate effect-dependent optimisations denotationally.
However, their approach suffers from the following drawback,
independently posed by Wadler~\cite{wadler:marriage-conference}:
\begin{quote}
``As hypothesised by Moggi and as born out by practice, most
computational effects can be viewed as a monad. Does this provide the
possibility to formulate a general theory of effects and monads,
avoiding the need to create a new effect system for each new effect?''
\end{quote}
In this thesis we propose a general theory of type-and-effect systems,
and answer Wadler's question in the affirmative.

\Section{Effect-dependent optimisation}
Consider the following illustrative \Ocaml-like code:
\begin{lstlisting}[frame=none]
 let z = 2 in
 let f = fun b -> if z*z > 1
                  then x := if b             %*\label{code mutate state 1} *)
                            then z*z
                            else 4           %*\label{code mutate state 1 end} *)
                  else x := !y + z*z in      %*\label{code mutate state 2}\label{code lookup} *)
 let c = getchar () in                       %*\label{code input} *)
 f (c = 'y')                                 %*\label{code penultimate} *)
 f (c = 'y')                                 %*\label{code ultimate}    *)
\end{lstlisting}
This program mixes functional code with \emph{computational effects}:
lines~\ref{code mutate state 1} and~\ref{code mutate state 2} update a
global memory location \lstinline{x}, line~\ref{code lookup} looks-up
some global state, and line~\ref{code input} reads a character from
the user.

An \emph{optimising compiler} may transform this program to an
equivalent program that is better in some way. The precise nature of
the improvement is not the focus of this thesis, and it may include
run-time efficiency, space utilisation, code size, or energy
consumption. For example, the compiler may transform lines~\ref{code mutate
  state 1}--\ref{code mutate state 2} to the following code,
pre-computing \lstinline{z*z} and reusing the result:
\begin{lstlisting}[numbers=none, frame=none]
let u = z*z
if u > 1
then x := if b
          then u
          else 4
else x := !y + u
\end{lstlisting}
However, the presence of computational effects introduces subtlety to
the optimisation process. For example, the following two program
phrases are
\emph{not} equivalent:
\begin{multicols}2
\begin{lstlisting}[numbers=none, frame=none]
x := !x+1
x := !x+1
\end{lstlisting}
\columnbreak
\begin{lstlisting}[numbers=none, frame=none]
let u = !x+1 in
x := u
x := u
\end{lstlisting}
\end{multicols}
Fortunately, not all computational effects rule out this optimisation. If
\lstinline{y} is a different global memory location, the following two
phrases \emph{are} equivalent:
\begin{multicols}2
\begin{lstlisting}[numbers=none, frame=none]
x := !y+1
x := !y+1
\end{lstlisting}
\columnbreak
\begin{lstlisting}[numbers=none, frame=none]
let u = !y+1 in
x := u
x := u
\end{lstlisting}
\end{multicols}
More generally, if the only effects a program phrase may cause are
restricted to reading from one memory region $\mreg_1$ and writing to
a different memory region $\mreg_2$, this phrase may be safely
reused. Thus, the compiler may first analyse the program to determine
which computational effects each phrase causes. For this purpose, in
the presence of higher-order functions, the simplest such effect
analysis is a \defterm{Gifford-style type-and-effect
  system}~\cite{lucassen-gifford:polymorphic-effect-systems}, which
assigns to each phrase both a type and a \emph{set} of effects it may
cause. Thus, the \lstinline{then} branch on lines~\ref{code mutate
  state 1}--\ref{code mutate state 1 end} will be assigned the type
\lstinline{int} and the effect set
$\set{\mathrm{read}_{\mreg_1}}$. More formally, Gifford and Lucassen
introduced type-and-effect judgements $\Gamma \infer M \of A!\e$,
which state that $M$ has type $A$ and effect $\e$ in context
$\Gamma$. For example:
\[
\ocaml{b : bool}, \ocaml{x : Loc}_{\mreg_1} \infer \text{\lstinline{x := if b then z*z else 4}} \of
\ocaml{unit} ! \set{\mathrm{write}_{\mreg_1}}
\]
The typing rules then propagate effects, for example:
\begin{mathpar}
  \inferrule{\Gamma \infer M \of \mathtt{bool} ! \e_1
  \quad
  \Gamma \infer N \of B ! \e_2
  \quad
  \Gamma \infer K \of B ! \e_3
  }{\Gamma \infer
  \mathbf{if}\ M\ \mathbf{then}\  N\ \mathbf{else}\ K \of B ! \e_1 \union
  \e_2 \union \e_3}
\end{mathpar}
Note that we gloss over how to \emph{slice} the global memory locations
into regions, as it is not the focus of this thesis. Henglein et
al.~\cite[Section~3.6]{henglein-makholm-niss:effect-types-and-region-based-memory-management}
discuss such effect inference, focussing on Tofte and Birkedal's
inference
algorithm~\cite{tofte-birkedal:a-region-inference-algorithm,birkedal-tofte:a-constraint-based-region-inference-algorithm}.

Crucially, type-and-effect systems admit higher-order treatment. We
refine function types $A\xto{\hphantom\e}B$ with effect annotations $A
\xto{\e} B$ that state that the functions may cause effects in $\e$
during their execution. The rules for abstraction and application
propagate the effects as follows:
\begin{mathpar}
\inferrule{\Gamma,x \of A \infer M \of B!\e}{\Gamma \infer \abst x
  AM\of (A\xto{\e}B)!\emptyset}

\inferrule{\Gamma \infer M \of A\xto{\e}B!\e' \quad
\Gamma\infer N \of A ! \e''}{\Gamma \infer M N \of B ! \e \union \e'
  \union \e''}
\end{mathpar}
Thus, the type-and-effect assigned to the function \lstinline{f} in our sample
program is:
\[
\lstinline{x} \of \lstinline{Loc}_{\mreg_1}, \lstinline{y} \of \lstinline{Loc}_{\mreg_2}, \lstinline{z} \of \lstinline{int} \infer \lstinline{f} \of
(\lstinline{bool} \xto{\set{\mathrm{write}_{\mreg_1},
    \mathrm{read}_{\mreg_2}}} \lstinline{int})!\emptyset
\]

Using such type-and-effect systems (\emph{effect systems} for brevity), we can now precisely describe
when it is safe to reuse a piece of code:
\begin{mathpar}
  \inferrule{
    \Gamma \infer M \of A ! \e \quad \Gamma, x : A, y : A \infer N \of
    B ! \e'
  }{
   \boxed{\begin{aligned}[c]
      &\mathtt{{\bf let}\ x = }\ M\ \mathtt{\bf in}\ \\
      &\mathtt{{\bf let}\ y = }\ M\ \mathtt{\bf in}\ \\
      &N
    \end{aligned}} \quad=\quad
   \boxed{\begin{aligned}[c]
      &\mathtt{{\bf let}\ x = }\ M\ \mathtt{\bf in}\ \\
      &\mathtt{{\bf let}\ y = }\ x\ \mathtt{\bf in}\ \\
      &N
    \end{aligned}}}
  \parent{\begin{array}{l}
   \scriptstyle\text{for all $\mreg$, }\set{\mathrm{read}_{\mreg},
       \mathrm{write}_{\mreg}} \nsubset \e
   \\\scriptstyle\e\subset
   \Union_{\mreg'}\set{\mathrm{read}_{\mreg'},
     \mathrm{write}_{\mreg'}}
  \end{array}}
\end{mathpar}
Thus, an optimising compiler should implement a decision procedure
guaranteeing the side condition before transforming the
source code to an equivalent variant using this equation. Such a
compiler may then transform lines~\ref{code penultimate}--\ref{code
  ultimate} in the sample program above as follows, using the
effect-dependent optimisation in the transition marked ($*$):
\begin{align*}
   \boxed{\begin{aligned}[c]
      &\lstinline{f(c = 'y')}\\
      &\lstinline{f(c = 'y')}
    \end{aligned}} \quad&=\quad
   \boxed{\begin{aligned}[c]
      &\mathtt{{\bf let}\ u = }\ \lstinline{f(c = 'y')}\ \mathtt{\bf in}\ \\
      &\mathtt{{\bf let}\ v = }\ \lstinline{f(c = 'y')}\ \mathtt{\bf in}\ \\
      &\mathtt{v}
    \end{aligned}} \quad\explain={($*$)}\quad
   \boxed{\begin{aligned}[c]
      &\mathtt{{\bf let}\ u = }\ \lstinline{f(c = 'y')}\ \mathtt{\bf in}\ \\
      &\mathtt{{\bf let}\ v = }\ \mathtt{u}\ \mathtt{\bf in}\ \\
      &\mathtt{v}
    \end{aligned}} \quad\\\\&=\quad
   \boxed{\begin{aligned}[c]
      &\mathtt{{\bf let}\ u = }\ \lstinline{f(c = 'y')}\ \mathtt{\bf in}\ \\
      &\mathtt{u}
    \end{aligned}} \quad=\quad \boxed{\lstinline{f(c = 'y')}}
\end{align*}

This thesis addresses three issues arising from this situation.
First, we need to guarantee that the side conditions on the optimisations are \emph{sound:}
if the side condition holds, then applying the transformation does result in
equivalent code.  In order to do so, we need to relate the syntactic
information included in the effect system to the semantics of the
program~\cite{benton:on-the-relationship-between-formal-semantics-and-static-analysis}.
Thus, the second issue we address is the semantics of the effect
annotated language, and its relationship to the original, unannotated
code.  Finally, we would like the side condition to be
\emph{complete:} if it is safe to apply this optimisation based on the
effect annotations, then the side condition is satisfied. For
example, the computational effects in our source language may also
include \emph{exceptions}. Then, the side condition given above is
\emph{not} complete: the optimisation is valid in the presence of
exceptions, i.e., $\e$ may contain the `$\throwop$' effect.

\Section{Denotational semantics for effect systems}
Our goal is to study the validity of equations between annotated
program terms. Therefore, the natural approach to the
semantics of effect systems is \emph{denotational}. Briefly, in the
denotational approach each program phrase is assigned a mathematical
object that captures its meaning by composing the meanings of its
sub-phrases. Thus, such semantics for an effect annotated language
makes \emph{denotational equality} a natural notion of validity for equations
between effect-analysed program phrases.

Historically, the validation of effect-dependent optimisations using
the denotational approach only took place following Moggi's unification of
effectful denotational semantics using
\emph{monads}~\cite{moggi:computational-lambda-calculus-and-monads,
  moggi:notions-of-computation-and-monads}, and its popularisation by
Wadler~\cite{wadler:comprehending-monads,
  wadler:the-essence-of-functional-programming}. With monads in place,
the connection between type-and-effect systems and monads was
independently published during the same year by
Wadler~\cite{wadler:marriage-conference},
Tolmach~\cite{tolmach:hierarchy}, and Benton et
al.~\cite{benton-kennedy-russell:compiling-standard-ml-to-java-bytecodes}.


To describe the connection concretely, consider a language whose
effects are interactions with a single global memory cell
capable of storing values from some set $\StorVal$.  We may interact
with this memory cell in two ways: we either \defterm{look-up} the
stored value, or \defterm{update} it to store a new value.  Languages
involving such a memory cell are modeled by the \defterm{global state}
monad
$\GlobalStateMonad[] \mX \definedby (\StorVal\times \mX)^{\StorVal}$.
Thus, a computation is modeled by a function
$\lam{\mval}{\pair{\mvalv_{\mval}}{\mvx_{\mval}}}$ mapping an initial
cell state $\mval$ to its new state $\mvalv_{\mval}$ following the
execution, and the return value of the computation $\mvx_{\mval}$. For
example, the function $\lam{\mval}{\pair{42}{\trueval}}$ models a
computation that modifies the cell contents to $42$ and returns the
boolean value $\trueval$.

One way to model the look-up interaction is by the following family
of functions:
\[
\begin{array}{r@{\ }l@{\ }l}
\opsem[]{\lookupop}_{\mX} \of &\parent{\GlobalStateMonad[]\mX}^{\StorVal} &\to
\GlobalStateMonad[]\mX
\\
\opsem[]{\lookupop}_{\mX} \of
&\lam{\mval_1}{\parent{\lam{\mval_2}{\pair{\mvalv_{\mval_1,\mval_2}}{\mvx_{\mval_1,\mval_2}}}}}
&\mapsto \lam \mval{\pair{\mvalv_{\mval,\mval}}{\mvx_{\mval,\mval}}}
\end{array}
\]
The domain of the function,
$\parent{\GlobalStateMonad[]\mX}^{\StorVal}$, models a given family of
computations para\-met\-rised by the value $\mval_1$ currently stored in the memory
cell.
Given such a family, $\mparcomp = \lam{\mval_1}{\parent{\lam{\mval_2}{\pair{\mvalv_{\mval_1,\mval_2}}{\mvx_{\mval_1,\mval_2}}}}}$, the function
$\opsem[]{\lookupop}(\mparcomp)$ looks-up the current value $\mval$ to
obtain
the computation
\(
\mparcomp (\mval) =
\lam{\mval_2}{\pair{\mvalv_{\mval,\mval_2}}{\mvx_{\mval,\mval_2}}}
\).  As such look-ups do
not affect the value stored in the cell, the execution is modeled by
applying the selected computation, $\mparcomp (\mval)$, to $\mval$,
resulting in \(
\mparcomp(\mval)(\mval) =
\lam \mval{\pair{\mvalv_{\mval,\mval}}{\mvx_{\mval,\mval}}}
\).

Similarly, updates are modeled by a family of functions
\[
\begin{array}{r@{\ }l@{\ }l}
\opsem[]{\updateop}_{\mX} \of &{\GlobalStateMonad[]\mX} &\to
\parent{\GlobalStateMonad[]\mX}^{\StorVal}
\\
\opsem[]{\updateop}_{\mX} \of &
\lam\mval{\pair{\mvalv_{\mval}}{\mvx_{\mval}}}
&\mapsto \lam{\mval_0}{\lam \mval{\pair{\mvalv_{\mval_0}}{\mvx_{\mval_0}}}}
\end{array}
\]
Thus, given a computation \(
\mcomp = \lam\mval{\pair{\mvalv_{\mval}}{\mvx_{\mval}}}
\) to be executed after the update, and given a value $\mval_0$ to
update the cell contents to $\mval_0$,
we model the update by ignoring, or overwriting, the currently stored
value $\mval$, and passing to $\mcomp$ the new value $\mval_0$ as the currently stored
state, resulting in \(
\mcomp(\mval_0) = {\lam \mval{\pair{\mvalv_{\mval_0}}{\mvx_{\mval_0}}}}
\).

Next, consider a language whose effects are interactions
with a single global \emph{read-only} memory cell for
$\StorVal$. In this scenario, the only interaction of interest is a memory
look-up. This language is modeled by
the \defterm{environment} monad $\EnvMonad[]\mX \definedby
\mX^{\StorVal}$.
%
The look-up interaction is modeled by the family:
\[
\begin{array}{r@{\ }l@{\ }l}
\opsem[]{\lookupop}_{\mX} \of &\parent{\EnvMonad[]\mX}^{\StorVal} &\to
\EnvMonad[]\mX
\\
\opsem[]{\lookupop}_{\mX} \of
&\lam{\mval_1}{\parent{\lam{\mval_2}{\mvx_{\mval_1,\mval_2}}}}
&\mapsto \lam \mval{\mvx_{\mval,\mval}}
\end{array}
\]
This time there is no need to return a new state for the cell, as the computation may not change
it.

Similarly, consider a language whose effects are
interactions with a single global \emph{write-only} cell for
$\StorVal$.  In this case, the only interaction of interest is a
memory update. This language is
modeled by the \defterm{overwrite} monad ${\OverwriteMonad[]\mX
\definedby (\terminal + \StorVal)\times\mX}$, a particular instance of
the more general \defterm{writer} monad, also called the
\defterm{complexity} monad, and the \defterm{monoid} monad.  These computations, in
addition to returning an $\mX$-value after execution, summarise the
change in the memory cell. The left injection, $\inj1\unitval$, models
a computation that leaves the cell unchanged. The right injections,
$\inj2\mval$, where $\mval\in\StorVal$, model computations that change the contents of the cell
to $\mval$.
%
The update interaction is modeled by the family:
\[
\begin{array}{r@{\ }c@{}l}
\opsem[]{\updateop}_{\mX} \of &{\OverwriteMonad[]\mX} &\to
\parent{\OverwriteMonad[]\mX}^{\StorVal}
\\
\opsem[]{\updateop}_{\mV} \of &\pair\updateaction\mx &\mapsto
\begin{cases}
  \lam{\mval_0}{\pair{\inj2{\mval_0}}\mx}   & \updateaction =
  \inj1\unitval \\
  \lam{\mval_0}{\pair{\inj2{\mval}}\mx}   & \updateaction =
  \inj2\mval
\end{cases}
\end{array}
\]

Finally, in this effectful context, a pure language, i.e.~a language
without side-effects, is modeled by the \defterm{identity} monad
$\IdentityMonad\mX \definedby \mX$.

In this setting, Wadler, Tolmach, and Benton made the following observation. In
\floatstyle{plain}%
\restylefloat{figure}%
\begin{wrapfigure}r{4cm}
\begin{center}
\vspace{-1cm}
\inlinediagram*{test-01}
\vspace{-1cm}
\end{center}
\end{wrapfigure}%
\floatstyle{boxed}%
\restylefloat{figure}%
 a language consisting of a single global memory cell,
there are four possible effect sets: $\emptyset$, $\set{\mathrm{read}}$,
$\set{\mathrm{write}}$, and $\set{\mathrm{read},\mathrm{write}}$.
These
sets are ordered by inclusion to form an \defterm{effect hierarchy}.
For each effect set $\e$ in
the effect hierarchy there is a corresponding monad $\Monad_{\e}$:
\[
 \Monad_{\set{\mathrm{read}, \mathrm{write}}} \definedby
 \GlobalStateMonad[]  \qquad\Monad_{\set{\mathrm{read}}}\definedby
 \EnvMonad[] \qquad \Monad_{\set{\mathrm{write}}}\definedby\OverwriteMonad[]
\qquad
\Monad_{\emptyset} \definedby \IdentityMonad
\]

Corresponding to each effect set inclusion, there is an obvious monad
morphism.  For example, the monad morphism from $\Monad_{\emptyset}$
to $\Monad_{\set{\updateop}}$ is given by
$\mval\mapsto{\pair{\inj1\unitval}{\mval}}$, which
\defterm{lifts} a
pure computation returning $\mval$ to a computation that does not
change the state and returns $\mval$.
As another example, the monad
morphism from $\Monad_{\set{\lookupop}}$ to
$\Monad_{\set{\lookupop,\updateop}}$
is
\floatstyle{plain}%
\restylefloat{figure}%
\begin{wrapfigure}r{4cm}
\begin{center}
\vspace{-1cm}
\inlinediagram*{test-04}
\vspace{-1cm}
\end{center}
\end{wrapfigure}%
\floatstyle{boxed}%
\restylefloat{figure}%
given by $\mcomp\mapsto{\lam\mval{\pair\mval{\mcomp{\mval}}}}$,
lifting a read-only computation $\mcomp$ to a computation that
inspects the current state, but does not change it.  Thus the effect
set hierarchy has a corresponding hierarchy of monads and monad
morphisms.
Consequently, computations only involving the interaction
in each effect set $\e$ can be interpreted within the monad
$\Monad_{\e}$, or lifted to monads above it in the hierarchy.

Wadler's contribution~\cite{wadler:marriage-conference,
  wadler:marriage-journal} is to identify the type-and-effect
judgements $M \of A ! \e$ in a Gifford-style type-and-effect system
for a language with multiple regions with monadic type judgements $M
\of \Monad_{\e}A$ in a multi-monadic language.  He then considers the
two languages as a variants of Moggi's computational lambda-calculus
and the computational
meta-language~\cite{moggi:computational-lambda-calculus-and-monads}.
His technical contribution shows that Moggi's translation from the
former to the latter preserves the types, effects, type-and-effect
derivations and inference, and operational semantics of the
Gifford-style language.  Wadler concludes by noting the monadic
hierarchy \emph{sans} the monad morphisms, and conjectures the
existence of these morphisms. As Wadler only considers a language
whose effects consist of memory allocation and access, he poses the
question regarding the existence of a general theory of
type-and-effect systems.

Tolmach's contribution~\cite{tolmach:hierarchy} consists of a
type-and-effect system for a recursive language with exceptions and
state. His effect hierarchy consists of a linearly-ordered partial
order of abstract effects (and not effect sets):
\[
ID \leq LIFT \leq EXN \leq ST
\]
which correspond to the effect sets
\[
\emptyset \subset \set{\mathrm{diverge}} \subset
\set{\mathrm{diverge}, \mathrm{exception}}
\subset \set{\mathrm{diverge}, \mathrm{exception}, \mathrm{read}, \mathrm{write}}
\]
where `$\mathrm{exception}$' means the program may throw an exception,
and `$\mathrm{diverge}$' means the program may diverge in a loop.
Tolmach uses this effect hierarchy to validate some effect-dependent
optimisations using his denotational equivalence. Tolmach outlines how
his approach generalises to the complete lattice of subsets, or, more generally, to
any lattice. However, he reports on the following problem:
\begin{quote}
``The lack of a generic mechanism for combining monads is rather
unfortunate, since it turns the proofs of many transformation laws
into lengthy case analyses.''
\end{quote}

We divide this problem into two causes. The first is Wadler's
question: it is unclear how to obtain the hierarchy of monads.  The
second caveat is that the Tolmach-style models require specifying
overwhelming amounts of data. In the small global state example we
gave earlier we had to deal with four monads, four effect interactions
and four monad morphisms.  In general, we expect a number of monads,
effect interactions, and monad morphisms exponential in the number of
effects.  Paired, these two caveats greatly restrict our ability to
present such models for realistic cases, as we will require lengthy
definitions and case-by-case analyses.

Benton et al.'s work in this area began with an optimising compiler
from \sml{} to \Java{} bytecodes that uses a monadic intermediate
language for effect-dependent
optimisations~\cite{benton-kennedy-russell:compiling-standard-ml-to-java-bytecodes}. In
a continued line of work, \Bentonetal{}
validate the optimisations employed by this compiler using
Tolmach-style models, independently from Tolmach. The key advantage of
the Benton et al.~models is their \emph{uniformity}.  For every effect
set $\e$, they define a monad $\Monad_{\e}$ as a function of $\e$.
This uniform definition saves much repetitiveness and tediousness in
the account for the language and optimisations. For example, a single
argument shows that $\Monad_{\e}$ is a monad, instead of a different
argument for each $\e$. However, Wadler's caveat still applies to
Benton et al.'s approach: each change to the overall set of effects
requires creating a new effect system with new semantics and new
proofs.

Our goal is to address the issues encountered by Wadler, Tolmach, and
Benton et al.~by developing a \emph{general} theory of type-and-effect
systems, accounting for all aspects required by effect-dependent
transformations: syntax, type system, effect inference, models, and optimisations
and their validation. Moreover, we strive for an \emph{applicable}
theory that leads to engineering methodologies for optimising
compilers. We thus formulate our thesis:
\begin{framed}\begin{quote}
There exists a general applicable theory of Gifford-style\\
type-and-effect systems.
\end{quote}
\end{framed}
\Section{An algebraic solution}
Our work relies on Plotkin and Power's algebraic theory of
computational
effects~\cite{plotkin-power:algebraic-operations-and-generic-effects,
  plotkin-power:notions-of-computation-determine-monads}.  Plotkin and
Power complement Moggi's monadic account of computational
effects~\cite{moggi:notions-of-computation-and-monads} by revisiting
the well-established connection between universal algebra and
monads~\cite{hyland-power:the-category-theoretic-understanding-of-universal-algebra:lawvere-theories-and-monads}.
Briefly, each equational theory gives rise to a monad, and most monads
used in denotational semantics arise from such theories, with the
notable exception of the continuation monad.

For example, the global state monad $(\StorVal\times(\placeholder))^{\StorVal}$ for a single memory cell storing
values from a finite set $\StorVal = \set{\mval_1, \ldots, \mval_n}$,
$n \geq 2$ arises from the following equational
theory~\cite{plotkin-power:notions-of-computation-determine-monads, mellies:segal-condition-meets-computational-effects}:
  \begin{align}
  \updateop_{\mval}(\updateop_{\mvalv}(\tx))                           &= \updateop_{\mvalv}(\tx)    \label{eq1}\\
  \updateop_{\mval_i}(\lookupop(\tx_1, \ldots, \tx_n))                &= \updateop_{\mval_i}(\tx_i)  \label{eq2}\\
  \lookupop(\updateop_{\mval_1}(\tx), \ldots, \updateop_{\mval_n}(\tx)) &= \tx                      \label{eq3}
  \end{align}
These equations have an operational reading as terms for manipulating
computation. For example, the left side of Equation~\eqref{eq1} reads:
first update the cell to $\mval$, then update it to $\mvalv$, and then
proceed with the computation $\tx$. Thus Equation~\eqref{eq1} states
that later updates override earlier updates. As another example, the
left side of Equation~\eqref{eq2} reads: first update the cell to
$\mval_i$, then look-up the currently stored value, say $\mval_j$, and
proceed with the computation $\tx_j$. Thus, Equation~\eqref{eq2}
states that we look-up the most recently updated value. Similarly,
Equation~\eqref{eq3} states that we do not keep track of the
interaction history if it has no bearing on the rest of the
computation.

Plotkin and
Power~\cite{plotkin-power:algebraic-operations-and-generic-effects}
define \emph{algebraic operations} as families of functions that arise
from syntactic terms such as $\updateop$ and $\lookupop$. For
example, the look-up and update interactions $\opsem[]\lookupop$,
$\opsem[]\updateop$ defined in the previous section are such algebraic
operations for the equational theory for global state.  The following
observation is the fundamental idea underlying this thesis:
\begin{framed}
\begin{quote}
  The annotation effects inside the effect-sets of Gifford-style\\
  type-and-effect systems denote Plotkin and Power's\\
  algebraic operations.
\end{quote}
\end{framed}
Thus, the annotation effects `$\mathrm{read}$' and `$\mathrm{write}$' we used
above denote effect operations $\opsem[]{\lookupop}$ and
$\opsem[]{\updateop}$.  Therefore, in the remainder of the thesis we
use the same name for both annotations and operations.

This observation naturally leads to an algebraic theory of
type-and-effect systems.
\begin{enumerate}
\item We begin with an equational theory as semantics to an effectful
  programming language.
\item The collection of syntactic constructs for algebraic effect
  operations in our language determines the effect annotations.
\item The effect annotations and their correspondence with the
  syntactic constructs determine the syntax, type-and-effect system,
  and effect inference.
\item By restricting the equational theory to the effect annotations
  in each effect-set, we obtain a hierarchy of monads and monad
  morphisms compatible with the effect hierarchy. We call this
  construction the \emph{conservative restriction construction.}
\item We now have both syntax and semantics for formulating and
  validating effect-dependent transformations.
\end{enumerate}
Note the interplay between \emph{structure} and \emph{property}. The
only structure we need to specify is the original, algebraic,
semantics of the programming language. The effect system and the valid
optimisations are then a property arising out of our structure, which
we may choose to investigate or ignore.  As a result, our account is
deeply coupled with the semantics of the language in question.

\Section{Our advantage}
We highlight four key properties of our approach:
\begin{description}
\item[rigorous.] If annotation effects indeed denote algebraic effect
operations, then even a relatively simple language involving ten
different effects will require over a thousand effect sets. A
non-rigorous treatment is therefore error-prone. Moreover, even if such
non-rigorous treatment is subject to thorough testing, it is
impossible to establish the completeness of the validity decision
procedures. Thus a non-rigorous design of effect-dependent
transformations cannot be complete apart from the most trivial cases.
\item[denotational.]Monads provide a mechanism to abstract over
  effects that is not available with axiomatic or operational
  approaches. Moreover, validating the soundness of high-order program
  equalities using operational methods is inherently difficult due to
  contextual equivalence. In contrast, the axiomatic approach is
  inappropriate for establishing the completeness of validity decision
  procedures.
\item[abstract.]As we will see in \chapterref{combination}, our
  abstract and algebraic treatment hides many irrelevant details and
  facilitates delicate algebraic manipulations of symbols. It is
  implausible that such subtle arguments can be applied rigorously and
  without error to large concrete programs.
\item[general.]Our generality allows us to present a systematic,
  rather than ad-hoc, account of the optimisations. For example, as we
  will see in \chapterref{optimisations}, this systematic account
  suggested new effect-dependent optimisations not present in the
  semantics literature.
\end{description}
\Section{Thesis structure}
In order to support our thesis, we establish results in two
directions. First, we show that the semantics of effect systems are a
property of the algebraic semantics. Then, we show how this semantics
accounts for the spectrum of type-and-effect systems and related
concepts.

To provide a general theory, we must support a wide selection of
effects. Even simply adding recursion to the language forces us to
work beyond sets and functions, for example, with an appropriate
notion of domains and continuous functions. For this reason, we
provide evidence that our account can be formulated in \emph{category
  theory}, to encompass the various standard denotational semantics
for effects. Such a formulation encounters two problems.
\begin{itemize}
\item First, not all the notions and tools from equational logic have
  been fully developed for the level of generality required by our categorical
  account~\cite{plotkin:some-varieties-of-equational-logic}.
\item Second, the abstract categorical language hinders the
  accessibility of our account.
\end{itemize}

To address the first problem, we keep the development of
new mathematical tools to a minimum, and reuse existing
accounts as much as possible. Thus, we present only our conservative
restriction construction in its full categorical generality. The other
results are formulated using sets and functions, but structured
in a manner we believe may generalise once the required tools are
developed.

To address accessibility, we spread the required background across the
thesis and introduce it as needed.  We also highlight the
parts of the thesis which require a deeper knowledge of category
theory.

\cats{}The sections indicated with a ``beware cats'' sign assume
deeper, but standard, knowledge of category theory. The assumed
knowledge includes: (co)limits, adjunctions, (co)continuity, and
monads, as covered by Mac Lane~\cite{maclane:working-mathematician},
and symmetric monoidal closed categories, and enrichment, as covered
by Kelly~\cite{kelly:basic-concepts-of-enriched-category-theory}.

\nocats{}The ``cat-free'' parts of this thesis assume only basic
categorical notions, which are common knowledge in the semantics and
functional programming communities. In particular, we assume
familiarity with functors, monads, natural transformations, and monad
morphisms. These parts of the thesis are designed to be understood if
read sequentially, skipping over the sections marked with ``beware
cats''. Of course, while the statements are formulated in these
more accessible terms, their proofs may rely on categorically involved
accounts. The scope of these two modifiers extends to the end of the literary
unit they are introduced in, such as Chapter, Section, or Proof.

The second supporting evidence we present for our thesis is an account
of the various concepts involved in type-and-effect systems and their
optimisations. Due to time and space limitations, we focus on the core
concepts required to study effect-dependent optimisations, namely an
annotated source language and its models, and the optimisations and
their validity. For example, we do \emph{not} study the effect
analysis phase that annotates a given source program with the effect
sets.

\newcommand\contrib[1]{}%\vspace{-1.5\baselineskip}\\\item[Contribution:] #1\\}
The thesis is structured as follows:
\begin{description}
\item[\partref{foundations}] develops the general semantic foundations
  of type-and-effect systems.
\begin{description}
\item[\chapterref{operations}]reviews Plotkin and Power's notion of
  algebraic operations.
\contrib{We generalise algebraic operations from monads to
  adjunctions.}
\item[\chapterref{models}]defines hierarchical categorical models for
  type-and-effect systems.
\contrib{A class of categorical models in which annotation effects
  denote algebraic operations.}
\item[\chapterref{recursion}]refines these models to account
  for languages with recursion.
\item[\chapterref{locally-presentable-categories}]reviews the
  background on locally presentable categories we require.
\contrib{We correct an error in the literature concerning the
  characterisation of countably presentable \wcpo{}s.}
\item[\chapterref{lawvere}]reviews Power's enrichment of equational
  logic via enriched Lawvere theories.
\item[\chapterref{algebraic-models}]specialises the categorical models to
  models arising from Lawvere theories, and presents our categorical conservative
  restriction construction.
\contrib{}
\item[\chapterref{presentations}]presents the conservative restriction
  construction in terms of equational logic, sets, and functions.
\item[\chapterref{predicates}]presents logical relations models for relating the semantics of multiple
  set-theoretic models.
\end{description}
\item[\partref{optimisations}]develops the general theory of
  type-and-effect systems and their effect-dependent optimisations
  based on the semantic foundations.
\begin{description}
\item[\chapterref{language}]presents a general type-and-effect intermediate
  language and its denotational semantics.
\item[\chapterref{optimisations}]develops the notion of
  effect-dependent optimisations, its validity conditions, and
  establishes the soundness and completeness of the conservative
  restriction construction.
\item[\chapterref{combination}]studies how the validity of
  optimisations in combined collections of effects follow from their
  validity in each component collection.
\item[\chapterref{example}]demonstrates a use case for analysing an
  imperative, higher-order language.
\end{description}
\item[\chapterref{conclusion}]concludes and discusses future work.
\item[\appendixref{conventions}]summarises our notational conventions for
cross-references.
\end{description}
