Commit 15632fed authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

patched example (10)

parent fd5f4370
...@@ -368,7 +368,7 @@ $\ifty{\textsf{false}}{\Bool}{\textsf{false}}{\textsf{true}}$): see Appendix~\re ...@@ -368,7 +368,7 @@ $\ifty{\textsf{false}}{\Bool}{\textsf{false}}{\textsf{true}}$): see Appendix~\re
\paragraph{Interdependence of checks} The last class of technical problems arise \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 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: that pose a problem. The first can be shown by two functions $f$ and $g$ both of type $(\Int\to\Int)\wedge(\Any\to\Bool)$, $x$ of type $\Any$ and the test:
\begin{equation}\label{nest1} \begin{equation}\label{nest1}
\ifty{(fx,gx)}{\pair\Int\Bool}{\,...\,}{\,...} \ifty{(fx,gx)}{\pair\Int\Bool}{\,...\,}{\,...}
\end{equation} \end{equation}
...@@ -377,8 +377,7 @@ we deduce $\Int$ for the first occurrence of $x$ and $\Any$ for the ...@@ -377,8 +377,7 @@ 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 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 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, 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 then the type deduced for $x$ is for positive branch of \eqref{nest1} is $\Empty$. In other words, we want to produce type
never be selected. In other words, we want to produce type
environmments for occurrence typing by taking into account all environmments for occurrence typing by taking into account all
hypotheses available, even when these hypotheses are formulated later hypotheses available, even when these hypotheses are formulated later
in the flow of control. This will be done in the type systems of in the flow of control. This will be done in the type systems of
......
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