Commit 9ed19474 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

introduce type shcemes in the proofs (in progress)

parent 73e043ca
......@@ -874,7 +874,86 @@
Immediate consequence of the previous results.
\end{proof}
\subsection{Full algorithmic type system}
\subsection{New algorithmic type system with type schemes}
TODO: Why do we introduce type schemes?
\subsubsection{Type schemes}
We introduce the new syntactic category of \emph{types schemes} which are the terms~$\ts$ inductively produced by the following grammar.
\[
\begin{array}{lrcl}
\textbf{Type schemes} & \ts & ::= & t \alt \tsfun {\arrow t t ; \cdots ; \arrow t t} \alt \ts \tstimes \ts \alt \ts \tsor \ts \alt \tsempty
\end{array}
\]
Type schemes denote sets of types, as formally stated by the following definition:
\begin{definition}[Interpretation of type schemes]
We define the function $\tsint {\_}$ that maps type schemes into sets of types.\vspace{-2.5mm}
\begin{align*}
\begin{array}{lcl}
\tsint t &=& \{s\alt t \leq s\}\\
\tsint {\tsfunone {t_i} {s_i}_{i=1..n}} &=& \{s\alt
\exists s_0 = \bigwedge_{i=1..n} \arrow {t_i} {s_i}
\land \bigwedge_{j=1..m} \neg (\arrow {t_j'} {s_j'}).\
\Empty \not\simeq s_0 \leq s \}\\
\tsint {\ts_1 \tstimes \ts_2} &=& \{s\alt \exists t_1 \in \tsint {\ts_1}\
\exists t_2 \in \tsint {\ts_2}.\ \pair {t_1} {t_2} \leq s\}\\
\tsint {\ts_1 \tsor \ts_2} &=& \{s\alt \exists t_1 \in \tsint {\ts_1}\
\exists t_2 \in \tsint {\ts_2}.\ {t_1} \vee {t_2} \leq s\}\\
\tsint \tsempty &=& \varnothing
\end{array}
\end{align*}
\end{definition}
Note that $\tsint \ts$ is closed under subsumption and intersection
and that $\tsempty$, which denotes the
empty set of types is different from $\Empty$ whose interpretation is
the set of all types.
\begin{lemma}[\cite{Frisch2008}]
Let $\ts$ be a type scheme and $t$ a type. It is possible to decide the assertion $t \in \tsint \ts$,
which we also write $\ts \leq t$.
\end{lemma}
We can now formally define the relation $v\in t$ used in
Section~\ref{sec:opsem} to define the dynamic semantics of
the language. First, we associate each (possibly, not well-typed)
value to a type scheme representing the best type information about
the value. By induction on the definition of values: $\tyof c {} =
\basic c$, $\tyof {\lambda^{\wedge_{i\in I}s_i\to t_i} x.e}{}=
\tsfun{s_i\to t_i}_{i\in I}$, $\tyof {(v_1,v_2)}{} = \tyof
{v_1}{}\tstimes\tyof {v_1}{}$. Then we have $v\in t\iffdef \tyof
v{}\leq t$.
We also need to perform intersections of type schemes so as to intersect the static type of an expression (i.e., the one deduced by conventional rules) with the one deduced by occurrence typing (i.e., the one derived by $\vdashp$). For our algorithmic system (see \Rule{Env$_{\scriptscriptstyle\mathcal{A}}$} in Section~\ref{sec:algorules}) all we need to define is the intersection of a type scheme with a type:
\begin{lemma}[\cite{Frisch2008}]
Let $\ts$ be a type scheme and $t$ a type. We can compute a type scheme, written $t \tsand \ts$, such that
\(\tsint {t \tsand \ts} = \{s \alt \exists t' \in \tsint \ts.\ t \land t' \leq s \}\)
\end{lemma}
Finally, given a type scheme $\ts$ it is straightforward to choose in its interpretation a type $\tsrep\ts$ which serves as the canonical representative of the set (i.e., $\tsrep \ts \in \tsint \ts$):
\begin{definition}[Representative]
We define a function $\tsrep {\_}$ that maps every non-empty type scheme into a type, \textit{representative} of the set of types denoted by the scheme.\vspace{-2mm}
\begin{align*}
\begin{array}{lcllcl}
\tsrep t &=& t & \tsrep {\ts_1 \tstimes \ts_2} &=& \pair {\tsrep {\ts_1}} {\tsrep {\ts_2}}\\
\tsrep {\tsfunone {t_i} {s_i}_{i\in I}} &=& \bigwedge_{i\in I} \arrow {t_i} {s_i} \qquad& \tsrep {\ts_1 \tsor \ts_2} &=& \tsrep {\ts_1} \vee \tsrep {\ts_2}\\
\tsrep \tsempty && \textit{undefined}
\end{array}\vspace{-4mm}
\end{align*}
\end{definition}
Type schemes are already present in the theory of semantic subtyping presented in~\cite[Section
6.11]{Frisch2008}. In particular, it explains how the operators such as $\circ$, $\bpl t$ and $\bpr t$
can be extended to type schemes (see also~\citep[\S4.4]{Cas15} for a detailed description).
\subsection{Full algorithmic type system with type schemes}
We present here a refinement of the algorithmic type system presented in \ref{sec:algorules}
that associates to an expression a type scheme instead of a regular type.
This allows to type expressions more precisely and thus to have a more powerful completeness theorem in regards to the
declarative type system.
The results about this new type system will be used in section TODO in order to obtain a soundness and completeness
theorem for the algorithmic type system presented in \ref{sec:algorules}.
\begin{mathpar}
\Infer[Efq\Aa]
......@@ -967,9 +1046,9 @@
\subsection{Proofs for the algorithmic type system}
This section is about the algorithmic type system (soundness and some completeness properties).
This section is about the algorithmic type system with type schemes (soundness and some completeness properties).
Note that we use a different but more convenient definition for $\tyof e \Gamma$ that the one
Note that, now that we have type schemes, use a different but more convenient definition for $\tyof e \Gamma$ that the one
in Section~\ref{sec:typenv}:
\begin{align*}
\tyof e \Gamma =
......@@ -1165,15 +1244,6 @@
Let $\ts_1$ and $\ts_2$ two type schemes. We write $\ts_2 \leq \ts_1$ iff $\tsint {\ts_1} \subseteq \tsint{\ts_2}$.
\end{definition}
\begin{definition}[Positive derivation]
A derivation of the declarative type system is said positive iff it does not contain any rule \Rule{Abs-}.
\end{definition}
\begin{definition}[Rank-0 negated derivation]
A derivation of the declarative type system is said rank-0 negated iff any application of \Rule{PAppL}
has a positive derivation as first premise ($\pvdash \Gamma e t \varpi.1:t_1$).
\end{definition}
\begin{lemma}
\begin{align*}
&\forall t,\ts.\ \tsrep{t\tsand\ts} \leq t \land \tsrep{\ts}\\
......@@ -1332,6 +1402,10 @@
The rest follows.
\end{proof}
\begin{definition}[Positive derivation]
A derivation of the declarative type system is said positive iff it does not contain any rule \Rule{Abs-}.
\end{definition}
\begin{theorem}[Completeness for positive derivations]
For every $\Gamma$, $e$, $t$ such that we have a positive derivation of $\Gamma \vdash e:t$,
......@@ -1489,32 +1563,23 @@
\textbf{Positive expression} & e_+ & ::= & c\alt x\alt e_+ e_+\alt\lambda^{t^\lambda_+} x.e_+\alt \pi_j e_+\alt(e_+,e_+)\alt\tcase{e_+}{t_{s}}{e_+}{e_+}
\end{array}
\]
\begin{corollary}\label{app:completeness}
If we restrict the language to positive expressions $e_+$, the algorithmic type system is complete and type schemes can be removed from it (we can use regular types instead).
More precisely:
$\forall \Gamma, e_+, t.\ \Gamma \vdash e_+:t \Rightarrow \tyof {e_+} \Gamma \neq \tsempty$
\end{corollary}
\begin{proof}
With such restrictions, the rule \Rule{Abs-} is not needed anymore
because the negative part of functional types (i.e. the $N_i$ part of their DNF) is useless.
Indeed, when typing an application $e_1 e_2$, the negative part of the type of $e_1$
is ignored by the operator $\apply {} {}$.
Moreover, as there is no negated arrows in the domain of lambda-abstractions,
the negative arrows of the type of $e_2$ can also be ignored.
Similarly, negative arrows can be ignored when refining an application ($\worra {} {}$ also ignore the negative part
of the type of $e_1$).
Finally, as the only functional type that we can test is $\arrow \Empty \Any$, a functional type
cannot be refined to $\Empty$ due to its negative part, and thus we can ignore its negative part
(it makes no difference relatively to the rule \Rule{Efq}).
\end{proof}
From this result, we will now prove a stronger but more complex completeness theorem.
We were not able to prove full completeness, just a partial form of it. Indeed,
the use of nested \Rule{PAppL} yields a precision that the algorithm loses by applying \tsrep{}
in the definition of \constrf{}. Completeness is recovered by forbidding nested negated arrows on the
left-hand side of negated arrows.
\begin{definition}[Rank-0 negated derivation]
A derivation of the declarative type system is said rank-0 negated iff any application of \Rule{PAppL}
has a positive derivation as first premise ($\pvdash \Gamma e t \varpi.1:t_1$).
\end{definition}
\noindent The use of this terminology is borrowed from the ranking of higher-order
types, since, intuitively, it corresponds to typing a language in
which in the types used in dynamic tests, a negated arrow never occurs on the
left-hand side of another negated arrow.
\begin{lemma}
If $e$ is an application, then $\tyof e \Gamma$ does not contain any constructor $\tsfun \cdots$.
Consequently, we have $\tsrep{\tyof e \Gamma} \simeq \tyof e \Gamma$.
......@@ -1634,3 +1699,32 @@
\end{description}
\end{description}
\end{proof}
\subsection{The algorithmic type system without type schemes}
TODO: states the inclusion between the regular type system and the one with type schemes
\begin{corollary}\label{app:completeness}
If we restrict the language to positive expressions $e_+$, the algorithmic type system is complete and type schemes can be removed from it (we can use regular types instead).
More precisely:
$\forall \Gamma, e_+, t.\ \Gamma \vdash e_+:t \Rightarrow \tyof {e_+} \Gamma \neq \tsempty$
\end{corollary}
\begin{proof}
With such restrictions, the rule \Rule{Abs-} is not needed anymore
because the negative part of functional types (i.e. the $N_i$ part of their DNF) is useless.
Indeed, when typing an application $e_1 e_2$, the negative part of the type of $e_1$
is ignored by the operator $\apply {} {}$.
Moreover, as there is no negated arrows in the domain of lambda-abstractions,
the negative arrows of the type of $e_2$ can also be ignored.
Similarly, negative arrows can be ignored when refining an application ($\worra {} {}$ also ignore the negative part
of the type of $e_1$).
Finally, as the only functional type that we can test is $\arrow \Empty \Any$, a functional type
cannot be refined to $\Empty$ due to its negative part, and thus we can ignore its negative part
(it makes no difference relatively to the rule \Rule{Efq}).
\end{proof}
......@@ -5,6 +5,7 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Packages
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\let\Bbbk\relax
\usepackage{amsmath}
\usepackage{mathtools}
\usepackage{amssymb}
......
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