Commit 6f56197c authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files


parent afa1169e
......@@ -183,7 +183,7 @@ application. Here by iterating a second time, the algorithm deduces
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
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 type 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.
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