~ohad-kammar/ohads-thesis/trunk

\Section{\cbpv{} with algebraic operations}\sectionlabel{source language}
We need to develop our effect analysis over a concrete concise
language. In order to remain general, we need a fundamental lambda
calculus that is well-designed to deal with effects. Levy's
Call-by-Push-Value~\cite{levy:cbpv-book} fits this description
exactly. The additional benefits of \cbpv{} are: it subsumes both the
call-by-value and call-by-name paradigms, opening application areas in
both \ml{} and \Haskell{}; Pretnar and Plotkin's account of
\defterm{effect
  handlers}~\cite{plotkin-pretnar:effect-handlers-conference,pretnar:thesis}
is formulated in terms of \cbpv{}, hence our account requires less
modifications to accommodate handlers; and, as we will see in
\sectionref{taxonomy}, the \cbpv{} paradigm decomposes complicated
optimisations into orthogonal ones.

\Subsection{Syntax and type system}
We present a family of \cbpv{} languages parametrised by
\defterm{signatures}, at both the syntax and the type system levels. We
begin with the syntax level:
\begin{definition}
  A \defterm{\cbpv{} syntax signature} $\calcParam$ is a triple
  $\seq{\PrimitiveTypes, \Opset, \PrimitiveConstants}$, where:
    \begin{itemize}
    \item $\PrimitiveTypes$ is a set of \defterm{basic types}, ranged
      over by $\mP$; %
    \item $\Opset$ is a set of \defterm{effect operation symbols}, ranged over
      by\/ $\mop$; and
    \item $\PrimitiveConstants$ is a set of \defterm{built-in constants},
      ranged over by $\mconst$.
    \end{itemize}
\end{definition}

For example, $\PrimitiveTypes$ may include the types:
\begin{multicols}{2}
\begin{itemize}
\item $\WordType$ for $64$-bit words;
\item $\LocType$ for memory locations;
\item $\CharType$ for characters;
\item $\StringType$ for strings; and
\item $\ExceptionType$ for exceptions.
\item[]
\end{itemize}
\end{multicols}
The set $\Opset$ may include the operation symbols:
\begin{itemize}
\item $\lookupop$, $\updateop$ for accessing state.
\item $\inputop$, $\outputop$ for reading input and printing output.
\item $\raiseop$ for raising an exception.
\end{itemize}
The set $\PrimitiveConstants$ typically includes primitives to
manipulate basic values, such as:
\begin{multicols}{2}
\begin{itemize}
\item number literals $\num 0$, $\num 1$,
$\num 2$, $\hex{FEED}$;
\item boolean operations $=$, $>=$, $<$;
\item string literals $\stringLiteral{cabab}$;
\item[]
\item string manipulation primitives, e.g. string concatenation
  $\concat$; and
\item predefined exception constants such as
  $\ArithmeticOverflowException$ and
  $\DivideByZeroException$.
\end{itemize}
\end{multicols}

\newcommand\UNDELTA[1]{}
\newcommand\dgor\gor
{
\renewcommand\unignore[1]{}
\renewcommand\dgor{}
\renewcommand\DELTA[1]{}
\renewcommand\UNDELTA[1]{#1}
\renewcommand\e{}
\renewcommand\sfix[5]{}
\renewcommand\cinf{\mathrel{\infer_{\mathrm c}}}
\renewcommand\CompKind[1]{\Kind{Comp}}
\renewcommand\CompTypes{\mathbf{Comp}}
%
Given a syntax signature $\calcParam$, the syntax of \cbpv{} is given
by \figureref{cpbv term syntax}. It follows the \cbpv{} dichotomy
between values and computations. We make this distinction explicit
using a kind system in preparation for the more sophisticated kind
system we will need for the intermediate language in the next
section. Using a kind system for both highlights the differences
between and similarities of the two languages.

Our types are the standard \cbpv{} types.  Note that basic types are
always value types. The unit, product, zero, and sum value types are
standard.  The type $\sU \mB$ is the type of thunks, i.e., suspended
computations, of type $\mB$.  The \defterm{returner type} $\sF\mA$ is
the type of computations that return a value of type $\mA$.  It plays
a similar r\^ ole to that of the monadic type $T\mA$ (where $T$ is a
monad) in Haskell.  We also have products of computations, and
functions that are computations that depend on a value.  The
\defterm{ground value types} $\mGround \in \GroundTypes$ are those
value types which do not include thunks.  We call types of the form
$\sF\mGround$ \defterm{ground returner types}.

All of the built-in constants of \cbpv{} are value terms. The
variables, unit value, and pairing construct are standard.  Injections
are annotated with their sum type.
Computations $\mM$ are
thunked into values $\thunk \mM$.

In \cbpv{}, we can turn any value into a computation by
returning it.   The construct ${\sbind
\mM\mx\mA\mN}$ sequences computations; it is analogous to
the \Haskell{} construct ${\mx\HaskellBind \mM;\mN}$ or the `let'
construct in \ml{}.
Note the intrinsic typing (a.k.a. Church-style typing).

We briefly describe an operational intuition behind the \cbpv{}
syntax.
The standard operational semantics of \cbpv{} uses a stack
machine, similar to other stack machines for call-by-value and
call-by-name semantics of the lambda calculus, such as Felleisen and
Friedman's
CK-machine~\cite{felleisen-friedman:control-operators-the-secd-machine-and-the-lamda-calculus}
and the Krivine machine\footnote{Jean-Louis Krivine, {{\it Un
      interpr\'{e}teur du $\lambda$-calcul}}, unpublished, 1986.}.  The two $\lambda$ terms pop
from the stack while the application terms
$\apply\mValue\mM$ and $\apply{\indx i}\mM$ push the onto it.
Thus, $\cpair{\mM_1}{\mM_2}$ pops a \defterm{tag} off the
stack and executes $\mM_1$ or $\mM_2$ accordingly.  In turn,
$\apply{\indx1}\mM$ pushes the tag $\indx1$ onto the stack and
continues to execute $\mM$.  Similarly, $\abst\mx\mA\mM$ pops a
value of type $\mA$ and binds $\mx$ to it, while $\apply\mValue\mM$ pushes $\mValue$
onto the stack.

\begin{figure}
\Include{syntax-fig}
\caption{\cbpv{} syntax}\figurelabel{cpbv term syntax}
\end{figure}







The pattern-matching terms eliminating products, zero and sum values
are standard. Thunked computations are eliminated by forcing.
%Recursion is expressed by least fixed-points, as usual.

  Importantly, computational effects are caused by the $\mop_{\mV}^{\mB}\mM$ terms.  As an
  example, the following computation consists of a memory lookup operation, dereferencing memory
  location $\loc$, followed by returning the memory word $\var w$ stored there:
  \[
  \derefop \parent{\ell} \definedby \lookupop_{\loc}^{\sF\WordType}\parent{\abst{\var
      w}{\WordType}{\,\return\ {\var w}}}
  \]
  The \defterm{effect operation symbol} $\lookupop$ takes as a
  \defterm{parameter} the location $\ell$ to be dereferenced. It then
  dereferences the memory word at location $\ell$, binds the result to
  $\var w$, and proceeds to execute $\return\ {\var w}$.

  As another example, consider a non-deterministic choice operator
  $\chooseop$, and a computation for non-deterministic coin tossing:
  \[
  \tossop \definedby \chooseop_{\unitval}^{\sF(\unittype\vplus\unittype)}\parent{\abst {\var
      v}{\unittype\vplus\unittype}{\,\return{\,\var v}}}
  \]
  In this case the parameter is the unit value $\unitval$.

  In general, $\mop_{\mV}^{\mB}\mM$ is an effect operation term with
  {parameter} $\mValue$ and \defterm{argument $\mM$}.  Terms of the form
  \[
  \generic\mop^{\e}\parent\mV\definedby
  \mop_{\mValue}^{\sF\mA}\parent{\abst\mx\mA{\,\return\mx}}
  \]
  are called \defterm{generic effects}.
  Thus $\derefop^{\e}$ and $\tossop^{\e}$ are the generic effects
  corresponding to $\lookupop$ and $\chooseop$\
  respectively.
  %(We suppress the parameter $\unitval$ whenever possible.)

\begin{figure}
\Include{cbpv-kind-system}
\caption{\cbpv{} kind system}\figurelabel{kind-system}
\end{figure}

The kind system for \cbpv{}, given a syntax signature $\calcParam{}$,
is displayed in \figureref{kind-system}; it consists of a kind
judgement relation $\kinf$ between types and kinds.  We denote by
$\ValueTypes$ the set of well-kinded value types $\set{\mV\,
  \suchthat\, \kinf \mV \of \ValueKind}$.  Similarly, we write
$\CompTypes$ for the set of well-kinded computation types.  Normally,
\cbpv{} is not presented with a kind system, as the kind system can be
enforced by the BNF grammar for types. Thus, $\ValueTypes$ contains
all value types, and $\CompTypes$ includes all computation
types. A \defterm{well-kinded context} ${\mG \of \Domain
  \mG \to \ValueTypes}$ is a function from a \emph{finite} set of
variables to $\ValueTypes$.  We write $\G, \mx \of \mA$ for the
extension $\G[\mx\mapsto \mA]$.

Given a term signature $\calcParam{}$, an \defterm{arity assignment}
$\sarityfun\! \of\!\Opset \to \GroundTypes\times\GroundTypes$ sends
elements of $\Opset$ to pairs of ground types.  When
$\sarityfun(\mop) = \pair{\sArity}{\sParam}$ we write instead $\mop \of
\sarity{\sArity}{\sParam}$. The first component $\sArity$ is called the
\defterm{arity type} and the second component $\sParam$ is called the
\defterm{parameter type}.  When the parameter type is $\sParam =
\unittype$ we simply write ${\mop \of \sArity}$.  When ${\mop \of
\zerotype}$ we call $\mop$ an \defterm{(effect) constant symbol}.

%
For example, ${\lookupop \of \sarity{\WordType}{\LocType}}$ as
memory look-up takes a location as parameter and its argument expects
the corresponding memory word.  Similarly, $\chooseop \of
\twotype$ where, $\twotype = \unittype \vplus\unittype$, as $\chooseop$ has a trivial parameter.
We say that $\chooseop$ is a \defterm{binary} operation symbol.
%

A \defterm{constant type assignment} is any function
$\constType\placeholder\of\PrimitiveConstants\to\ValueTypes$.
Example constant type assignments are:
\begin{align*}
\charLiteral a &\of
  \CharType\\
\concat &\of
\sU(\funtype{\parent{\StringType\vprod\StringType}}{\sF\,\StringType})
\\
+ &\of \sU(\funtype{\WordType\vprod\WordType}{\sF\,\WordType})
\\
\callcc\mValue\mB & \of \funtype{\sU({\funtype{\sU({\funtype\mValue\mB})}{\mB}})}\mB
\end{align*}

We define type level \cbpv{} signatures, and complete the parametrisation
of our \cbpv{} language:
\begin{definition}
  A \defterm{\cbpv{} signature} is a triple $\typeParam = \seq{\calcParam, \sarityfun,
    \constType\placeholder}$ %
  where: %
  \begin{itemize}
  \item $\calcParam$ is a \cbpv{} term signature; %
  \item $\sarityfun$ is an arity assignment for $\calcParam$; and %
  \item $\constType\placeholder \of \PrimitiveConstants \to \ValueTypes$
  is a \defterm{constant type assignment} for $\calcParam$.
  \end{itemize}
\end{definition}

\begin{figure}
\Include{cbpv-type-system}
\caption{\cbpv{} type system}\figurelabel{type-system}
\end{figure}

 The type system of \cbpv{},  given a signature  $\typeParam$,
 is displayed in \figureref{type-system}; it is given by  type judgement relations ${\mG \vinf \mV \of
\mA}$ and ${\mG \cinf \mM \of \mB}$, where $\mG$, $\mA$, $\mB$ are well-kinded contexts,
value types and computation kinds, respectively, and where $\mV$, $\mM$
are value and computation terms, respectively.
%
Signatures $\typeParam$ determine the language of \cbpv{}, meaning its syntax and kind and typing relations.
We call closed ground returners $\cinf \mProgram
\of \sF\mGround$ \defterm{programs}.
%consists of \effcalc{} along with $\calcParam$'s kind system and
%$\typeParam$'s type system.


The type system is straightforward, apart from the rules for effect operation symbols. %
The effect operation rules
formalise the informal explanation given earlier.  Another way to
view this rule is via continuation passing --- we pass a continuation $\mM$
that,
depending on the effect's result, proceeds after the effect has been
caused.  %
For example, the rules for the I/O effects $\inputop \of \Char$ and
$\outputop \of \sarity\unittype\Char$ are:
\[
\infrule{
  \G \cinf \mM \of \funtype\Char \mB
}{
  \G \cinf \inputop^{\mB} \mM \of \mB
}\quad
\infrule{
  \G \vinf \mV \of \Char
  \quad
  \G \cinf \mM \of \funtype \unittype\mB
}{
  \G \cinf \outputop_{\mV}^{\mB}\mM \of \mB
}
\]
The latter is analogous to Levy's ${\tt print}$ statement
\cite{levy:cbpv-book}.  For the corresponding generic
effects we derive the familiar $\getop^{\e}$, $\putop^{\e}$:
\[
\G \cinf \getop^{\e}\of\sF\,\Char
\qquad
\infrule{
  \G \vinf \mV \of \Char
}{
  \G \cinf \putop^{\e}\of \sF\unittype
}
\]

\begin{theorem}
  Every well-kinded type has a unique kind, and every well-typed term
  has a unique type.
\end{theorem}

\begin{proof}
Standard induction.
\end{proof}

We define capture avoiding substitution in the usual manner. We will
only substitute value terms for variables. The variable binders are
the following constructs:
\begin{itemize}
\item $\sbind \mM\mx\mA\mN$  binds $\mx$ in $\mN$;
\item $\abst \mx\mA\mM$ binds $\mx$ in $\mM$;
\item $\prodmatch \mValue{\mx_1}{\mA_1}{\mx_2}{\mA_2}\mM$ binds
  $\mx_1$ and $\mx_2$ in $\mM$; and
\item $\plusmatch \mValue{\mx_1}{\mA_1}{\mM_1}{\mx_2}{\mA_2}{\mM_2}$
  binds $\mx_1$ in $\mM_1$ and $\mx_2$ in $\mM_2$.
\end{itemize}
As usual, we identify terms up to $\alpha$-equivalence.

\begin{lemma}[substitution]
For every well-typed phrase (value term or computation term) $\mG \infer
\mPhrase \of \mX$, for all well-kinded contexts $\mGv$ and $\Dom\mG$-indexed family of values
$\mValue_{\placeholder}$, satisfying, for all ${\mx \in \Dom\mG}$, $\mGv \infer
\mValue_{\mx} \of \mG(\mx)$, we have $\mGv \infer
\Substitution\mPhrase{\Assign{\mValue_{\mx}}\mx}_{\mx\in\Dom\mG}$.
\end{lemma}
\begin{proof}
Standard induction.
\end{proof}

\newpage
\Subsection{Categorical semantics}
\cats
We now turn to the denotational semantics of \cbpv{}. Let $\ValCat$ be
a distributive category, and $\calcParam$ a \cbpv{} syntax signature. A
\defterm{base-type interpretation} is an assignment of a $\ValCat$-object
$\msemPrim\mP$ to every basic type $\mP \in \PrimitiveTypes$.  This
assignment extends to a \defterm{ground-type interpretation}
$\msemGround\placeholder$, which assigns, to every $\mGround \in
\GroundTypes$ a $\ValCat$-object:
\begin{gather*}
  \msemGround{\mP} \definedby \msemPrim\mP
  \\
  \begin{aligned}
  \msemGround{\unittype}  &\definedby \terminal
  &
  \msemGround{\mGround_1\vprod\mGround_2}  &\definedby
  \msem{\mGround_1}\times\msem{\mGround_2}
  \\
  \msemGround{\zerotype} &\definedby \initial
  &
  \msemGround{\mGround_1\vplus\mGround_2} &\definedby
  \msem{\mGround_1}+\msem{\mGround_2}
  \end{aligned}
\end{gather*}
We will henceforth omit the name of the semantic function if it can be
inferred from the context.
For example, we may choose $\msemPrim{\WordType}$ and
$\msemPrim{\LocType}$ to be $\mathbb{2}^{64}$ in a $64$-bit setting, and
$\msemPrim{\CharType}$ to be $\mathbb{2}^7$ for {\sc ASCII} characters.
As these interpretations are finite  sets, every ground type involving them
denotes a finite set.

\begin{figure}
\Include{cbpv-semantics-type-system}
\caption{\cbpv{} type interpretation}\figurelabel{type-system-semantics}
\end{figure}

Let $\pair\ValCat\Monad$ be a \cbpv{} model. Denote by $\F
\leftadjointto \carrier\placeholder \of
\AlgebraCat\ValCat\Monad\to\ValCat$ the Eilenberg-Moore resolution
for the monad $\Monad$. Given a term signature  $\calcParam$ and a
base-type interpretation $\msemGround{\placeholder}$, we define a
\defterm{type interpretation} for kind judgements of types (see \figureref{type-system-semantics}):
\begin{itemize}
\item values are interpreted as $\ValCat$-objects via
  $\msemVal\placeholder$; %
\item computations are interpreted as $\AlgebraCat\ValCat\Monad$-objects,
i.e., algebras, via $\msemComp\placeholder$; and %
\item  contexts as finite products in $\ValCat$ via
  $\msemCtxt\placeholder$.
\end{itemize}
This interpretation is straightforward. Note that if $\Algebra_1$,
$\Algebra_2$ are two algebras for $\Monad$, then the product of their
underlying objects, $\carrier{\Algebra_1}\times \carrier{\Algebra_2}$
carries an algebra structure, given by:
\[
\algebra[\Algebra_1\times\Algebra_2] \of
\Monad(\carrier{\Algebra_1}\times\carrier{\Algebra_2})
\xto{\prodmorphism{\Monad\proj1}{\Monad\proj2}}
\Monad\carrier{\Algebra_1}\times\Monad\carrier{\Algebra_2}
\xto{\algebra[\Algebra_1][\placeholder]\times\algebra[\Algebra_2][\placeholder]}
\carrier{\Algebra_1}\times\carrier{\Algebra_2}
\]
The fact that this is indeed an algebra for $\Monad$ follows from the
solution of an exercise in Mac Lane's
book~\cite[Exercise~VI.2.2]{maclane:working-mathematician}. Similarly,
the algebra structure on $\carrier{\Algebra}^{\mV}$ is well-defined
(see \lemmaref{homomorphism lemma}(\ref{homomorphism lemma: exponential})).


Let $\pair\ValCat\Monad$ be a \cbpv{} model, $\typeParam$ a \cbpv{}
signature, and $\msemPrim\placeholder$ a base-type
interpretation. We define a type assignment $\msemArities\sarityfun$ for
$\Opset$ in $\ValCat$ by assigning ${\mop
\of \arity{\msem{\sArity}}{\msem{\sParam}}}$ to every $\mop \in
\Opset$, $\mop \of \arity\sArity\sParam$.

With these notions in place, we are ready to define the semantic data
required for modelling \cbpv{} with effects:
\begin{definition}\definitionlabel{cbpv lang cat model}
  Let $\typeParam$ be a \cbpv{} signature. A
  \defterm{$\typeParam$-model} $\mModel$ is a quintuple
  \[
  \seq{\ValCat, \msemPrim\placeholder, \Monad, \opsem[]\placeholder,
    \msemConst\placeholder}
  \] where:
\begin{itemize}
\item $\ValCat$ is a distributive category;
\item $\msemPrim\placeholder$ is a basic-type assignment;
\item $\seq{\ValCat, \Monad, \msem\sarityfun, \opsem[]\placeholder}$ is a \cbpv{}
  $\Opset$-model (cf. \definitionref{non-hierarchical cbpv model});
\item $\msemConst\placeholder$ assigns to every constant $\mconst \in
  \PrimitiveConstants$ an arrow
  \[
  \msemConst\mconst \of \terminal \to \msem{\constType\mconst}
  \]
  \end{itemize}
\end{definition}

Let $\mModel = \seq{\ValCat, \msemPrim\placeholder, \Monad,
  \opsem[]\placeholder, \msemConst\placeholder}$ be a
$\typeParam$-model.  We interpret the \cbpv{}
terms as follows (see \figureref{cat-term-semantics}):
\begin{itemize}
  \item
  value terms ${\mG \vinf \mValue \of \mA}$ are interpreted as $\ValCat$-morphisms
\[
{\msemValTerm{\mValue} \of \msemCtxt\mG \to \msemVal\mA}
\]
\item computation terms ${\mG \cinf \mM \of \mB}$ are interpreted as
$\ValCat$-morphisms
\[
{\msemCompTerm{\mM} \of \msemCtxt\mG \to
\carrier{\msemComp\mB}}
\]
\end{itemize}
\begin{figure}
\Include{cbpv-cat-term-semantics}
\caption{term interpretation}\figurelabel{cat-term-semantics}
\end{figure}
The type system and the definition of models ensure these denotations
are well-defined. Using $\alpha$-equivalence, we may assume that all
differently bound variable names in terms are distinct. Thus, whenever we extend the
context, we indeed have:
\[
\msemCtxt{\mG,\mx\of\mA} \isomorphic \msem{\mG}\times\msem\mA
\]
In addition, we use the generic model structure to simplify the
denotations of effect operation symbols.

{
\renewcommand\DELTA[1]{\ifmmode{\DELT@{\ensuremath{#1}}}\else\DELT@{{#1}}\fi}
The definition of an \defterm{algebraic} \cbpv{} $\typeParam$-model is
straightforward:
\begin{definition+}{\algebraic{definition}{cbpv lang cat model}}
  Let $\typeParam$ be a \cbpv{} signature. A\DELTA{n \defterm{algebraic}}
  $\typeParam$-model $\mModel$ is a
  \[
  \seq{\DELTA{\regcard}, \ValCat, \msemPrim\placeholder, \DELTA{\mL, \algopsem[]\placeholder},
    \msemConst\placeholder}
  \] where:
\begin{itemize}
\item \DELTA{$\regcard$ is a regular cardinal;}
\item $\ValCat$ is a \DELTA{$\regcard$-Power category};
\item $\msemPrim\placeholder$ is a basic-type assignment;
\item $\seq{\DELTA{\regcard,} \ValCat, \DELTA{\mL_{\placeholder}},
  \msem\sarityfun, \DELTA{\algopsem[]\placeholder}}$ is a\DELTA{n
  algebraic} \cbpv{} $\Opset$-model;
\item $\msemConst\placeholder$ assigns to every constant $\mconst \in
  \PrimitiveConstants$ an arrow
  \[
  \msemConst\mconst \of \terminal \to \msem{\constType\mconst}
  \]
  \end{itemize}
\end{definition+}
Note that part of this definition requires our choice of basic-type
assignment to ensure all operation type assignments are
$\regcard$-presentable objects. We can ensure this condition if all
ground types involved in effect operation type assignments are
interpreted as $\regcard$-presentable objects.  Indeed, as the
$\regcard$-presentable objects in a $\regcard$-Power category are
closed under finite products and coproducts, a simple inductive
argument shows this condition on the type assignment holds in this
case.
}

\Subsection{Set-theoretic semantics}
\nocats{}We now spell out the special case where the semantics is given in
terms of sets and functions, i.e., $\ValCat = \Set$. Let  $\calcParam$ a \cbpv{} term signature. A
\defterm{set-theoretic base-type interpretation} is an assignment of a set
$\msemPrim\mP$ to every basic type $\mP \in \PrimitiveTypes$.  This
assignment extends to a \defterm{ground-type interpretation}
$\msemGround\placeholder$, which assigns, to every $\mGround \in
\GroundTypes$ a set:
\begin{gather*}
  \msemGround{\mP} \definedby \msemPrim\mP
  \\
  \begin{aligned}
  \msemGround{\unittype}  &\definedby \terminal
  &
  \msemGround{\mGround_1\vprod\mGround_2}  &\definedby
  \msem{\mGround_1}\times\msem{\mGround_2}
  \\
  \msemGround{\zerotype} &\definedby \initial
  &
  \msemGround{\mGround_1\vplus\mGround_2} &\definedby
  \msem{\mGround_1}+\msem{\mGround_2}
  \end{aligned}
\end{gather*}
We will henceforth omit the name of the semantic function if it can be
inferred from the context.
For example, we may choose $\msemPrim{\WordType}$ and
$\msemPrim{\LocType}$ to be $\mathbb{2}^{64}$ in a $64$-bit setting, and
$\msemPrim{\CharType}$ to be $\mathbb{2}^7$ for {\sc ASCII} characters.
As these interpretations are finite  sets, every ground type involving them
denotes a finite  set.

\begin{figure}
  \renewcommand\F{\Monad}
  \renewcommand\carrier[1]{\mathcal{C}#1}
\Include{cbpv-semantics-type-system}
\cap+{\revisit{figure}{type-system-semantics}}{\cbpv{} type interpretation}
\end{figure}

Let $\Monad$ be a monad over $\Set$. Given a syntax signature  $\calcParam$ and a
base-type interpretation $\msemGround{\placeholder}$, we define a
\defterm{type interpretation} for kind judgements of types (see
\figureref{type-system-semantics}), where each type is interpreted as
a set.  Note that each interpretation of a computation type
$\msemComp\mB$ comes equipped with a bind function \[
\mathord{\MonadicBind{}{}} \of \Monad\mX \times (\msemComp\mB)^{\mX} \to \msemComp\mB
\] For the types $\Monad\msem\mA$ (i.e., returners), the function $\MonadicBind{}{}$ is the usual monadic bind
function. For the computation products, given any $\ta$ in
$\Monad\mX$ and $f$in $\msem\mB^{\mX}$, we define:
\[
\MonadicBind\ta f \definedby \pair{\MonadicBind \ta{f_1}}{\MonadicBind
\ta{f_2}}
\]
where $f_i\of \mX \to \msem{\mB_i}$ are the two component functions of
$f$, i.e., for all $\mx$ in $\mX$, $f(x)$ consists of the pair $\pair {f_1(x)}{f_2(x)}$.
For function types, given any $\ta$ in $\Monad\mX$ and $\alpha$ in $\parent{\msem{\mB}^{\mY}}^{\mX}$, we define:
\[
\MonadicBind \ta \alpha \definedby \lam\my{\parent{\MonadicBind\ta {\lam\mx {\alpha(\mx)(\my)}}}}
\]

Let $\Monad$ be a strong monad over $\Set$, $\typeParam$ a \cbpv{}
signature, and $\msemPrim\placeholder$ a base-type
interpretation. We define a set-theoretic type assignment $\msemArities\sarityfun$ for
$\Opset$ by assigning $\mop
\of \arity{\msem{\sArity}}{\msem{\sParam}}$ to every $\mop \in
\Opset$.

With these notions in place, we are ready to define the semantic data
required for modelling \cbpv{} with effects using sets and functions:
\begin{definition+}{\revisit{definition}{cbpv lang cat model}}
  Let $\typeParam$ be a set-theoretic \cbpv{} signature. A
  \defterm{set-theoretic $\typeParam$-model} $\mModel$ is a quadruple
  \[
  \seq{\Monad, \msemPrim\placeholder, \genopsem[]\placeholder,
    \msemConst\placeholder}
  \] where:
\begin{itemize}
\item $\msemPrim\placeholder$ is a basic-type assignment;
\item $\Monad$ is a monad over $\Set$;
\item $\genopsem\placeholder$ assigns to every $\mop\of\arity\Ar\Pa$ in $\Opset$ a generic
  effect $\genopsem\mop \of \msem\Pa\to\Monad\msem\Ar$;
\item $\msemConst\placeholder$ assigns to every constant $\mconst \in
  \PrimitiveConstants$ an element
  \(
  \msemConst\mconst\) in \( \msem{\constType\mconst}
  \).
  \end{itemize}
\end{definition+}

Let $\mModel = \seq{\Monad, \msemPrim\placeholder,
  \genopsem[]\placeholder, \msemConst\placeholder}$ be a set-theoretic
$\typeParam$-model.  We interpret the \cbpv{}
terms as $\mG \infer \mPhrase \of \mX$ as functions $\msem{\mPhrase}
\of \msem\mG \to \msem\mX$ (see \figureref{cat-term-semantics}).
\begin{figure}[tb]
\Include{semantics-elements}
\cap+{\revisit{figure}{cat-term-semantics}}{\cbpv{} term interpretation}
\end{figure}
The denotations have straightforward definitions.  Note our use of the
monadic unit, $\eta$, and bind functions. We denote the empty function
$\emptyset \to \mX$ by $\initialmorphism_{\mX}$. Note how the
type system and the definition of models ensure these
denotations are well-defined.

By replacing the monad with a presentation and the generic effect
with an indexed family of terms we obtain the notion of a
\defterm{presentation $\typeParam$-model}. Each presentation model
yields a set-theoretic model, and hence can be used to interpret \cbpv{}.
}