Commit 42b60d34 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

typos

parent 36b670ed
......@@ -45,7 +45,7 @@ denoted by the type) or $t = \neg t$ (which cannot represent any
set).
\iflongversion%%%%%%%%%%%%%%%%%%
It also ensures that the binary relation $\vartriangleright
\,\subseteq\!\types^{2}$ defined by $t_1 \lor t_2 \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.
This gives an induction principle on $\types$ that we
......@@ -57,9 +57,10 @@ 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 (see~\cite{types18post} for a simpler alternative
definition (see~\citet{types18post} for a simpler alternative
definition that we recall in Appendix~\ref{sec:subtyping} for the
reader's convenience). A detailed description of the algorithm to decide it can be found in~\cite{Cas15}.
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
types are interpreted as sets of \emph{values} ({i.e., either
constants, $\lambda$-abstractions, or pairs of values: see
......@@ -231,7 +232,7 @@ type $(\Int\to t)\wedge\neg(\Int\to\neg\Bool)$, that is,
$(\Int\to t)\setminus(\Int\to\neg\Bool)$ ). But the sole rule \Rule{Abs+}
above does not allow us to deduce negations of
arrows for abstractions: the rule \Rule{Abs-} makes this possible. As an aside, note that this kind
of deduction was already present in the system by~\citet{Frisch2008}
of deduction is already present in the system by~\citet{Frisch2008}
though in that system this presence was motivated by the semantics of types rather than, as in our case,
by the soundness of the type system.
......@@ -270,12 +271,7 @@ expression whose type environment contains an empty assumption:
\end{mathpar}
Once more, this kind of deduction was already present in the system
by~\citet{Frisch2008} to type full fledged overloaded functions,
though it was embedded in the typing rule for the type-case.%
%\ifsubmission%
%~\pagebreak
%\else
%
%\fi%
though it was embedded in the typing rule for the type-case.
Here we
need the rule \Rule{Efq}, which is more general, to ensure the
property of subject reduction.
......@@ -455,7 +451,8 @@ rules that essentially state that if $\pi_1 e$ (respectively, $\pi_2
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 our type system, which satisfies
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
the property of safety, deduced, as customary, from the properties
of progress and subject reduction (\emph{cf.} Appendix~\ref{app:soundness}).\vspace{-.5mm}
\begin{theorem}[type safety]
......
......@@ -303,22 +303,28 @@ The authors thank Paul-André Melliès for his help on type ranking.
\label{sec:subtyping}
\input{subtyping}
\newpage
\section{Proof of Type Soundness}
\label{sec:proofs}
\input{proofs}
\newpage
\section{Typing Algorithm: Operators, Type Schemes, Proofs of Soundness and Completeness}
\label{sec:proofs-algo}
\input{proofs-algo}
\newpage
\section{Record types operators}\label{app:recop}
\input{record_operations}
\newpage
\section{A more precise rule for inference}\label{app:optimize}
\input{optimize}
\newpage
\section{A Roadmap to Polymorphic Types}
\label{app:roadmap}
......
......@@ -5,7 +5,7 @@ well as the proof of its type safety.
\newtheorem{property}{Property}
\subsection{The declarative type system}
\subsection{The declarative type system}\label{sec:declarative}
\begin{mathpar}
\Infer[Env]
......
......@@ -41,7 +41,8 @@ so that it satisfies the following equalities,
where $ \Pf $ denotes the restriction of the powerset to finite
subsets and $ \ConstantsInBasicType{()}$ denotes the function
that assigns to each basic type the set of constants of that type, so
that $ c\in \ConstantsInBasicType(\basic {c})$:
that for every constant $c$ we have $ c\in \ConstantsInBasicType(\basic {c})$ ($\basic c$ is
Defined in Section~\ref{sec:syntax}):
\begin{align*}
\TypeInter{\Empty} & = \emptyset&
\TypeInter{t_1 \lor t_2} & = \TypeInter{t_1} \cup \TypeInter{t_2} &
......@@ -57,17 +58,26 @@ that assigns to each basic type the set of constants of that type, so
We cannot take the equations above
directly as an inductive definition of $ \TypeInter{} $
because types are not defined inductively but coinductively.
\iflongversion%%%%%%%%%%%%%%%%%%%
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}),
which validates these equalities.
\else
Notice however that the contractivity condition of
Definition~\ref{def:types} ensures that the binary relation $\vartriangleright
\,\subseteq\!\types^{2}$ defined by $t_1 \lor t_2 \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.
This gives an induction principle \footnote{In a nutshell, we can do
This gives an induction principle\footnote{In a nutshell, we can do
proofs and give definitions by induction on the structure of unions and negations---and, thus, intersections---but arrows, products, and basic types are the base cases for the induction.} 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}),
which validates these equalities.
\fi%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{definition}[Set-theoretic interpretation of types~\cite{types18post}]\label{def:interpretation-of-types}
We define a binary predicate $ (d : t) $
(``the element $ d $ belongs to the type $t$''),
......
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