WIP

macros.tex

@@ -23,6 +23,8 @@
 \newcommand{\SC}{\ensuremath{\mathsf{S}}}
 \newcommand{\ST}{\ensuremath{\mathsf{T}}}
 \newcommand{\ar}{\ensuremath{\mathsf{ar}}}
+\newcommand{\Tm}{\ensuremath{\mathsf{Tm}}}
+\newcommand{\Ty}{\ensuremath{\mathsf{Ty}}}
 
 %%
 %% Partiality

thesis.tex

@@ -2344,14 +2344,22 @@ rigorous.% but rather to give
   A statically typed programming language $\LLL$ consists of a syntax
   $S$, static semantics $T$, and dynamic semantics $E$ where
   \begin{itemize}
-  \item $S$ is a collection of syntax constructors $\SC_1,\SC_2,\dots$
-    constructing members of each syntactic category of $\LLL$
-    (e.g. terms, types, and kinds);
-  \item $T : S \to \B$ is \emph{typechecking} function, which decides
-    whether a given (closed) term is well-typed; and
+  \item $S$ is a collection of, possibly mutually, inductively defined
+    syntactic categories (e.g. terms, types, and kinds). Each
+    syntactic category contains a collection of syntax constructors
+    with nonnegative arities $\{(\SC_i,\ar_i)\}$ which construct
+    abstract syntax trees. We insist that $S$ contains at least two
+    syntactic categories for constructing terms and types of
+    $\LLL$. We write $\Tm(S)$ for the terms category and $\Ty(S)$ for
+    the types category;
+  \item $T : \Tm(S) \times \Ty(S) \to \B$ is \emph{typechecking}
+    function, which decides whether a given term is well-typed; and
   \item $E : P \pto R$ is an \emph{evaluation} function, which maps
-    well-typed programs $P \subseteq S$ to some unspecified set of
-    answers $R$.
+    well-typed programs
+    \[
+      P \defas \{ M \in \Tm(S) \mid A \in \Ty(S), T(M, A)~\text{is true} \},
+    \]
+    to some unspecified set of answers $R$.
   \end{itemize}
 \end{definition}
 %
@@ -2379,52 +2387,75 @@ original language.
   \emph{conservative extension} of a language $\LLL' = (S', T', E')$
   if the following conditions are met.
   \begin{itemize}
-    \item $S'$ is a proper subset of $S$.
-    \item $\LLL$ preserves the static semantics of $\LLL'$,
-      i.e. $T(p)$ holds if and only if $T'(p)$ holds for all programs
-      $p$ generated by $S'$.
-    \item $\LLL$ preserves the dynamic semantics of $\LLL'$, i.e.
-      $E(p)$ holds if and only if $E'(p)$ holds for all programs $p$
-      generated by $S'$.
+    \item $\LLL$ syntactically extends $\LLL'$, i.e. $S'$ is a proper
+      subset of $S$.
+    \item $\LLL$ preserves the static semantics and dynamic semantics
+      of $\LLL'$, that is $T(M, A) = T'(M, A)$ and $E(M)$ holds if and
+      only if $E'(M)$ holds for all types $A \in \Ty(S)$ and programs
+      $M \in \Tm(S)$.
   \end{itemize}
   Conversely, $\LLL'$ is a \emph{conservative restriction} of $\LLL$.
 \end{definition}
 
+We will often work with translations on syntax between languages. It
+is often the case that a syntactic translation is \emph{homomorphic}
+on most syntax constructors, which is a technical way of saying it
+does not perform any interesting transformation on those
+constructors. Therefore we will omit homomorphic cases in definitions
+of translations.
+%
+\begin{definition}
+  Let $\LLL = (S, T, E)$ and $\LLL' = (S', T', E')$ be programming
+  languages. A translation $\sembr{-} : S \to S'$ on the syntax
+  between $\LLL$ and $\LLL'$ is a homomorphism if it distributes over
+  the syntax constructors, i.e. for every $\{(\SC_i,\ar_i)\}_i \in S$
+  \[
+    \sembr{\SC_i(t_1,\dots,t_{\ar_i})} = \sembr{\SC_i}(\sembr{t_1},\cdots,\sembr{t_{\ar_i}}),
+  \]
+  %
+  where $t_1,\dots,t_{\ar_i}$ are abstract syntax trees. We say that
+  $\sembr{-}$ is homomorphic on $S_i$.
+\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
+languages~\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}.
 %
+Informally, if $\LLL$ admits a translation into a sublanguage $\LLL'$
+in a way which respects not only the behaviour of programs but also
+their local syntactic structure, then $\LLL'$ macro-expresses
+$\LLL$. % If the translation of some $\LLL$-program into $\LLL'$
+% requires a complete global restructuring, then we may say that $\LLL'$
+% is in some way less expressive than $\LLL$.
+%
 \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$
+  programming languages such that the syntax constructors
+  $\SC_1,\dots,\SC_k$ are unique to $\LLL$. If there exists a
+  translation $\sembr{-} : S \to S'$ on the syntax of $\LLL$ that is
+  homomorphic on all syntax constructors but $\SC_1,\dots,\SC_k$, such
+  that for all $A \in \Ty(S)$ and $M \in \Tm(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
+     T(M,A) = T'(\sembr{M},\sembr{A})~\text{and}~
+     E(M)~\text{holds if and only if}~E'(\sembr{M})~\text{holds},
   \]
   %
   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'$
+only required to ensure that the translated term is typable in the
+target language $\LLL'$.
+
+\begin{definition}[Type-respecting expressiveness]
+  Let $\LLL = (S,T,E)$ and $\LLL' = (S',T',E')$ be programming
+  languages and $A$ be a type such that $A \in \Ty(S)$ and
+  $A \in \Ty(S')$.
+\end{definition}
 
 % \dhil{Definition of (typed) programming language, conservative extension, macro-expressiveness~\cite{Felleisen90,Felleisen91}}