From 2fbbf04bd4013d9fd340c8333f3f495be92f9f1c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Fri, 28 May 2021 10:51:07 +0100 Subject: [PATCH] WIP --- macros.tex | 2 ++ thesis.tex | 97 +++++++++++++++++++++++++++++++++++------------------- 2 files changed, 66 insertions(+), 33 deletions(-) diff --git a/macros.tex b/macros.tex index 0d3769f..565e9ef 100644 --- a/macros.tex +++ b/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 diff --git a/thesis.tex b/thesis.tex index 1f6eb1e..533a3cf 100644 --- a/thesis.tex +++ b/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}}