dhil/phd-dissertation
1
0
Fork 0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-13 02:58:26 +00:00
Code Issues Releases Wiki Activity

Revisions, parametricity.

Browse Source
This commit is contained in:
Daniel Hillerström
2020-03-25 16:19:44 +00:00
parent 753996ae9f
commit a37812aad5
3 changed files with 202 additions and 102 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
macros.tex
View File

@@ -63,6 +63,8 @@
\newcommand{\Put}{\dec{Put}} \newcommand{\Put}{\dec{Put}}
\newcommand{\Zero}{\dec{Zero}} \newcommand{\Zero}{\dec{Zero}}
\newcommand{\Fail}{\dec{Fail}} \newcommand{\Fail}{\dec{Fail}}
\newcommand{\Read}{\dec{Read}}
\newcommand{\Write}{\dec{Write}}
\newcommand{\True}{\mathsf{true}} \newcommand{\True}{\mathsf{true}}
\newcommand{\False}{\mathsf{false}} \newcommand{\False}{\mathsf{false}}

32
thesis.bib
View File

@@ -812,4 +812,34 @@
number = {2}, number = {2},
pages = {125--143}, pages = {125--143},
year = {1998} year = {1998}
} }
% System F
@phdthesis{Girard72,
author = {J. Y. Girard},
school = {Universit{\'e} Paris 7},
title = {Interpr{\'e}tation fonctionnelle et {\'e}limination des coupures de l'arithm{\'e}tique d'ordre sup{\'e}rieur},
type = {PhD thesis},
year = 1972
}
@inproceedings{Reynolds74,
author = {John C. Reynolds},
title = {Towards a theory of type structure},
booktitle = {Symposium on Programming},
series = {Lecture Notes in Computer Science},
volume = {19},
pages = {408--423},
publisher = {Springer},
year = {1974}
}
@inproceedings{Wadler89,
author = {Philip Wadler},
title = {Theorems for Free!},
booktitle = {{FPCA}},
pages = {347--359},
publisher = {{ACM}},
year = {1989}
}

270
thesis.tex
View File

@@ -312,8 +312,9 @@ Section~\ref{sec:base-language-type-rules}.
\label{fig:base-language-types} \label{fig:base-language-types}
\end{figure} \end{figure}
% %
Figure~\ref{fig:base-language-types} depicts the syntax for types, The types are divided into several distinct syntactic categories which
kinds, and their environments. are given in Figure~\ref{fig:base-language-types} along with the
syntax of kinds and environments.
% %
\paragraph{Value types} \paragraph{Value types}
We distinguish between values and computations at the level of We distinguish between values and computations at the level of
@@ -338,46 +339,69 @@ presence type. A presence type indicates whether a label is
\emph{present} with type $A$ ($\Pre{A}$), \emph{absent} ($\Abs$) or \emph{present} with type $A$ ($\Pre{A}$), \emph{absent} ($\Abs$) or
\emph{polymorphic} in its presence ($\theta$). \emph{polymorphic} in its presence ($\theta$).
% %
For example, the effect row $\{\Read:\Pre{\Int},\Write:\Abs,\cdot\}$
denotes a read-only context in which the operation label $\Read$ may
occur to access some integer value, whilst the operation label
$\Write$ cannot appear.
%
Row types are either \emph{closed} or \emph{open}. A closed row type 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 ends in~$\cdot$, whilst an open row type ends with a \emph{row
variable} $\rho$ (in an effect row we usually use $\varepsilon$ variable} $\rho$ (in an effect row we usually use $\varepsilon$
rather than $\rho$ and refer to it as an \emph{effect variable}). rather than $\rho$ and refer to it as an \emph{effect variable}).
% %
The row variable in an open row type can be instantiated with The example effect row above is closed, an open variation of it ends
additional labels. Each label may occur at most once in each row (we in an effect variable $\varepsilon$,
enforce this restriction at the level of kinds). We identify rows up i.e. $\{\Read:\Pre{\Int},\Write:\Abs,\varepsilon\}$.
to the reordering of labels. We assume structural equality on labels.
% %
% \begin{mathpar} The row variable in an open row type can be instantiated with
% \inferrule*[Lab=\rowlab{Closed}] additional labels subject to the restriction that each label may only
% {~} occur at most once (we enforce this restriction at the level of
% {\cdot \equiv_{\mathrm{row}} \cdot} kinds). We identify rows up to the reordering of labels as follows.
%
\begin{mathpar}
\inferrule*[Lab=\rowlab{Closed}]
{~}
{\cdot \equiv_{\mathrm{row}} \cdot}
% \inferrule*[Lab=\rowlab{Open}] \inferrule*[Lab=\rowlab{Open}]
% {~} {~}
% {\rho \equiv_{\mathrm{row}} \rho} {\rho \equiv_{\mathrm{row}} \rho'}
% \inferrule*[Lab=\rowlab{Head}] \inferrule*[Lab=\rowlab{Head}]
% {R \equiv_{\mathrm{row}} R'} {R \equiv_{\mathrm{row}} R'}
% {\ell:P;R \equiv_{\mathrm{row}} \ell:P;R'} {\ell:P;R \equiv_{\mathrm{row}} \ell:P;R'}
% \inferrule*[Lab=\rowlab{Swap}] \inferrule*[Lab=\rowlab{Swap}]
% {R \equiv_{\mathrm{row}} R'} {R \equiv_{\mathrm{row}} R'}
% {\ell:P;\ell':P';R \equiv_{\mathrm{row}} \ell':P';\ell:P;R'} {\ell:P;\ell':P';R \equiv_{\mathrm{row}} \ell':P';\ell:P;R'}
% \end{mathpar} \end{mathpar}
% % %
% The last rule $\rowlab{Swap}$ let us identify rows up to the % The last rule $\rowlab{Swap}$ let us identify rows up to the
% reordering of labels. For instance, the two rows % reordering of labels. For instance, the two rows
% $\ell_1 : P_1; \cdots; \ell_n : P_n; \cdot$ and % $\ell_1 : P_1; \cdots; \ell_n : P_n; \cdot$ and
% $\ell_n : P_n; \cdots ; \ell_1 : P_1; \cdot$ are equivalent. % $\ell_n : P_n; \cdots ; \ell_1 : P_1; \cdot$ are equivalent.
% %
Absent labels in closed rows are redundant. The \rowlab{Closed} rule states that the closed marker $\cdot$ is
equivalent to itself, similarly the \rowlab{Open} rule states that any
two row variables are equivalent if and only if they have the same
syntactic name. The \rowlab{Head} rule compares the head of two given
rows and inductively compares their tails. The \rowlab{Swap} rule
permits reordering of labels. We assume structural equality on
labels. The \rowlab{Head} rule
% %
The standard zero and unit types are definable using rows. We define The standard zero and unit types are definable using rows. We define
the zero type as the empty, closed variant $\ZeroType \defas the zero type as the empty, closed variant $\ZeroType \defas
[\cdot]$. Dually, the unit type is defined as the empty, closed record [\cdot]$. Dually, the unit type is defined as the empty, closed record
type, i.e. $\UnitType \defas \Record{\cdot}$. We shall often omit type, i.e. $\UnitType \defas \Record{\cdot}$.
$\cdot$ for closed rows.
% As absent labels in closed rows are redundant we will, for example,
% consider the following two rows equivalent
% $\Read:\Pre{\Int},\Write:\Abs,\cdot \equiv_{\mathrm{row}}
% \Read:\Pre{\Int},\cdot$.
For brevity, we shall often write $\ell : A$
to mean $\ell : \Pre{A}$ and omit $\cdot$ for closed rows.
% %
\begin{figure} \begin{figure}
@@ -450,10 +474,9 @@ $\cdot$ for closed rows.
\paragraph{Kinds} \paragraph{Kinds}
The kinds classify the different categories of types. The $\Type$ kind The kinds classify the different categories of types. The $\Type$ kind
classifies for value types, $\Presence$ classifies presence classifies value types, $\Presence$ classifies presence annotations,
annotations, $\Comp$ classifies computation types, $\Effect$ $\Comp$ classifies computation types, $\Effect$ classifies effect
classifies effect types, and lastly $\Row_{\mathcal{L}}$ classifies types, and lastly $\Row_{\mathcal{L}}$ classifies rows.
rows.
% %
The formation rules for kinds are given in The formation rules for kinds are given in
Figure~\ref{fig:base-language-kinding}. The kinding judgement Figure~\ref{fig:base-language-kinding}. The kinding judgement
@@ -472,7 +495,7 @@ Kind and type environments are right-extended sequences of bindings. A
kind environment binds type variables to their kinds, whilst a type kind environment binds type variables to their kinds, whilst a type
environment binds term variables to their types. environment binds term variables to their types.
\paragraph{Type variable} The type structure has three syntactically \paragraph{Type variables} The type structure has three syntactically
distinct type variables (the kinding system gives us five semantically distinct type variables (the kinding system gives us five semantically
distinct notions of type variables). As we sometimes wish to refer distinct notions of type variables). As we sometimes wish to refer
collectively to type variables, we define the set of type variables, collectively to type variables, we define the set of type variables,
@@ -512,6 +535,122 @@ $\TyVarCat$, to be generated by:
% to ensure uniqueness amongst labels in each row type. We shall % to ensure uniqueness amongst labels in each row type. We shall
% elaborate on this in Section~\ref{sec:row-polymorphism}. % elaborate on this in Section~\ref{sec:row-polymorphism}.
\paragraph{Free type variables} Sometimes we need to compute the free
type variables ($\FTV$) of a given type. To this end we define a
metafunction $\FTV$ by induction on the type structure, $T$, and
point-wise on type environments, $\Gamma$. Note that we always work up
to $\alpha$-conversion~\cite{Church32} of types.
%
\[
\ba[t]{@{~}l@{~~~~~~}c@{~}l}
\multicolumn{3}{c}{\begin{eqs}
\FTV &:& \TypeCat \to \TyVarCat
\end{eqs}}\\
\ba[t]{@{}l}
\begin{eqs}
% \FTV &:& \ValTypeCat \to \TyVarCat\\
\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}\ea & &
\begin{eqs}
% \FTV([R]) &\defas& \FTV(R)\\
% \FTV(\Record{R}) &\defas& \FTV(R)\\
% \FTV(\{R\}) &\defas& \FTV(R)\\
% \FTV &:& \RowCat \to \TyVarCat\\
\FTV(\cdot) &\defas& \emptyset\\
\FTV(\rho) &\defas& \{\rho\}\\
\FTV(l:P;R) &\defas& \FTV(P) \cup \FTV(R)\\
% \FTV &:& \PresenceCat \to \TyVarCat\\
\FTV(\theta) &\defas& \{\theta\}\\
\FTV(\Abs) &\defas& \emptyset\\
\FTV(\Pre{A}) &\defas& \FTV(A)\\
\end{eqs}\\\\
\multicolumn{3}{c}{\begin{eqs}
\FTV &:& \TyEnvCat \to \TyVarCat\\
\FTV(\cdot) &\defas& \emptyset\\
\FTV(\Gamma,x : A) &\defas& \FTV(\Gamma) \cup \FTV(A)
\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
\]
%
We now have the basic vocabulary to construct types in $\BCalc$. For
example, we can give the signature of the standard polymorphic
identity function:
%
\[
\forall \alpha^\Type. \alpha \to \alpha \eff \emptyset.
\]
%
Modulo the empty effect signature, this type is akin to the type one
would give for the identity function in System
F~\cite{Girard72,Reynolds74}, and thus we can use standard techniques
from parametricity~\cite{Wadler89} to reason about inhabitants of this
signature. However, in our system we can give an even more general
type to the identity function:
%
\[
\forall \alpha^\Type,\varepsilon^{\Row_\emptyset}. \alpha \to \alpha \eff \{\varepsilon\}.
\]
%
This type is polymorphic in its effect signature as signified by the
singleton open effect row $\{\varepsilon\}$, meaning it may be used in
an effectful context. By contrast, the former type may only be used in
a strictly pure context, i.e. the effect-free context.
%
\dhil{Maybe say something about reasoning effect types}
%
We can use the effect system to give precise types to effectful
computations. For instance, we can give the signature of some
polymorphic computation that may read from and write to some integer
store:
%
\[
\forall \alpha^\Type, \varepsilon^{\{\Read,\Write\}}. \alpha \eff \{\Read:\Int,\Write:\Int \to \UnitType \eff \emptyset,\varepsilon\}.
\]
%
The effect row comprise a nullary $\Read$ operation returning some
integer and a unary $\Write$ carrying an integer and returning
unit. Since the effect row ends in an effect variable, an inhabitant
of this type may be used in a larger effect context.
%
We can also be precise about how a higher-order function may use its
function arguments. The $\dec{map}$ function for lists is a canonical
example of a higher-order function which is parametric in its own
effects and the effects of its function argument. Supposing $\BCalc$
have some polymorphic list datatype $\List$, then we would be able to
ascribe the following signature to $\dec{map}$
%
\[
\forall \alpha^\Type,\beta^\Type,\varepsilon^{\Row_\emptyset}. \Record{\alpha \to \beta \eff \{\varepsilon\},\List~\alpha} \to \List~\beta \eff \{\varepsilon\}.
\]
%
Note that the two effect rows are identical and share the same effect
variable $\varepsilon$, it is thus evident that an inhabitant of this
type can only perform whatever effects its first argument is allowed
to perform.
\subsection{Terms} \subsection{Terms}
\label{sec:base-language-terms} \label{sec:base-language-terms}
% %
@@ -536,8 +675,7 @@ $\TyVarCat$, to be generated by:
The syntax for terms is given in The syntax for terms is given in
Figure~\ref{fig:base-language-term-syntax}. We assume countably Figure~\ref{fig:base-language-term-syntax}. We assume countably
infinite set of names $\VarCat$ from which we draw fresh variable infinite set of names $\VarCat$ from which we draw fresh variable
names at will. We shall typically denote term variables by $x$, $y$, names. We shall typically denote term variables by $x$, $y$, or $z$.
or $z$.
% %
The syntax partitions terms into values and computations. The syntax partitions terms into values and computations.
% %
@@ -697,76 +835,6 @@ Computations
\label{fig:base-language-type-rules} \label{fig:base-language-type-rules}
\end{figure} \end{figure}
% %
\dhil{There is some rendering issue with T-labels in the typing rules.}
%
The typing rules are given by
Figure~\ref{fig:base-language-type-rules}. In each typing rule, we
implicitly assume that each type is well-kinded with respect to the
kinding environment $\Delta$.
\paragraph{Typing values} 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$) to ensure that we do not
inadvertently capture a free type variable from the context.
%
We define $\FTV$ by mutual induction over type environments, $\Gamma$,
and the type structure, $T$. Note that we always work up to
$\alpha$-conversion~\cite{Church32} of types.
%
\[
\ba[t]{@{~}l@{~~~~~~}c@{~}l}
\multicolumn{3}{c}{\begin{eqs}
\FTV &:& \TypeCat \to \TyVarCat
\end{eqs}}\\
\ba[t]{@{}l}
\begin{eqs}
% \FTV &:& \ValTypeCat \to \TyVarCat\\
\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}\ea & &
\begin{eqs}
% \FTV([R]) &\defas& \FTV(R)\\
% \FTV(\Record{R}) &\defas& \FTV(R)\\
% \FTV(\{R\}) &\defas& \FTV(R)\\
% \FTV &:& \RowCat \to \TyVarCat\\
\FTV(\cdot) &\defas& \emptyset\\
\FTV(\rho) &\defas& \{\rho\}\\
\FTV(l:P;R) &\defas& \FTV(P) \cup \FTV(R)\\
% \FTV &:& \PresenceCat \to \TyVarCat\\
\FTV(\theta) &\defas& \{\theta\}\\
\FTV(\Abs) &\defas& \emptyset\\
\FTV(\Pre{A}) &\defas& \FTV(A)\\
\end{eqs}\\\\
\multicolumn{3}{c}{\begin{eqs}
\FTV &:& \TyEnvCat \to \TyVarCat\\
\FTV(\cdot) &\defas& \emptyset\\
\FTV(\Gamma,x : A) &\defas& \FTV(\Gamma) \cup \FTV(A)
\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 Thus the rule states that a type abstraction $(\Lambda \alpha. M)$ has
type $\forall \alpha.C$ if the computation $M$ has type $C$ assuming type $\forall \alpha.C$ if the computation $M$ has type $C$ assuming
$\alpha : K$ and $\alpha$ does not appear in the free type variables $\alpha : K$ and $\alpha$ does not appear in the free type variables