WIP

macros.tex

@@ -44,6 +44,8 @@
 \newcommand{\Effect}{\mathsf{Effect}}
 \newcommand{\Handler}{\mathsf{Handler}}
 
+\newcommand{\ZeroType}{0}
+\newcommand{\UnitType}{1}
 \newcommand{\One}{1}
 \newcommand{\Int}{\mathsf{Int}}
 \newcommand{\Bool}{\mathsf{Bool}}
@@ -84,6 +86,7 @@
 \newcommand{\tylab}[1]{\text{\scshape{T-#1}}}
 \newcommand{\mlab}[1]{\text{\scshape{M-#1}}}
 \newcommand{\siglab}[1]{\text{\scshape{Sig-#1}}}
+\newcommand{\rowlab}[1]{\textrm{\scshape{R-#1}}}
 
 %%
 %% Lindley's array stuff.
@@ -107,4 +110,9 @@
 \newcommand{\reason}[1]{\quad (\text{#1})}
 
 
-\newenvironment{smathpar}{\vspace{-3ex}\small\begin{mathpar}}{\end{mathpar}\normalsize\ignorespacesafterend}
+\newenvironment{smathpar}{\vspace{-3ex}\small\begin{mathpar}}{\end{mathpar}\normalsize\ignorespacesafterend}
+
+%%
+%% Defined-as equality
+%%
+\newcommand{\defas}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\text{def}}}}{=}}}

thesis.tex

@@ -278,31 +278,96 @@ Section~\ref{sec:base-language-type-rules}, respectively.
 Figure~\ref{fig:base-language-types} depicts the syntax for kinds and
 types.
 %
+\paragraph{Value types}
 We distinguish between values and computations at the level of
-types. Value types comprise the function type $A \to C$, whose domain
+types. Value types comprise the function type $A \to C$, which maps
-is a value type and its codomain is a computation type $B \eff E$,
+values of type $A$ to computations of type $C$; the polymorphic type
-where $E$ is an effect type detailing which effects the implementing
+$\forall \alpha^K . C$ is parameterised by a type variable $\alpha$ of
-function may perform. Value types further comprise type variables
+kind $K$; and the record type $\Record{R}$ represents records with
-$\alpha$ and quantification $\forall \alpha^K.C$, where the quantified
+fields constrained by row $R$. Dually, the variant type $[R]$
-type variable $\alpha$ is annotated with its kind $K$. Finally, the
+represents tagged sums constrained by row $R$.
-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
+\paragraph{Computation types and effect types}
-presence variables, $\Comp$ for computation type variables, $\Effect$
+The computation type $A \eff E$ is given by a value type $A$ and an
-for effect variables, and lastly $\Row_{\mathcal{L}}$ for row
+effect type $E$, which specifies the effectful operations a
-variables. The row kind is annotated by a set of labels
+computation inhabiting this type may perform. An effect type
-$\mathcal{L}$. We use this set to track the labels of a given row type
+$E = \{R\}$ is constrained by row $R$.
-to ensure uniqueness amongst labels in each row type. We shall
+
-elaborate on this in Section~\ref{sec:row-polymorphism}.
+\paragraph{Row types}
+Row types play a pivotal role in our type system as effect, record,
+and variant types are uniformly given by row types. A \emph{row type}
+describes a collection of distinct labels, each annotated by a
+presence type. A presence type indicates whether a label is
+\emph{present} with type $A$ ($\Pre{A}$), \emph{absent} ($\Abs$) or
+\emph{polymorphic} in its presence ($\theta$).
+%
+Row types are either \emph{closed} or \emph{open}. A closed row type
+ends in~$\cdot$, whilst an open row type ends with a \emph{row
+  variable} $\rho$ (in an effect row we usually use $\varepsilon$
+rather than $\rho$ and refer to it as an \emph{effect variable}).
+%
+The row variable in an open row type can be instantiated with
+additional labels. Each label may occur at most once in each row (we
+enforce this restriction at the level of kinds). Two rows are
+equivalent if they contain the same labels and both end in either
+$\cdot$ or a row variable $\rho$.
+%
+\begin{mathpar}
+  \inferrule*[Lab=\rowlab{Closed}]
+    {~}
+    {\cdot \equiv_{\mathrm{row}} \cdot}
+
+  \inferrule*[Lab=\rowlab{Open}]
+    {~}
+    {\rho \equiv_{\mathrm{row}} \rho}
+
+  \inferrule*[Lab=\rowlab{Head}]
+    {R \equiv_{\mathrm{row}} R'}
+    {\ell:P;R \equiv_{\mathrm{row}} \ell:P;R'}
+
+  \inferrule*[Lab=\rowlab{Swap}]
+    {R \equiv_{\mathrm{row}} R'}
+    {\ell:P;\ell':P';R \equiv_{\mathrm{row}} \ell':P';\ell:P;R'}
+\end{mathpar}
+%
+The last rule $\rowlab{Swap}$ let us identify rows up to the
+reordering of labels.  For instance, the two rows
+$\ell_1 : P_1; \cdots; \ell_n : P_n; \cdot$ and
+$\ell_n : P_n; \cdots ; \ell_1 : P_1; \cdot$ are equivalent.
+%
+Absent labels in closed rows are redundant.
+%
+The standard zero and unit types are definable using rows. We define
+the zero type as the empty, closed variant $\ZeroType \defas
+[\cdot]$. Dually, the unit type is defined as the empty, closed record
+type, i.e. $\UnitType \defas \Record{\cdot}$. We shall often omit
+$\cdot$ for closed rows.
+
+
+% 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}
@@ -365,8 +430,19 @@ 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
+\subsection{Kind and type environments}
-semantics.
+\label{sec:kind-and-type-environments}
+We define kind and type environments as right-extended sequences
+mapping type variables to and their kinds and terms to their types,
+respectively.
+%
+\begin{syntax}
+  \slab{Kind environments} &\Delta &::=& \cdot \mid \Delta, \alpha:K\\
+  \slab{Type environments} &\Gamma &::=& \cdot \mid \Gamma, x:A
+\end{syntax}
+%
+Having introduced all the syntax, we now move onto introducing the
+static semantics.
 
 \subsection{Kinding rules}
 \label{sec:base-language-kind-rules}