Commit 1d014a41 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

final pass main paper

parent ad91dd0a
......@@ -56,21 +56,24 @@ instantiation. The idea is to single out the two most general type
substitutions for which some test may succeed and fail, respectively, and apply these
substitutions to refine the types of the corresponding occurrences
in the ``then'' and ``else'' branches. Concretely, consider the test
$x_1x_2\in t$ where $t$ is a closed type and $x_1$, $x_2$ are
$x_1x_2\in t^\circ$ where $t^\circ$ is a closed type and $x_1$, $x_2$ are
variables of type $x_1: s\to t$ and $x_2: u$ with $u\leq s$. For the
positive branch we first check whether there exists a type
substitution $\sigma$ such that $t\sigma\leq\neg\tau$. If it does not
substitution $\sigma$ such that $t\sigma\leq\neg t^\circ$. If it does not
exists, then this means that for all possible assignments of
polymorphic type variables of $s\to t$, the test may succeed, that is,
the success of the test does not depend on the particular instance of
$s\to t$ and, thus, it is not possible to pick some substitution for
refining the occurrence typing. If it exists, then
we find a type substitution $\sigma_\circ$ such that $\tau\leq
we find a type substitution $\sigma_\circ$ such that $t^\circ\leq
t\sigma_\circ$ and we refine for the
positive branch the types of $x_1$, of $x_2$, and of $x_1x_2$ by applying $\sigma_\circ$ to their types. While the
idea is clear (see Appendix~\ref{app:roadmap} for a more detailed explanation),
the technical details are quite involved, especially when considering
functions typed by intersection types and/or when integrating gradual
typing. This needs a whole gamut of non trivial research that we plan to
the technical details are quite involved, especially if we also want
functions with intersection types and/or gradual
typing. Nevertheless, our approach has an edge on current systems which,
in our ken, do not account for polymorphism.
\iflongversion
This needs a whole gamut of non trivial research that we plan to
develop in the near future.
\fi
......@@ -76,7 +76,7 @@ collections. Types are mapped to first order formulæ and an SMT-solver is
then used to (try to) prove their satisfiability. The refinement
types they present go well beyond what can be expressed with the set-theoretic
types we use (as they allow almost any pure expression to occur in
types). However, the system forgoes any notion of completeness
types). However, the system forgoes any notion (or just characterization) of completeness
and the
subtyping algorithm is largely dependent on the subtle behaviour of
the SMT solver (which may timeout or give an incorrect model that
......@@ -84,7 +84,7 @@ cannot be used as a counter-example to explain the type-error).
As with our work, the typing rule for the {\tt if~$e$ then $e_1$ else
$e_2$} construct
of Dminor refines the type of each branch by remembering that $e$
(resp. $\lnot e$) is true in $e_1$ (resp. $e_2$) but this information
(resp. $\lnot e$) is true in $e_1$ (resp. $e_2$) and this information
is not propagated to the outer context.
A similar approach is taken in \cite{Chugh12}, and extended to so-called nested refinement types. In these types, an arrow type may
appear in a logical formula (where previous work only allowed formulae
......@@ -116,13 +116,13 @@ did here and, since they perform flow analysis and use an effect
system (to track mutable variables), even more. However, this results
in a specific and very complex system. Their formalization includes
only union types (though, Flow accepts also intersection types as
in \eqref{foo2}) which are used in \emph{ad hoc} manner by the type
we showed in \eqref{foo2}) which are used in \emph{ad hoc} manner by the type
system, for instance to type record types. This allows Flow to perform
an analysis similar to the one we did for Code 8 in
Table~\ref{tab:implem}, but also has as a consequence that in some
cases unions do not behave as expected. In contrast, our approach is
more classic and foundational: we really define a type system, typing
rules looks like classic ones and are easy to understand, unions are
rules look like classic ones and are easy to understand, unions are
unions of values (and so are intersections and negations), and the
algorithmic part is---excepted for fix points---relatively simple
(algorithmically Flow relies on constraint generation and
......
......@@ -26,7 +26,7 @@ Take again the expression in~\eqref{typagain} and imagine that $t$ is
(\alpha\vee\Bool)$.\footnote{%
A non-trivial example of an expression
of this type is the function $\lambda^{\alpha\to
(\alpha\vee\Bool)}x. \ite e u x \texttt{true}$.}
(\alpha\vee\Bool)}x. \ite e u x \texttt{true}$. for some expression $e$ and type $u$.}
%
We suppose the expression $x_1x_2$ to be well-typed and
therefore that $x_2$ is typed by a subtype of $\alpha$, say,
......
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