diff --git a/macros.tex b/macros.tex index 9f8168b..0d3769f 100644 --- a/macros.tex +++ b/macros.tex @@ -20,6 +20,9 @@ \newcommand{\Delim}[1]{\ensuremath{\keyw{del}.#1}} \newcommand{\sembr}[1]{\ensuremath{\llbracket #1 \rrbracket}} \newcommand{\BigO}{\ensuremath{\mathcal{O}}} +\newcommand{\SC}{\ensuremath{\mathsf{S}}} +\newcommand{\ST}{\ensuremath{\mathsf{T}}} +\newcommand{\ar}{\ensuremath{\mathsf{ar}}} %% %% Partiality @@ -564,6 +567,7 @@ %% %% Asymptotic improvement macros %% +\newcommand{\LLL}{\ensuremath{\mathcal L}} \newcommand{\naive}{naïve\xspace} \newcommand{\naively}{naïvely\xspace} \newcommand{\Naive}{Naïve\xspace} diff --git a/thesis.tex b/thesis.tex index cb88c16..ac73457 100644 --- a/thesis.tex +++ b/thesis.tex @@ -2332,8 +2332,149 @@ of growth of $f$ is constant. \section{Typed programming languages} \label{sec:pls} +We will be working mostly with statically typed programming +languages. The following definition informally describes the component +of a programming language. % -\dhil{Definition of (typed) programming language, conservative extension, macro-expressiveness~\cite{Felleisen90,Felleisen91}} +The point here is not to be mathematical 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 + $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 $E : P \pto R$ is an \emph{evaluation} function, which maps + well-typed programs $P \subseteq S$ to some unspecified set of + answers $R$. + \end{itemize} +\end{definition} +% +We will always present the syntax of a programming language on +Backus-Naur form. +% +The static semantics will always be given in form a typing judgement +(and a kinding judgement for languages with polymorphism), and the +dynamic semantics will be given as either a reduction relation or an +abstract machine. + +We will take the view that an untyped programming language is a +special instance of a statically typed programming language, where the +typechecking function $T$ is the constant function that always returns +true. + +\begin{definition} + A programming language $\LLL = (S, T, E)$ is said to be a + \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'$. + \end{itemize} +\end{definition} +% \dhil{Definition of (typed) programming language, conservative extension, macro-expressiveness~\cite{Felleisen90,Felleisen91}} + +% \begin{definition} +% A signature $\Sigma$ is a collection of abstract syntax constructors +% with arities $\{(\SC_i, \ar_i)\}_i$, where $\ST_i$ are syntactic +% entities and $\ar_i$ are natural numbers. Syntax constructors with +% arities $0$, $1$, $2$, and $3$ are referred to as nullary, unary, +% binary, and ternary, respectively. +% \end{definition} + +% \begin{definition}[Terms in contexts] +% A context $\mathcal{X}$ is set of variables $\{x_1,\dots,x_n\}$. For +% a signature $\Sigma = \{(\SC_i, \ar_i)\}_i$ the $\Sigma$-terms in +% some context $\mathcal{X}$ are generated according to the following +% inductive rules: +% \begin{itemize} +% \item each variable $x_i \in \mathcal{X}$ is a $\Sigma$-term, +% \item if $t_1,\dots,t_{\ar_i}$ are $\Sigma$-terms in context +% $\mathcal{X}$, then $\SC_i(t_1,\dots,t_{\ar_i})$ is +% $\Sigma$-term in context $\mathcal{X}$. +% \end{itemize} +% We write $\mathcal{X} \vdash t$ to indicate that $t$ is a +% $\Sigma$-term in context $\mathcal{X}$. A $\Sigma$-term $t$ is +% said to be closed if $\emptyset \vdash t$, i.e. no variables occur +% in $t$. +% \end{definition} + +% \begin{definition} +% A $\Sigma$-equation is a pair of terms $t_1,t_2 \in \Sigma$ in +% context $\mathcal{X}$, which we write as +% $\mathcal{X} \vdash t_1 = t_2$. +% \end{definition} + +% The notation $\mathcal{X} \vdash t_1 = t_2$ begs to be read as a +% logical statement, though, in universal algebra the notation is simply +% a syntax. In order to give it a meaning we must first construct a +% \emph{model} which interprets the syntax. We shall not delve deeper +% here; for our purposes we may think of a $\Sigma$-equation as a +% logical statement (the attentive reader may already have realised that . + + +% The following definition is an adaptation of +% \citeauthor{Felleisen90}'s definition of programming language to +% define statically typed programming languages~\cite{Felleisen90}. +% % +% \begin{definition} +% % +% A statically typed programming language $\LLL$ consists of the +% following components. +% % +% \begin{itemize} +% \item A signature $\Sigma_T = \{(\ST_i,\ar_i)\}_i$ of \emph{type syntax constructors}. +% \item A signature $\Sigma_t = \{(\SC_i,\ar_i)\}_i$ of \emph{term syntax constructors}. +% \item A signature $\Sigma_p = \{(\SC_i, +% \item A static semantics, which is a function +% $typecheck : \Sigma_t \to \B$, which decides whether a +% given closed term is well-typed. +% \item An operational semantics, which is a partial function +% $eval : P \pto R$, where $P$ is the set of well-typed terms, i.e. +% % +% \[ +% P = \{ t \in \Sigma_t \mid typecheck~t~\text{is true} \}, +% \] +% % +% and $R$ is some unspecified set of answers. +% \end{itemize} +% \end{definition} +% % + +% An untyped programming language is just a special instance of a +% statically typed programming language, where the signature of type +% syntax constructors is a singleton containing a nullary type syntax +% constructor for the \emph{universal type}, and the function +% $typecheck$ is a constant function that always returns true. + +% A statically polymorphic typed programming language $\LLL$ also +% includes a set of $\LLL$-kinds of kind syntax constructors as well as +% a function $kindcheck_\LLL : \LLL\text{-types} \to \B$ which checks +% whether a given type is well-kinded. + +% \begin{definition} +% A context free grammar is a quadruple $(N, \Sigma, R, S)$, where +% \begin{enumerate} +% \item $N$ is a finite set called the nonterminals. +% \item $\Sigma$ is a finite set, such that +% $\Sigma \cap V = \emptyset$, called the alphabet (or terminals). +% \item $R$ is a finite set of rules, each rule is on the form +% \[ +% P ::= (N \cup \Sigma)^\ast, \quad\text{where}~P \in N. +% \] +% \item $S$ is the initial nonterminal. +% \end{enumerate} +% \end{definition} + % \chapter{State of effectful programming} % \label{ch:related-work} @@ -15181,10 +15322,7 @@ the captured context and continuation invocation context to coincide. \chapter{Asymptotic speedup with effect handlers} \label{ch:handlers-efficiency} -\def\LLL{{\mathcal L}} -\def\N{{\mathbb N}} % - When extending some programming language $\LLL \subset \LLL'$ with some new feature it is desirable to know exactly how the new feature impacts the language. At a bare minimum it is useful to know whether