WIP

thesis.tex

@@ -2336,8 +2336,9 @@ We will be working mostly with statically typed programming
 languages. The following definition informally describes the core
 components used to construct a statically typed programming language.
 %
-The point here is not to be mathematical rigorous, but rather to give
+The objective here is not to be mathematical
-an idea of what constitutes a programming language.
+rigorous.% but rather to give
+% an idea of what constitutes a programming language.
 %
 \begin{definition}
   A statically typed programming language $\LLL$ consists of a syntax
@@ -2386,7 +2387,45 @@ original language.
       $E(p)$ holds if and only if $E'(p)$ holds for all programs $p$
       generated by $S'$.
   \end{itemize}
+  Conversely, $\LLL'$ is a \emph{conservative restriction} of $\LLL$.
 \end{definition}
+
+We will be using a typed variation of \citeauthor{Felleisen91}'s
+macro-expressivity to compare the relative expressiveness of different
+kinds of effect
+handlers~\cite{Felleisen90,Felleisen91}. Macro-expressivity is a
+syntactic notion based on the idea of macro rewrites as found in the
+programming language Scheme~\cite{SperberDFSFM10}.
+%
+\begin{definition}[Typability-preserving macro-expressiveness]
+  Let both $\LLL = (S, T, E)$ and $\LLL' = (S', T', E')$ be
+  programming languages such that $\SC_1,\dots,\SC_k \in S$ but
+  $\SC_1,\dots,\SC_k \notin S'$. If there exists a translation on
+  syntax constructors $\sembr{-} : S \to S'$ that is homomorphic on
+  all syntax constructors but $\SC_1,\dots,\SC_k$, such that for all
+  $p$ programs generated by $S$
+  %
+  \[
+    \ba{@{~}l@{~}l}
+             &T(p)~\text{holds if and only if}~T'(\sembr{p})~\text{holds}, \\
+             \text{and}& E(p)~\text{holds if and only if}~E'(\sembr{p})~\text{holds}
+    \ea
+  \]
+  %
+  then we say that $\LLL'$ can \emph{macro-express} the
+  $\SC_1,\dots,\SC_k$ facilities of $\LLL$.
+\end{definition}
+%
+% In essence, if $\LLL$ admits a translation into a sublanguage $\LLL'$
+% in a way which respects not only the behaviour of programs but also
+% aspects of their local syntactic structure, then $\LLL'$
+% macro-expresses $\LLL$. If the translation of some $\LLL$-program into
+% $\LLL'$ requires a complete global restructuring, we may say that
+% $\LLL'$ is in some way less expressive than $\LLL$.
+In general, it is not the case that $\sembr{-}$ preserves types, it is
+only required to ensure that the translated term $p$ is typable in
+the target language $\LLL'$
+
 % \dhil{Definition of (typed) programming language, conservative extension, macro-expressiveness~\cite{Felleisen90,Felleisen91}}
 
 % \begin{definition}