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

empty

parent eeec9bf6
...@@ -140,7 +140,7 @@ $(\lnot\True\to((\True\to\True) \land (\lnot\True\to\False))$ ...@@ -140,7 +140,7 @@ $(\lnot\True\to((\True\to\True) \land (\lnot\True\to\False))$
let example10 = fun (x : Any) -> let example10 = fun (x : Any) ->
if (f x, g x) is (Int, Bool) then 1 else 2 if (f x, g x) is (Int, Bool) then 1 else 2
\end{lstlisting} &\vfill \end{lstlisting} &\vfill
$(\Int\to\Empty)\land(\Any\setminus\Int\to{}2)$\newline $(\Int\to\textsf{Empty})\land(\neg\Int\to{}2)$\newline
\texttt{Warning: line 4, 39-40: unreachable expression} \texttt{Warning: line 4, 39-40: unreachable expression}
\\\hline \\\hline
\end{tabular} \end{tabular}
......
...@@ -176,13 +176,13 @@ for which the very same types as in Table~\ref{tab:implem} are deduced. ...@@ -176,13 +176,13 @@ for which the very same types as in Table~\ref{tab:implem} are deduced.
Last but not least Code~10 (corresponding to our introductory Last but not least Code~10 (corresponding to our introductory
example~\eqref{nest1}) illustrates the need for iterative refinement of example~\eqref{nest1}) illustrates the need for iterative refinement of
type environments, as defined in Section~\ref{sec:typenv}. As type environments, as defined in Section~\ref{sec:typenv}. As
explained, a single pass analysis would deduce independently explained, a single pass analysis would deduce
for {\tt x} for {\tt x}
a type \Int{} from the {\tt f\;x} application and \Any{} from the {\tt g\;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 application. Here by iterating a second time, the algorithm deduces
that {\tt x} has type \Empty, that is that the first branch can never that {\tt x} has type $\Empty$ (i.e., $\textsf{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 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 type $(\Int{\to}\Int)\land(\Any{\to}\Bool)$ is to diverge when the
argument is of type \Int: since this intersection types states that argument is of type \Int: since this intersection types states that
whenever the input is \Int, {\em both\/} branches can be selected, 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. yielding a result that is at the same time an integer and a Boolean.
......
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