Commit 6b4f63ef authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

moved subtyping definition

parent f55f9f27
......@@ -370,7 +370,7 @@ that the application $e(42)$ reduces to a Boolean value, then the whole
expression in \eqref{bistwo} reduces to $e$; but this has type
$\Int\to t$ which, in general, is \emph{not} a subtype of $(\Int\to
t)\setminus(\Int\to\neg\Bool)$, and therefore type is not preserved by the reduction. To cope with this problem, the proof
of type preservation (see Appendix~\ref{app:subject-reduction}) resorts to \emph{type schemes}, a
of type preservation (see \Appendix\ref{app:subject-reduction}) resorts to \emph{type schemes}, a
technique introduced by~\citet{Frisch2008} to type expressions by
sets of types, so that the expression in \eqref{bistwo} will have both the types at issue.
......@@ -383,7 +383,7 @@ eventually reduce to a \Bool). This problem will be handled in the
proof of type preservation by considering parallel reductions (e.g, if
$e(42)$ reduces in a step to, say, $\textsf{false}$, then
$\ifty{e(42)}{\Bool}{e(42)}{\textsf{true}}$ reduces in one step to
$\ifty{\textsf{false}}{\Bool}{\textsf{false}}{\textsf{true}}$): see Appendix~\ref{app:parallel}.
$\ifty{\textsf{false}}{\Bool}{\textsf{false}}{\textsf{true}}$): see \Appendix\ref{app:parallel}.
\paragraph{Interdependence of checks} The last class of technical problems arise
......@@ -448,8 +448,8 @@ A discussion of future work concludes this
presentation.
\fi
%
For space reasons several technical definitions and all the proofs are
omitted from this presentation and can be found in the appendix
To ease the presentation all the proofs are
omitted from the main text and can be found in the appendix
\ifsubmission
joint to the submission as supplemental material.
\else
......
......@@ -56,11 +56,24 @@ and to $ \lor $, $ \land $, $ \lnot $, and $ \setminus $
as \emph{type connectives}.
The subtyping relation for these types, noted $\leq$, is the one defined
by~\citet{Frisch2008} to which the reader may refer for the formal
definition (we recall it in Appendix~\ref{sec:subtyping} for the
reader's convenience). A detailed description of the algorithm to
by~\citet{Frisch2008}
%
\iflongversion
and detailed description of the algorithm to
decide this relation can be found in~\cite{Cas15}. For the reader's
convenince we succintly recall the definition of the subtyping relations in the next subsection.
This subsection can be skipped at first reading and the reader can
jump directly to Subsection~\ref{sec:syntax}, since to understand
what will follow
\else
to which the reader may refer for the formal
definition (we recall it in \Appendix\ref{sec:subtyping} for the
reader's convenience).
A detailed description of the algorithm to
decide this relation can be found in~\cite{Cas15}.
For this presentation it suffices to consider that
For this presentation
\fi
it suffices to consider that
types are interpreted as sets of \emph{values} ({i.e., either
constants, $\lambda$-abstractions, or pairs of values: see
Section~\ref{sec:syntax} right below) that have that type, and that subtyping is set
......@@ -78,6 +91,14 @@ corresponding set-theoretic operators (e.g.,~$s\vee t$ is the
union of the values of the two types). We use $\simeq$ to denote the
symmetric closure of $\leq$: thus $s\simeq t$ (read, $s$ is equivalent to $t$) means that $s$ and $t$ denote the same set of values and, as such, they are semantically the same type.
\iflongversion
The above is formalized as follows.
\subsection{Subtyping}
\label{sec:subtyping}
\input{subtyping}
\fi
\subsection{Syntax}\label{sec:syntax}
The expressions $e$ and values $v$ of our language are inductively generated by the following grammars:\svvspace{-1mm}
\begin{equation}\label{expressions}
......@@ -104,7 +125,7 @@ typed if $\lambda^{\wedge_{i\in I}s_i\to t_i} x.e$ has type $s_i\to
t_i$ for all $i\in I$. Every value is associated to a most specific type (mst): the mst of $c$ is $\basic c$; the mst of
$\lambda^{\wedge_{i\in I}s_i\to t_i} x.e$ is $\wedge_{i\in I}s_i\to t_i$; and, inductively,
the mst of a pair of values is the product of the mst's of the
values. We write $v\in t$ if the most specific type of $v$ is a subtype of $t$ (see Appendix~\ref{app:typeschemes} for the formal definition of $v\in t$ which deals with some corner cases for negated arrow types).
values. We write $v\in t$ if the most specific type of $v$ is a subtype of $t$ (see \Appendix\ref{app:typeschemes} for the formal definition of $v\in t$ which deals with some corner cases for negated arrow types).
......@@ -451,9 +472,9 @@ e$) is of type $t'$, then the type of $e$ must be of the form
$\pair{t'}\Any$ (respectively, $\pair\Any{t'}$).
This concludes the presentation of all the rules of our type system
(they are summarized for the reader's convenience in Appendix~\ref{sec:declarative}), which satisfies
(they are summarized for the reader's convenience in \Appendix\ref{sec:declarative}), which satisfies
the property of safety, deduced, as customary, from the properties
of progress and subject reduction (\emph{cf.} Appendix~\ref{app:soundness}).\svvspace{-.5mm}
of progress and subject reduction (\emph{cf.} \Appendix\ref{app:soundness}).\svvspace{-.5mm}
\begin{theorem}[type safety]
For every expression $e$ such that $\varnothing\vdash e:t$ either $e$
diverges or there
......
......@@ -37,6 +37,8 @@
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\newif\ifelsevierstyle
\elsevierstyletrue
\newif\ifwithcomments
\withcommentstrue
\withcommentsfalse
......@@ -44,9 +46,6 @@
\submissiontrue
\newif\iflongversion
\longversiontrue
\newcommand{\svvspace}[1]{
\iflongversion\else\vspace{#1}\fi
}
%\longversionfalse
\usepackage{setup}
......@@ -244,11 +243,12 @@ The authors thank Paul-André Melliès for his help on type ranking.
%% Appendix
\appendix
\iflongversion\else
\section{Definition of the Subtyping Relation}
\label{sec:subtyping}
\input{subtyping}
\newpage
\fi
\section{Proof of Type Soundness}
\label{sec:proofs}
......
......@@ -21,6 +21,9 @@
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\newif\ifelsevierstyle
\elsevierstylefalse
\newif\ifwithcomments
\withcommentstrue
\withcommentsfalse
......
......@@ -37,6 +37,17 @@
\newcommand{\victor}[1]{}
\fi
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Style dependend definitions
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\ifelsevierstyle
\newcommand{\Appendix}{}
\else
\newcommand{\Appendix}{Appendix }
\fi
\newcommand{\svvspace}[1]{
\iflongversion\else\vspace{#1}\fi
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Support macros
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......
\noindent
Subtyping is defined by giving a set-theoretic interpretation of the
types of Definition~\ref{def:types} into a suitable domain $\Domain$:
\begin{definition}[Interpretation domain~\cite{Frisch2008}]\label{def:interpretation}
......@@ -63,8 +64,8 @@ However, recall that the contractivity condition of
Definition~\ref{def:types} ensures that the binary relation $\vartriangleright
\,\subseteq\!\types{\times}\types$ defined by $t_1 \lor t_2 \vartriangleright
t_i$, $t_1 \land t_2 \vartriangleright t_i$, $\neg t \vartriangleright t$ is Noetherian which gives an induction principle on $\types$ that we
use combined with structural induction on $\Domain$ to give the following definition (due to~\citet{types18post}
and equivalent to but simpler than the definition in~\cite{Frisch2008}),
use combined with structural induction on $\Domain$ to give the
following definition
which validates these equalities.
\else
Notice however that the contractivity condition of
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment