From aaa862b1c5a8e387aeb39b14332a46769f142615 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Fri, 20 Dec 2019 17:01:35 +0000 Subject: [PATCH] Typing --- macros.tex | 8 +- thesis.tex | 321 +++++++++++++++++++++++++++++++++++++++++++++-------- 2 files changed, 279 insertions(+), 50 deletions(-) diff --git a/macros.tex b/macros.tex index b6030ba..3c2e82b 100644 --- a/macros.tex +++ b/macros.tex @@ -66,6 +66,11 @@ \newcommand{\False}{\mathsf{false}} \newcommand{\eff}{!} +\newcommand{\typ}[2]{#1 \vdash #2} +\newcommand{\typv}[2]{#1 \vdash #2} +\newcommand{\typc}[3]{#1 \vdash #2 \eff #3} + +\newcommand{\FTV}{\ensuremath{\mathrm{FTV}}} %% Handler projections. \newcommand{\hret}{H^{\mathrm{val}}} @@ -82,11 +87,12 @@ %% Labels %% \newcommand{\slab}[1]{\textrm{#1}} +\newcommand{\klab}[1]{\text{\scshape{K-#1}}} \newcommand{\semlab}[1]{\text{\scshape{S-#1}}} \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}}} +\newcommand{\rowlab}[1]{\text{\scshape{R-#1}}} %% %% Lindley's array stuff. diff --git a/thesis.tex b/thesis.tex index e9e235a..eb4c1b8 100644 --- a/thesis.tex +++ b/thesis.tex @@ -230,9 +230,8 @@ 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. +before presenting the formation rules for types in +Section~\ref{sec:base-language-type-rules}. % Typically the presentation of a programming language begins with its % syntax. If the language is typed there are two possible starting @@ -269,14 +268,15 @@ Section~\ref{sec:base-language-type-rules}, respectively. \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, kinds, and their environments.} + \label{fig:base-language-types} \end{figure} % -Figure~\ref{fig:base-language-types} depicts the syntax for kinds and -types. +Figure~\ref{fig:base-language-types} depicts the syntax for types, +kinds, and their environments. % \paragraph{Value types} We distinguish between values and computations at the level of @@ -308,32 +308,31 @@ 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$. +enforce this restriction at the level of kinds). We identify rows up +to the reordering of labels. % -\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. +% \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. % @@ -343,6 +342,97 @@ the zero type as the empty, closed variant $\ZeroType \defas type, i.e. $\UnitType \defas \Record{\cdot}$. We shall often omit $\cdot$ for closed rows. +% +\begin{figure} +\begin{mathpar} +% alpha : K + \inferrule*[Lab=\klab{TyVar}] + { } + {\Delta, \alpha : K \vdash \alpha : K} + +% Computation + \inferrule*[Lab=\klab{Comp}] + { \Delta \vdash A : \Type \\ + \Delta \vdash E : \Effect \\ + } + {\Delta \vdash A \eff E : \Comp} + +% A -E-> B, A : Type, E : Row, B : Type + \inferrule*[Lab=\klab{Fun}] + { \Delta \vdash A : \Type \\ + \Delta \vdash C : \Comp \\ + } + {\Delta \vdash A \to C : \Type} + +% forall alpha : K . A : Type + \inferrule*[Lab=\klab{Forall}] + { \Delta, \alpha : K \vdash C : \Comp} + {\Delta \vdash \forall \alpha^K . \, C : \Type} + +% Record + \inferrule*[Lab=\klab{Record}] + { \Delta \vdash R : \Row_\emptyset} + {\Delta \vdash \Record{R} : \Type} + +% Variant + \inferrule*[Lab=\klab{Variant}] + { \Delta \vdash R : \Row_\emptyset} + {\Delta \vdash [R] : \Type} + +% Effect + \inferrule*[Lab=\klab{Effect}] + { \Delta \vdash R : \Row_\emptyset} + {\Delta \vdash \{R\} : \Effect} + +% Present + \inferrule*[Lab=\klab{Present}] + {\Delta \vdash A : \Type} + {\Delta \vdash \Pre{A} : \Presence} + +% Absent + \inferrule*[Lab=\klab{Absent}] + { } + {\Delta \vdash \Abs : \Presence} + +% Empty row + \inferrule*[Lab=\klab{EmptyRow}] + { } + {\Delta \vdash \cdot : \Row_\mathcal{L}} + +% Extend row + \inferrule*[Lab=\klab{ExtendRow}] + { \Delta \vdash P : \Presence \\ + \Delta \vdash R : \Row_{\mathcal{L} \uplus \{\ell\}} + } + {\Delta \vdash \ell : P;R : \Row_\mathcal{L}} +\end{mathpar} +\caption{Kinding Rules} +\label{fig:base-language-kinding} +\end{figure} +% + +\paragraph{Kinds} +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 formation rules for kinds are given in +Figure~\ref{fig:base-language-kinding}. The kinding judgement +$\Delta \vdash T : K$ states that type $T$ has kind $K$ in kind +environment $\Delta$. +% +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. For example, the kinding rule +$\klab{ExtendRow}$ uses this set to constrain which labels may be +mentioned in the tail of $R$. We shall elaborate on this in +Section~\ref{sec:row-polymorphism}. + +\paragraph{Environments} +Kind and type environments are right-extended sequences of bindings. A +kind environment binds type variables to their kinds, whilst a type +environment binds term variables to their 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$, @@ -430,25 +520,156 @@ kind information (term abstraction, type abstraction, injection, operations, and empty cases). However, we shall omit these annotations whenever they are clear from context. -\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. +\subsection{Typing rules} +\label{sec:base-language-type-rules} % -\begin{syntax} - \slab{Kind environments} &\Delta &::=& \cdot \mid \Delta, \alpha:K\\ - \slab{Type environments} &\Gamma &::=& \cdot \mid \Gamma, x:A -\end{syntax} +\begin{figure} +Values +\begin{mathpar} +% Variable + \inferrule*[Lab=\tylab{Var}] + {x : A \in \Gamma} + {\typv{\Delta;\Gamma}{x : A}} + +% Abstraction + \inferrule*[Lab=\tylab{Lam}] + {\typ{\Delta;\Gamma, x : A}{M : C}} + {\typv{\Delta;\Gamma}{\lambda x^A .\, M : A \to C}} + +% Polymorphic abstraction + \inferrule*[Lab=\tylab{PolyLam}] + {\typv{\Delta,\alpha : K;\Gamma}{M : C} \\ + \alpha \notin FTV(\Gamma) + } + {\typv{\Delta;\Gamma}{\Lambda \alpha^K .\, M : \forall \alpha^K . \,C}} +\\ +% unit : () + \inferrule*[Lab=\tylab{Unit}] + { } + {\typv{\Delta;\Gamma}{\Record{} : \Record{}}} + +% Extension + \inferrule*[Lab=\tylab{Extend}] + { \typv{\Delta;\Gamma}{V : A} \\ + \typv{\Delta;\Gamma}{W : \Record{\ell:\Abs;R}} + } + {\typv{\Delta;\Gamma}{\Record{\ell=V;W} : \Record{\ell:\Pre{A};R}}} + +% Inject + \inferrule*[Lab=\tylab{Inject}] + {\typv{\Delta;\Gamma}{V : A}} + {\typv{\Delta;\Gamma}{(\ell~V)^R : [\ell : \Pre{A}; R]}} +\end{mathpar} +Computations +\begin{mathpar} +% Application + \inferrule*[Lab=\tylab{App}] + {\typv{\Delta;\Gamma}{V : A \to C} \\ + \typv{\Delta;\Gamma}{W : B} + } + {\typ{\Delta;\Gamma}{V\,W : C}} + +% Polymorphic application + \inferrule*[Lab=\tylab{PolyApp}] + {\typv{\Delta;\Gamma}{V : \forall \alpha^K . \, C} \\ + \Delta \vdash A : K + } + {\typ{\Delta;\Gamma}{V\,A : C[A/\alpha]}} + +% Split + \inferrule*[Lab=\tylab{Split}] + {\typv{\Delta;\Gamma}{V : \Record{\ell : \Pre{A};R}} \\\\ + \typ{\Delta;\Gamma, x : A, y : \Record{\ell : \Abs; R}}{N : C} + } + {\typ{\Delta;\Gamma}{\Let \; \Record{\ell =x;y} = V\; \In \; N : C}} + +% Case + \inferrule*[Lab=\tylab{Case}] + { \typv{\Delta;\Gamma}{V : [\ell : \Pre{A};R]} \\\\ + \typ{\Delta;\Gamma,x:A}{M : C} \\\\ + \typ{\Delta;\Gamma,y:[\ell : \Abs;R]}{N : C} + } + {\typ{\Delta;\Gamma}{\Case \; V \{\ell\; x \mapsto M;y \mapsto N \} : C}} + +% Absurd + \inferrule*[Lab=\tylab{Absurd}] + {\typv{\Delta;\Gamma}{V : []}} + {\typ{\Delta;\Gamma}{\Absurd^C \; V : C}} + +% Return + \inferrule*[Lab=\tylab{Return}] + {\typv{\Delta;\Gamma}{V : A}} + {\typc{\Delta;\Gamma}{\Return \; V : A}{E}} +\\ +% Let + \inferrule*[Lab=\tylab{Let}] + {\typc{\Delta;\Gamma}{M : A}{E} \\ + \typ{\Delta;\Gamma, x : A}{N : C} + } + {\typ{\Delta;\Gamma}{\Let \; x \revto M\; \In \; N : C}} +\end{mathpar} +\caption{Typing Rules} +\label{fig:base-language-type-rules} +\end{figure} % -Having introduced all 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} +The typing rules are given by +Figure~\ref{fig:base-language-type-rules}. The \tylab{Var} rule states +that a variable $x$ has type $A$ if $x$ is bound to $A$ in the type +environment $\Gamma$. The \tylab{Lam} rules states that a lambda value +$(\lambda x.M)$ has type $A \to C$ if the computation $M$ has type $C$ +assuming $x : A$. In the \tylab{PolyLam} rule we make use of the set +of \emph{free type variables} (FTV). +% +We define FTV by mutual induction over type environments, $\Gamma$, +and the type structure: +% +\[ + \ba[t]{@{~}l@{~~~~~~}c@{~}l} +\begin{eqs} + \FTV(\alpha) &\defas& \{\alpha\}\\ + \FTV(\forall \alpha^K.C) &\defas& \FTV(C) \setminus \{\alpha\}\\ + \FTV(A \to C) &\defas& \FTV(A) \cup \FTV(C)\\ + \FTV(A \eff E) &\defas& \FTV(A) \cup \FTV(E)\\ + % \FTV(\{R\}) &\defas& \FTV(R)\\ + % \FTV(\Record{R}) &\defas& \FTV(R)\\ + % \FTV([R]) &\defas& \FTV(R)\\ + % \FTV(l:P;R) &\defas& \FTV(P) \cup \FTV(R)\\ + % \FTV(\Pre{A}) &\defas& \FTV(A)\\ + % \FTV(\Abs) &\defas& \emptyset\\ + % \FTV(\theta) &\defas& \{\theta\} +\end{eqs} & & +\begin{eqs} + \FTV([R]) &\defas& \FTV(R)\\ + \FTV(\Record{R}) &\defas& \FTV(R)\\ + \FTV(\{R\}) &\defas& \FTV(R)\\ + \FTV(l:P;R) &\defas& \FTV(P) \cup \FTV(R)\\ +\end{eqs}\\\\ +\begin{eqs} + \FTV(\theta) &\defas& \{\theta\}\\ + \FTV(\Abs) &\defas& \emptyset\\ + \FTV(\Pre{A}) &\defas& \FTV(A) +\end{eqs} & & +\begin{eqs} + \FTV(\cdot) &\defas& \emptyset\\ + \FTV(\Gamma,x : A) &\defas& \FTV(\Gamma) \cup \FTV(A) +\end{eqs} +\ea +\] +% +Thus the rule states that a type abstraction $(\Lambda \alpha. M)$ has +type $\forall \alpha.C$ if the computation $M$ has type $C$ assuming +$\alpha : K$ and $\alpha$ does not appear in the free type variables +of current type environment $\Gamma$. The \tylab{Unit} rule provides +the basis for all records as it simply states that the empty record +has type unit. The \tylab{Extend} rule handles record +extension. Supposing we wish to extend some record $\Record{W}$ with +$\ell = V$, that is $\Record{\ell = V; W}$. This extension has type +$\Record{\ell : \Pre{A};R}$ if and only if $V$ is well-typed and we +can ascribe $W : \Record{\ell : \Abs; R}$. In other words, the label +$\ell$ must not be mentioned in $W$. The \tylab{Inject} rule states +that $(\ell~V)^R$ has type $[\ell : \Pre{A}; R]$ if the payload $V$ is +well-typed. \section{Dynamic semantics} @@ -469,6 +690,8 @@ static semantics. \subsection{Effect inference} \subsection{Dynamic semantics} +\section{Default handlers} + \section{Parameterised handlers} \section{Shallow handlers}