~ohad-kammar/ohads-thesis/trunk

\section{Model generation}\sectionlabel{model generation}
Our goal is to generate most or all of the structure needed by \mail{}
models from a given \cbpv{} model.   Most of the work has been done in
previous chapters, but the choice of built-in constants complicates
matters slightly.

\cats{}One case in which no complication arises is for the
\defterm{benchmark models}, defined in \exampleref{benchmark
  model}. Because these models ignore the effect annotations, the
\cbpv{} semantics and the \mail{} semantics agree on the nose.
\begin{lemma}\lemmalabel{benchmark model}
  Let $\typeParam$ be a \cbpv{} signature, $\mModel = \seq{\ValCat,
    \msemPrim\placeholder, \Monad, \opsem[]\placeholder,
    \msemConst\placeholder}$ a \cbpv{} $\typeParam$-model, and
  $\Signature$ an effect hierarchy.  Let $\seq{\ValCat, \msem\arities,
    \benchmark\Presheaf,
    \opsem[\placeholder][\benchmarksymbol]\placeholder}$ be the
  benchmark model corresponding to the \cbpv{} model $\seq{\ValCat,
    \msem\arities, \Monad, \opsem[]\placeholder}$ (see
  \exampleref{benchmark model}).

  \noindent
  The \defterm{benchmark \mail{} model} $\benchmark\mModel$ is given
  by
  \[
  \seq{\ValCat, \msemPrim\placeholder, \benchmark\Presheaf,
    \opsem[\placeholder][\benchmarksymbol]\placeholder, \msemConst\placeholder}
  \]
  and for every \mail{} type, context, and term $\mX$, we have
  $\benchmark\mModel\msem\mX = \mModel\msem{\erase\mX}$.
\end{lemma}
\begin{proof}%
  Straightforward calculation.
\end{proof}

We can always define benchmark models. However, they completely ignore effect
annotations.  We are interested in obtaining a similar construction for the
\defterm{conservative restriction models} (see \theoremref{categorical
conservative restriction}). However, as the built-in constants may
have arbitrary types and involve arbitrary effects, we do not have a
canonical choice of their types and interpretations.

For example, the arithmetic addition constant in \cbpv{}:
\[
+ \of \sU[](\funtype{\WordType\vprod\WordType}{\sF[]\,\WordType})
\]
can have an effect-dependent type in \mail{}:
\[
+ \of \sU[\set{\ArithmeticOverflowException}](\funtype{\WordType\vprod\WordType}{\sF[\set{\ArithmeticOverflowException}]\WordType})
\]
The situation becomes more complicated with higher-order built-in
constants, due to contravariance.

We have no general solution to this problem. However, the amount of
work involved in choosing the effect annotations and interpretations
for the built-in constants is linear in the number of the built-in
constants. Therefore, we foresee no problems in leaving them
unspecified by our general account, and manually choosing the
appropriate effect annotation and interpretation in any concrete
case. We formulate our results to be of use in this general case.

Nevertheless, under some simplifying assumptions on the \mail{} and
\cbpv{} signatures, we can guarantee a suitable choice of types and
interpretations for the built-in constants. We will describe the
simplest such method, by restricting to a sub-class of signatures,
which we call \defterm{simple signatures}.

\begin{definition}\definitionlabel{simple signature}
A \defterm{simple \mail{} signature} is a \mail{} signature $\mailtypeParam{}$ such
that $\Opset \in \E$, and for each built-in constant $\mconst$, the only effect set
appearing in $\constType\mconst$ is $\Opset$.
\end{definition}
Thus, a simple signature may include number and string literals $\num
1, \hex{FEED} \of \WordType$, and boolean operations $=, >=, < \of
\sU[\Opset](\funtype{\WordType\vprod\WordType}{\sF[\Opset]\twotype})$
but not a pure string concatenation function $\concat \of
\sU[\emptyset](\funtype{\StringType\vprod\StringType}{\sF[\emptyset]\StringType})$.

Our simplifying assumptions are:
\begin{itemize}
\item the \cbpv{} model is algebraic, i.e., given by an enriched
  Lawvere theory $\mL$;
\item the operation set $\Opset$ is surjective, in the sense that the
  (unique) morphism from the initial $\pair{\Opset}{\msem\arities}$
  theory $\SignatureTheory{\pair{\Opset}{\msem\arities}}$ to $\mL$ is
  an $\Epi$-morphism, i.e., surjective in the set-theoretic case; and
\item the \mail{} signature is simple.
\end{itemize}
The first assumption is essential, as we cannot construct the
conservative restriction model otherwise. The second assumption is
reasonable, as it means we include \emph{all} the effects in our
effect analysis. If the initial morphism is not an $\Epi$-morphism, the
theory $\mL$ may include effects that lie beyond the
reach of our type-and-effect analysis. As we discussed, the last
assumption is restrictive, but non-essential. We keep it as it
simplifies the account greatly.

\begin{lemma}
  Let $\mailtypeParam$ be a simple \mail{} signature, $\mModel =
  \seq{\ValCat, \msem\arities, \Monad, \opsem[]\placeholder}$ a
  \cbpv{} $\erasedmailtypeParam$-model, and $\seq{\ValCat,
    \msem\arities, \Presheaf, \opsem[\placeholder]\placeholder}$ a
  $\Sigma$-model.
  %
  If $\Presheaf\Opset = \Monad$, then for every built-in constant
  $\mconst \in \PrimitiveConstants$, the type interpretation of
  $\constType\mconst$ induced by $\Presheaf$ is
  $\mModel\msem{\constType\mconst}$.
\end{lemma}

Let $\FunctorFact\Epi$ be a class of morphisms in $\Lawvere\ValCat$. We say that an algebraic \cbpv{} $\typeParam$-model is \defterm{$\FunctorFact\Epi$-covered} if the initial morphism $\LawHomo \of
  \SignatureTheory{\pair{\Opset}{\msem{\arities}}} \to \mL$ is an
  $\FunctorFact\Epi$-morphism.

\begin{corollary}\corollarylabel{simple signature conservative
    restriction mail model}
  Let $\mailtypeParam$ be a simple \mail{} signature, let \[
  \mModel =
  \seq{\regcard, \ValCat,
    \msemPrim\placeholder, \mL, \algopsem[]\placeholder,
    \msemConst\placeholder}
  \] be
  an algebraic \cbpv{} $\erasedmailtypeParam$-model, and let
  $\pair{\FunctorFact\Epi}{\FunctorFact\Mono}$ be a factorisation system
  of $\Lawvere\ValCat$, such that $\mModel$ is $\FunctorFact\Epi$-covered.
  Let \[
  \seq{\regcard, \ValCat, \msem\arities,
    \mL_{\placeholder},
    \opsem[\placeholder][]\placeholder}
  \] be the
  conservative restriction model corresponding to the \cbpv{} model
  \[
  \seq{\regcard, \ValCat,
    \msem\arities, \mL, \algopsem[]\placeholder}
  \] (see
  \theoremref{categorical conservative restriction}).

  \noindent
  The \defterm{conservative restriction \mail{} model}
  $\conservative\mModel$ is given as the algebraic \mail{}
  $\mailtypeParam{}$-model
  \[
  \seq{\ValCat, \msemPrim\placeholder, \mL_{\placeholder},
    \opsem[\placeholder]\placeholder, \msemConst\placeholder}
  \]
\end{corollary}
\begin{proof}%
  From the assumptions follows that $\mL_{\Opset} \isomorphic \mL$,
  hence by the previous lemma, the interpretation for the built-in
  constants from $\mModel$ can be used in $\conservative\mModel$.
\end{proof}

We now turn to construction of logical relations \mail{} models.
\begin{lemma}\lemmalabel{diagonal lifting of ground types}
  Let $\mailtypeParam$ be a simple \mail{} signature, and let
  $\msemPrim\placeholder$ be the \defterm{diagonal} base-type
  interpretation in $\LogRel$, i.e., for every $\mP \in
  \PrimitiveTypes$, $\msemPrim\mP$ is the diagonal relation. Then, for
  every ground type $\mGround \in \GroundTypes$, $\msemGround\mGround$
  is the diagonal relation.
\end{lemma}
\begin{proof}%
  By induction over ground types, noting that the diagonal relations
  are closed under products and coproducts.
\end{proof}

We will use the following construction to relate different \mail{}
semantics.

\begin{theorem}\theoremlabel{mail model lifting}
  Given a \mail{} signature $\mailtypeParam$, consider any two
  \mail{} $\mailtypeParam$-models sharing the same base-type interpretation:
  \begin{align*}
    \mModel_1&=\seq{\Set, \Presheaf_1, \msemPrim[][0]\placeholder, \opsem[\placeholder][1]\placeholder,
      \msemConst[][1]\placeholder}\\
    \mModel_2&=\seq{\Set, \Presheaf_2, \msemPrim[][0]\placeholder, \opsem[\placeholder][2]\placeholder,
      \msemConst[][2]\placeholder}
  \end{align*}
  Let $\seq{\LogRel, \msem\sarityfun, \Presheaf,
    \opsem[\placeholder]\placeholder}$ be the free lifting of
  the induced $\Signature$-models \[
  \seq{\Set, \msem\sarityfun, \Presheaf_1,
    \opsem[\placeholder][1]\placeholder}
  ,\qquad \seq{\Set, \msem\sarityfun, \Presheaf_2,
    \opsem[\placeholder][2]\placeholder}
  \] via the diagonal lifting of $\msem\sarityfun$.

  Denote by $\msemPrim\placeholder$ the diagonal lifting of the shared base-type interpretation
  $\msemPrim[][0]\placeholder$. The assignment $\msemPrim\placeholder$ and the
  functor $\Presheaf$ then induce a logical relations \mail{} type
  interpretation $\msemVal\placeholder$.

  If, for every $\mconst \in
    \PrimitiveConstants$, the pair
    $\pair{\mModel_1\msem{\mconst}}{\mModel_2\msem{\mconst}}$ lifts to
    a logical relations morphism $\msemConst\placeholder \of \terminal \to
    \msemVal{\constType\mconst}$, then
    \[
    \mModel=\seq{\LogRel, \Presheaf, \msemPrim\placeholder, \opsem[\placeholder]\placeholder,
      \msemConst\placeholder}
    \]
    is a logical relation \mail{} $\mailtypeParam{}$-model. We call
    $\mModel$ the \defterm{free lifting of $\mModel_1$, $\mModel_2$}.
\end{theorem}

\begin{proof}%
  By the previous lemma, $\mModel\msem{\sarityfun}$ is the diagonal lifting
  of $\msem\sarityfun$. Thus, by fiat, $\mModel$ is a \mail{}
  $\mailtypeParam$-model.
\end{proof}

\nocats{}To aid accessibility, we recast the model generation process
in terms of presentations.

\begin{definition+}{\revisit{definition}{simple signature}}
A \defterm{simple \mail{} signature} is a \mail{} signature $\mailtypeParam{}$ such
that $\Opset \in \E$, and for each built-in constant $\mconst$, the only effect set
appearing in $\constType\mconst$ is $\Opset$.
\end{definition+}

We say that a presentation \cbpv{} $\typeParam$-model is
\defterm{fully-covered} if the initial translation from the free
presentation whose signature is generated by $\msemArities\sarityfun$
is surjective. In simpler terms, a model is fully-covered if every term
in its presentation can be expressed using the indexed terms that
define the generic effects of this model.

\begin{corollary+}{\revisit{corollary}{simple signature conservative
      restriction mail model}}
  Let $\mailtypeParam$ be a simple \mail{} signature, let
  \[
  \mModel = \seq{\msemPrim\placeholder, \Ax, \opsem[]\placeholder, \msemConst[]\placeholder}
  \]
  be a fully-covered presentation \cbpv{} $\erasedmailtypeParam$-model.   Let \[
  \seq{\msem\arities,
    \Ax_{\placeholder},
    \opsem[\placeholder][]\placeholder}
  \] be the
  conservative restriction model corresponding to the pair $\Ax$,
  $\opsem[]\placeholder$ (see
  \theoremref+{presentation conservative restriction}).

  \noindent
  The \defterm{conservative restriction \mail{} model}
  $\conservative\mModel$ is given as the presentation \mail{}
  $\mailtypeParam{}$-model
  \[
  \seq{\msemPrim\placeholder, \Ax_{\placeholder},
    \opsem[\placeholder]\placeholder, \msemConst\placeholder}
  \]
\end{corollary+}

To summarise, we defined a general type-and-effect system and its
semantics, and in the algebraic case we constructed the hierarchical
semantics from the \cbpv{} semantics and related them to each other.