diff --git a/thesis.tex b/thesis.tex index 1ef2e09..527a4b8 100644 --- a/thesis.tex +++ b/thesis.tex @@ -226,26 +226,31 @@ and programming with computational effects. \section{Syntax and static semantics} \label{sec:syntax-base-language} -Typically the presentation of a programming language begins with its -syntax. If the language is typed there are two possible starting -points: Either one presents the term syntax first, or alternatively, -the type syntax first. Although the choice may seem rather benign -there is, however, a philosophical distinction to be drawn between -them. Terms are, on their own, entirely meaningless, whilst types -provide, on their own, an initial approximation of the semantics of -terms. This is particularly true in an intrinsic typed system perhaps -less so in an extrinsic typed system. In an intrinsic system types -must necessarily be precursory to terms, as terms ultimately depend on -the types. Following this argument leaves us with no choice but to -first present the type syntax of \BCalc{} and subsequently its term -syntax. - -\subsection{Types, kinds, and their environments} +In \BCalc{}, types are precursory to terms, as it is intrinsically +typed. Thus we begin by presenting the syntax of its kind and type +structure in Section~\ref{sec:base-language-types}. Subsequently in +Section~\ref{sec:base-language-terms} we present the term syntax, +before presenting the formation rules for kinds and types in +Section~\ref{sec:base-language-kind-rules} and +Section~\ref{sec:base-language-type-rules}, respectively. + +% Typically the presentation of a programming language begins with its +% syntax. If the language is typed there are two possible starting +% points: Either one presents the term syntax first, or alternatively, +% the type syntax first. Although the choice may seem rather benign +% there is, however, a philosophical distinction to be drawn between +% them. Terms are, on their own, entirely meaningless, whilst types +% provide, on their own, an initial approximation of the semantics of +% terms. This is particularly true in an intrinsic typed system perhaps +% less so in an extrinsic typed system. In an intrinsic system types +% must necessarily be precursory to terms, as terms ultimately depend on +% the types. Following this argument leaves us with no choice but to +% first present the type syntax of \BCalc{} and subsequently its term +% syntax. + +\subsection{Types and their kinds} \label{sec:base-language-types} - -Figure~\ref{fig:base-language-types} depicts the syntax for types of -\BCalc{}. - +% \begin{figure} \begin{syntax} \slab{Value types} &A,B &::= & A \to C @@ -259,23 +264,121 @@ Figure~\ref{fig:base-language-types} depicts the syntax for types of \slab{Row types} &R &::= & \ell : P;R \mid \rho \mid \cdot \\ \slab{Presence types} &P &::= & \Pre{A} \mid \Abs \mid \theta\\ %\slab{Labels} &\ell & & \\ -\slab{Handler types} &F &::= & C \Rightarrow D \\ -\slab{Types} &T &::= & A \mid C \mid E \mid R \mid P \mid F \\ +% \slab{Types} &T &::= & A \mid C \mid E \mid R \mid P \\ \slab{Kinds} &K &::= & \Type \mid \Row_\mathcal{L} \mid \Presence - \mid \Comp \mid \Effect \mid \Handler \\ + \mid \Comp \mid \Effect \\ \slab{Label sets} &\mathcal{L} &::=& \emptyset \mid \{\ell\} \uplus \mathcal{L}\\ %\slab{Type variables} &\alpha, \rho, \theta& \\ -\slab{Type environments} &\Gamma &::=& \cdot \mid \Gamma, x:A \\ -\slab{Kind environments} &\Delta &::=& \cdot \mid \Delta, \alpha:K +% \slab{Type environments} &\Gamma &::=& \cdot \mid \Gamma, x:A \\ +% \slab{Kind environments} &\Delta &::=& \cdot \mid \Delta, \alpha:K \end{syntax} - \caption{Syntax of types in \BCalc{}}\label{fig:base-language-types} + \caption{Syntax of types in \BCalc{}.}\label{fig:base-language-types} \end{figure} +% +Figure~\ref{fig:base-language-types} depicts the syntax for kinds and +types. +% +We distinguish between values and computations at the level of +types. Value types comprise the function type $A \to C$, whose domain +is a value type and its codomain is a computation type $B \eff E$, +where $E$ is an effect type detailing which effects the implementing +function may perform. Value types further comprise type variables +$\alpha$ and quantification $\forall \alpha^K.C$, where the quantified +type variable $\alpha$ is annotated with its kind $K$. Finally, the +value types also contains record types $\Record{R}$ and variant types +$[R]$, which are built up using row types $R$. An effect type $E$ is +also built up using a row type. A row type is a sequence of fields of +labels $\ell$ annotated with their presence information $P$. The +presence information denotes whether a label is present $\Pre{A}$ with +some type $A$, absent $\Abs$, or polymorphic in its presence +$\theta$. A row type may be either \emph{open} or \emph{closed}. An +open row ends in a row variable $\rho$ which can be instantiated with +additional fields, effectively growing the row, whilst a closed row +ends in $\cdot$, meaning the row cannot grow further. + +The kinds comprise $\Type$ for regular type variables, $\Presence$ for +presence variables, $\Comp$ for computation type variables, $\Effect$ +for effect variables, and lastly $\Row_{\mathcal{L}}$ for row +variables. The row kind is annotated by a set of labels +$\mathcal{L}$. We use this set to track the labels of a given row type +to ensure uniqueness amongst labels in each row type. We shall +elaborate on this in Section~\ref{sec:row-polymorphism}. \subsection{Terms} \label{sec:base-language-terms} +% +\begin{figure} +\begin{syntax} +\slab{Variables} &x \in \mathcal{N}&&\\ +\slab{Values} &V,W &::= & x + \mid \lambda x^A .\, M \mid \Lambda \alpha^K .\, M + \mid \Record{} \mid \Record{\ell = V;W} \mid (\ell~V)^R \\ + & & &\\ +\slab{Computations} &M,N &::= & V\,W \mid V\,A\\ + & &\mid& \Let\; \Record{\ell=x;y} = V \; \In \; N\\ + & &\mid& \Case\; V \{\ell~x \mapsto M; y \mapsto N\} \mid \Absurd^C~V\\ + & &\mid& \Return~V \mid \Let \; x \revto M \; \In \; N +\end{syntax} + +\caption{Term syntax of \BCalc{}.} +\label{fig:base-language-term-syntax} +\end{figure} +% +The syntax for terms is given in +Figure~\ref{fig:base-language-term-syntax}. We assume countably +infinite set of names $\mathcal{N}$ from which we draw fresh variable +names at will. We shall typically denote term variables by $x$, $y$, +or $z$. +% +The syntax partitions terms into values and computations. +% +Value terms comprise variables ($x$), lambda abstraction +($\lambda x^A . \, M$), type abstraction ($\Lambda \alpha^K . \, M$), +and the introduction forms for records and variants. Records are +introduced using the empty record $\Record{}$ and record extension +$\Record{\ell = V; W}$, whilst variants are introduced using injection +$(\ell~V)^R$, which injects a field with label $\ell$ and value $V$ +into a row whose type is $R$. We include the row type annotation in +order to support bottom-up type reconstruction. + +All elimination forms are computation terms. Abstraction and type +abstraction are eliminated using application ($V\,W$) and type +application ($V\,A$) respectively. +% +The record eliminator $(\Let \; \Record{\ell=x;y} = V \; \In \; N)$ +splits a record $V$ into $x$, the value associated with $\ell$, and +$y$, the rest of the record. Non-empty variants are eliminated using +the case construct ($\Case\; V\; \{\ell~x \mapsto M; y \mapsto N\}$), +which evaluates the computation $M$ if the tag of $V$ matches +$\ell$. Otherwise it falls through to $y$ and evaluates $N$. The +elimination form for empty variants is ($\Absurd^C~V$). +% +There is one computation introduction form, namely, the trivial +computation $(\Return~V)$ which returns value $V$. Its elimination +form is the expression $(\Let \; x \revto M \; \In \; N)$ which evaluates +$M$ and binds the result value to $x$ in $N$. +% + +% +As our calculus is intrinsically typed, we annotate terms with type or +kind information (term abstraction, type abstraction, injection, +operations, and empty cases). However, we shall omit these annotations +whenever they are clear from context. + +Having introduced the syntax, we now move onto introducing the static +semantics. + +\subsection{Kinding rules} +\label{sec:base-language-kind-rules} + +\subsection{Typing rules} +\label{sec:base-language-type-rules} \section{Dynamic semantics} +\section{Row polymorphism} +\label{sec:row-polymorphism} + \section{Type and effect inference} \dhil{While I would like to detail the type and effect inference, it may not be worth the effort. The reason I would like to do this goes