Commit e4289328 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

finished elimination of type schemes from main text

parent 7f0d3a38
......@@ -211,9 +211,8 @@ not converge. As an example, consider the (dumb) expression $\tcase
$\Refinef$ yields for $x_1$ a type strictly more precise than the type deduced in the
previous iteration.
\beppe{REWRITE BELOW TILL THE END OF THE SUBSECTION TO STRESS SEMI-DECIDABILITY INSTEAD OF UNCOMPLETENESS}
The solution we adopt here is to bound the number of iterations to some number $n_o$.
From a formal point of view, this means to give up the completeness of the algorithm: $\Refinef$ will be complete (i.e., it will find all solutions) for the deductions of $\Gamma \evdash e t \Gamma'$ of depth at most $n_o$. This is obtained by the following definition of $\Refinef$\vspace{-1mm}
The solution we adopt in practice is to bound the number of iterations to some number $n_o$. This is obtained by the following definition of $\Refinef$\vspace{-1mm}
\[
\begin{array}{rcl}
\Refinef_{e,t} \eqdef (\RefineStep{e,t})^{n_o}\\[-2mm]
......@@ -234,21 +233,6 @@ bound our search to $n_o$ iterations. Since $\RefineStep {e,t}$ is
monotone (w.r.t.\ the subtyping pre-order extended to type environments pointwise), then
every iteration yields a better solution.
While this is unsatisfactory from a formal point of view, in practice
the problem is a very mild one. Divergence may happen only when
refining the type of a function in an application: not only such a
refinement is meaningful only when the function is typed by a union
type (which is quite rare in practice)\footnote{\label{foo:typecase}The only impact of
adding a negated arrow type to the type of a function is when we
test whether the function has a given arrow type: in practice this
never happens since programming languages test whether a value
\emph{is} a function, rather than the type of a given function.},
but also we had to build the expression that causes the divergence in
quite an \emph{ad hoc} way which makes divergence even more unlikely.
%: setting
%an $n_o$ twice the depth of the syntax tree of the outermost type case
%should be enough to capture all realistic cases \beppe{can we give an estimate
% based on benchmarking the prototype?}
......@@ -325,46 +309,102 @@ We now have all the notions we need for our typing algorithm, which is defined b
The side conditions of the rules ensure that the system is syntax
directed, that is, that at most one rule applies when typing a term:
priority is given to \Rule{Eqf\Aa} over all the other rules and to
\Rule{Env\Aa} over all remaining logical rules.
\beppe{Modifies till here} Type schemes are
used to account for the type-multiplicity stemming from
$\lambda$-abstractions as shown in particular by rule \Rule{Abs\Aa}
(in what follows we use the word ``type'' also for type schemes). The
subsumption rule is no longer in the system; it is replaced by: $(i)$
using a union type in \Rule{Case\Aa}, $(ii)$ checking in \Rule{Abs\Aa}
that the body of the function is typed by a subtype of the type
declared in the annotation, and $(iii)$ using type operators and
checking subtyping in the elimination rules \Rule{App\Aa,Proj\Aa}. In
particular, for \Rule{App\Aa} notice that it checks that the type of
the function is a functional type, that the type of the argument is a
subtype of the domain of the function, and then returns the result
type of the application of the two types. The intersection rule is
replaced by the use of type schemes in \Rule{Abs\Aa} and by the rule
\Rule{Env\Aa}. The latter intersects the type deduced for an
expression $e$ by occurrence typing and stored in $\Gamma$ with the
type deduced for $e$ by the logical rules: this is simply obtained by
removing any hypothesis about $e$ from $\Gamma$, so that the deduction
of the type $t$ for $e$ cannot but end by a logical rule. Of course
this does not apply when the expression $e$ is a variable, since
an hypothesis in $\Gamma$ is the only way to deduce the type of a
variable, which is why the algorithm reintroduces the classic rule
for variables.
\Rule{Env\Aa} over all remaining logical rules. The subsumption rule
is no longer in the system; it is replaced by: $(i)$ using a union
type in \Rule{Case\Aa}, $(ii)$ checking in \Rule{Abs\Aa} that the body
of the function is typed by a subtype of the type declared in the
annotation, and $(iii)$ using type operators and checking subtyping in
the elimination rules \Rule{App\Aa,Proj\Aa}. In particular, for
\Rule{App\Aa} notice that it checks that the type of the function is a
functional type, that the type of the argument is a subtype of the
domain of the function, and then returns the result type of the
application of the two types. The intersection rule is (partially)
replaced by the rule \Rule{Env\Aa} which intersects the type deduced
for an expression $e$ by occurrence typing and stored in $\Gamma$ with
the type deduced for $e$ by the logical rules: this is simply obtained
by removing any hypothesis about $e$ from $\Gamma$, so that the
deduction of the type $t$ for $e$ cannot but end by a logical rule. Of
course this does not apply when the expression $e$ is a variable,
since an hypothesis in $\Gamma$ is the only way to deduce the type of
a variable, which is why the algorithm reintroduces the classic rule
for variables. Finally notice that there is no counterpart for the
rule \Rule{Abs-} and that therefore it is not possible to deduce
negated arrow types for functions. This means that the algorithmic
system is not complete as we discuss in details in the next section.
\subsubsection{Properties of the algorithmic system}\label{sec:algoprop}
The algorithmic system above is sound with respect to the deductive one of Section~\ref{sec:static}
\begin{theorem}[Soundness]
For every $\Gamma$, $e$, $t$, $n_o$, if $\Gamma\vdashA e: t$, then $\Gamma \vdash e:t$ for every $t\int$.
\begin{theorem}[Soundness]\label{th:algosound}
For every $\Gamma$, $e$, $t$, $n_o$, if $\Gamma\vdashA e: t$, then $\Gamma \vdash e:t$.
\end{theorem}
The proof of this theorem (see Appendix~\ref{}) is obtained by
defining an algorithmic system $\vdashAts$ that uses type schemes,
that is, which associates each typable term $e$ with a possibly
infinite set of types $\ts$ (in particular a $\lambda$-expression
$\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e$ will
be associated to a set of types of the form $\{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 \}$) and proving that, if
$\Gamma\vdashA e: t$ then $\Gamma\vdashAts e: \ts$ with
$t\in\ts$: the soundness of $\vdashA$ follows from the soundness
of $\vdashAts$.
Completeness needs a more detailed explaination. The algorithmic
system $\vdashA$
is not complete w.r.t.\ the language presented in
Section~\ref{sec:syntax} because it cannot deduce negated arrow
types for functions.
However, no practical programming language would implement the full
language of Section~\ref{sec:syntax}, but rather restrict all
expressions of the form $\tcase{e}{t}{e_1}{e_2}$ so that the type $t$ tested in them is either
non functional (e.g., products, integer, a record type, etc.) or it is
$\Empty\to\Any$ (i.e., the expression can just test whether $e$ returns a function
or not). There are multiple reasons to impose such a restriction, the
most important ones can be summarized as follows:
\begin{enumerate}[left=0pt .. 12pt]
\item For explicitly-typed languages it may yield conterintutive results,
since for instance $\lambda^{\Int\to\Int}x.x\in\Bool\to\Bool$
should fail despite the fact that identity functions maps Booleans
to Booleans.
\item For implicitly-typed languages it yields a semantics that
depends on the inference algorithm, since $(\lambda
y.(\lambda x.y))3\in 3{\to} 3$ may either fail or not according to
whether the type deduced for the result of the expression is either
$\Int{\to}\Int$ or $3{\to}3$ (which are both valid but incomparable).
\item For gradually-typed languages it would yield an unsound system as
we explain in Section~\ref{sec:gradual}.
\end{enumerate}
Now, if we apply this restriction to the language of
Section~\ref{sec:syntax}, then the algorithmic system of
section~\ref{sec:algorules} is complete. Let say that an expression $e$
is \emph{positive} if it never tests a functional type more precise
than $\Empty\to\Any$ (see
Appendix~\ref{sec:proofs_algorithmic_without_ts} for the formal
definition). Then we have:
\begin{theorem}[Completeness]
For every type environment $\Gamma$ and positive expression $e$, if
$\Gamma\vdash e: t$, then there exists $t'$ such that $\Gamma\vdashA
e: t'$.
\end{theorem}
We were not able to prove full completeness, just a partial form of it. As
anticipated, the problems are twofold: $(i)$ the recursive nature of
We can also use the algorithmic system $\vdashAts$ defined for the proof
of Theorem~\ref{th:algosound} to give a more precise characterization
of terms for which our algorithm is complete. The system $\vdashAts$
copes with negated arrow types but it still is not
complete essentially for two reasons: $(i)$ the recursive nature of
rule \Rule{Path} and $(ii)$ the use of nested \Rule{PAppL} that yield
a precision that the algorithm loses by applying \tsrep{} in the
a precision that the algorithm loses by using type schemes in the
definition of \constrf{} (case~\eqref{due} is the critical
one). Completeness is recovered by $(i)$ limiting the depth of the
derivations and $(ii)$ forbidding nested negated arrows on the
left-hand side of negated arrows.\vspace{-.7mm}
\begin{definition}[Rank-0 negation]
A derivation of $\Gamma \vdash e:t$ is \emph{rank-0 negated} if \Rule{Abs--} never occurs in the derivation of a left premise of a \Rule{PAppL} rule.\vspace{-.7mm}
A derivation of $\Gamma \vdash e:t$ is \emph{rank-0 negated} if
\Rule{Abs--} never occurs in the derivation of a left premise of a
\Rule{PAppL} rule.\vspace{-.7mm}
\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
......@@ -373,14 +413,9 @@ left-hand side of another negated arrow.
\begin{theorem}[Partial Completeness]
For every $\Gamma$, $e$, $t$, if $\Gamma \vdash e:t$ is derivable by a rank-0 negated derivation, then there exists $n_o$ such that $\Gamma\vdashA e: t'$ and $t'\leq t$.
\end{theorem}
\noindent The use of type schemes and of possibly diverging iterations
yields a system that may seem overly complicated. But it is important
to stress that this system is defined only to study the
type inference system of Section~\ref{sec:static} and in particular to probe
how close we can get to a complete algorithm for it. But for
practical applications type schemes are not needed, since they are
necessary only when type cases may specify types with negative arrows
and this, in practice, never happens (see Footnote~\ref{foo:typecase} and Corollary~\ref{app:completeness}). This is why for our implementation we use the
CDuce library in which type schemes are absent and functions are typed
only by intersections of positive arrows. We present the implementation in Section~\ref{sec:practical}
but before let us study some extensions.
\noindent This last result is only of theoretical interest since in
practice one will implement languages with positive
expressions only. This is why for our implementation we use the CDuce
library in which type schemes are absent and functions are typed only
by intersections of positive arrows. We present the implementation in
Section~\ref{sec:practical} but before let us study some extensions.
......@@ -155,6 +155,6 @@ It is equivalent to the type $\orecord{b=\Bool}$, and thus we can deduce that $x
\subsection{Refining function types}\label{sec:refining}
\input{refining}
\subsection{Integrating gradual typing}
\subsection{Integrating gradual typing}\label{sec:gradual}
\input{gradual}
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