From f7ab2dbea6fa651f7541c28ffd079dfc91925221 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Fri, 20 Dec 2019 11:55:57 +0000 Subject: [PATCH] WIP --- macros.tex | 10 ++++- thesis.tex | 128 ++++++++++++++++++++++++++++++++++++++++++----------- 2 files changed, 111 insertions(+), 27 deletions(-) diff --git a/macros.tex b/macros.tex index faa4992..b6030ba 100644 --- a/macros.tex +++ b/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} \ No newline at end of file +\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}}}}{=}}} \ No newline at end of file diff --git a/thesis.tex b/thesis.tex index 527a4b8..e9e235a 100644 --- a/thesis.tex +++ b/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 -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}. +types. Value types comprise the function type $A \to C$, which maps +values of type $A$ to computations of type $C$; the polymorphic type +$\forall \alpha^K . C$ is parameterised by a type variable $\alpha$ of +kind $K$; and the record type $\Record{R}$ represents records with +fields constrained by row $R$. Dually, the variant type $[R]$ +represents tagged sums constrained by row $R$. + +\paragraph{Computation types and effect types} +The computation type $A \eff E$ is given by a value type $A$ and an +effect type $E$, which specifies the effectful operations a +computation inhabiting this type may perform. An effect type +$E = \{R\}$ is constrained by row $R$. + +\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 -semantics. +\subsection{Kind and type environments} +\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}