|
|
|
@ -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 |
|
|
|
|
