Commit 638c93a5 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

.

parent bae02fd0
......@@ -133,6 +133,18 @@ let xor_ = fun (x : Any) -> fun (y : Any) ->
$\True\to((\True\to\False)\land(\lnot\True\to\True))~\land$\newline
$(\lnot\True\to((\True\to\True) \land (\lnot\True\to\False))$
\\\hline
10 & \begin{lstlisting}
(* f and g have type:
(Int -> Int) & (Any ->Bool) *)
let example10 =
fun (x : Any) ->
if (f x, g x) is (Int, Bool) then 1 else 2
\end{lstlisting} &\vfill
$(\Int\to\Empty)\land(\Any\setminus\Int\to{}2)$
\texttt{Warning: line 4, charcater 39-40: expression is unreachable}
\\\hline
\end{tabular}
}
\caption{Types inferred by implementation}\vspace{-10mm}
......
......@@ -370,13 +370,13 @@ $\ifty{\textsf{false}}{\Bool}{\textsf{false}}{\textsf{true}}$): see Appendix~\re
from the mutual dependence of different type checks. In particular, there are two cases
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}
\ifty{(fx,gx)}{\pair\Int\Bool}{\,...\,}{\,...}
\ifty{(f\,x,g\,x)}{\pair\Int\Bool}{\,...\,}{\,...}
\end{equation}
If we independently check $fx$ against $\Int$ and $gx$ against $\Bool$
If we independently check $f\,x$ against $\Int$ and $g\,x$ 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,
the test of $f\,x$, that is, that $x$ is of type \Int, to check $g\,x$ against \Bool,
then the type deduced for $x$ is $\Empty$---i.e., the branch is never selected. In other words, we want to produce type
environmments for occurrence typing by taking into account all
the available hypotheses, even when these hypotheses are formulated later
......
......@@ -127,7 +127,7 @@ nodes. This splits, at the type level, the case for the \Keyw{Element}
type depending on whether the content of the \texttt{childNodes} field
is the empty list or not.
Our implementation features one last enhancement that allows us
Our implementation features another enhancement that allows us
to further improve the precision of the inferred type.
Consider the definition of the \texttt{xor\_} operator (Code~9).
Here the rule~[{\sc AbsInf}+] is not sufficient to precisely type the
......@@ -172,3 +172,21 @@ We consider \True, \Any, and $\lnot\True$ as candidate types for
let xor_ = fun (x : Any) -> fun (y : Any) -> and_ (or_ x y) (not_ (and_ x y))
\end{alltt}
for which the very same types as in Table~\ref{tab:implem} are deduced.
Last but not least Code~10 (which corresponds to our introductory
Example~\ref{nest1}) illustrate the need for iterative refinement of
type environments, as defined in Section~\ref{sec:typenv}. Indeed, has
we have explained, a single pass analysis would deduce independently
for {\tt x}
a type \Int from the {\tt f~x} application and \Any from the {\tt g~x}
application. Here by iterating a second time, the algorithm deduces
that {\tt x} has type \Empty, that is that the first branch can never
be selected (and our implementation warns the user accordingly). In
hindsight, the only way for a well typed overloaded function to have
type $(\Int\to\Int)\land(\Any\to\Bool)$ is to diverge when the
argument is of type \Int (since this intersection types states that
whenever the input is \Int, {\em both\/} branches can be selected,
yielding a result that is at the same time an integer and a Boolean.
This is precisely reflected by the case $\Int\to\Empty$ in the result.
Indeed our {\tt example10} function can be applied to an integer, but
at runtime the application of {\tt f ~x} will diverge.
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