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

rewording

parent 8e45f539
......@@ -332,9 +332,9 @@ for the multiple occurrences of it.
\paragraph{Type preservation} We aim at defining a type system sound in the usual sense of~\citet{Wright1994}, that is, a system that
\paragraph{Type preservation} We want our type system to be sound in the sense of~\citet{Wright1994}, that is, it
satisfies progress and type preservation. The latter property is
challenging in our system because, as explained just above, our type
challenging because, as explained just above, our type
assumptions are not only about variables but also about
expressions. Two corner cases are particularly difficult. The first is
shown by the following example
......@@ -365,13 +365,22 @@ $\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}.
\paragraph{Checks interdependence} The last class of technical problems arise
from the multual dependence of different checks type checks. In particular, there are two cases
\paragraph{Interdependence of checks} The last class of technical problems arise
from the mutual dependence of different type checks. In particular, there are two cases
that pose a problem. The first can be shown by considering two functions $f$ and $g$ both of type $(\Int\to\Int)\wedge(\Any\to\Bool)$ and the test
\begin{equation}\label{nest1}
\ifty{(fx,gx)}{\pair\Int\Bool}{\,...\,}{\,...}
\end{equation}
if we independently check $fx$ against $\Int$ and $gx$ against $\Bool$ we deduce $\Int$ for the first occurrence of $x$ and $\Any$ for the second. Thus we would type the positive branch under the hypothesis that $x$ is of type $\Int$. But if we use the hypothesis generated by the test of $fx$, that is that $x$ is of type \Int, to check $gx$, then it is easy to see that the positive branch of \eqref{nest1} can never be selected. In other words, we want to produce type environmments for occurrence typing by taking into account all all hypotheses available, even when these hypotheses are formulated later in the flow of control. This will be done in the type systems of
If we independently check $fx$ against $\Int$ and $gx$ against $\Bool$
we deduce $\Int$ for the first occurrence of $x$ and $\Any$ for the
second. Thus we would type the positive branch of \eqref{nest1} under the hypothesis
that $x$ is of type $\Int$. But if we use the hypothesis generated by
the test of $fx$, that is, that $x$ is of type \Int, to check $gx$ against \Bool,
then it is easy to see that the positive branch of \eqref{nest1} can
never be selected. In other words, we want to produce type
environmments for occurrence typing by taking into account all
hypotheses available, even when these hypotheses are formulated later
in the flow of control. This will be done in the type systems of
Section~\ref{sec:language} by the rule \Rule{Path} and will require at
algorithmic level to look for a fix-point solution of a function, or
an approximation thereof.
......
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