has type $\Int\vee\Bool$ as we show in detail next.

All these type deductions require to make different type assumptions for

the typing of the ``then'' and of the ``else'' branches. Let us

examine it more in detail for the expression in~\eqref{two}. This expression is

typed in the following type environment:

$x_1:(\Int\to\Int)\wedge(\Bool\to\Bool), x_2:\Int\vee\Bool$. All we

can deduce is then that the application $x_1x_2$ has type

$\Int\vee\Bool$ which is not enough to type either the ``then''branch

$\Int\vee\Bool$ which is not enough to type either the ``then''branch

or the ``else'' branch. In order to type the ``then'' branch

$(x_1x_2)+x_2$ we must be able to deduce that both $x_1x_2$ and $x_2$

are of type \Int. Since we are in the ``then'' branch, then we know that

...

...

@@ -113,13 +113,13 @@ barring an \Int. If we denote by \Any\ the type of all values and by

$\setminus$ the set difference, then this means that in the else branch we

know that $x_1x_2$ has type $\Any{\setminus}\Int$---written

$\neg\Int$---, that is, it can return values of any type barred \Int. Reasoning as for the ``then'' branch we then assume that

$x_1x_2$ has type $(\Int\vee\Bool)\wedge\neg\Int$ (i.e., $(\Int\vee\Bool)\setminus\Int$, that is,\Bool), that

$x_1x_2$ has type $(\Int\vee\Bool)\wedge\neg\Int$ (i.e., $(\Int\vee\Bool)\setminus\Int$, that is,\Bool), that

$x_2$ must be of type \Bool\ for the application to have type

$\neg\Int$ and therefore we assume that $x_2$ has type

$(\Int\vee\Bool)\wedge\Bool$ (i.e., again \Bool).

We have seen that we can specialize in the branches the type of the

whole expression, the type of the argument $x_2$ of the application,

whole expression$x_1x_2$, the type of the argument $x_2$ of the application,

but what about the type of $x_1$? Well, this depends on the type of

$x_1$ itself. In particular, if instead of an intersection type $x_2$

is typed by a union type, then the test may give us information about

...

...

@@ -210,7 +210,7 @@ function in $t_1$ will surely yield a $\String$ result.

Once we have determined $t_2^+$, it is then not very difficult to refine the

type $t_1$, too. If the test succeeded, then we know two facts: first,

type $t_1$ for the positive branch, too. If the test succeeded, then we know two facts: first,

that the function was applied to a value in $t_2^+$ and, second, that

the application did not diverge and, thus, returned a result in

$t_1\!\circ t_2^+$ (which is a subtype of $t_1\!\circ

...

...

@@ -282,7 +282,7 @@ This is essentially what we formalize in Section~\ref{sec:language}.

In the previous section we outlined the main ideas of our approach to occurrence typing. However, devil is in the details. So the formalization we give in Section~\ref{sec:language} is not so smooth as we just outlined: we must introduce several auxiliary definitions to handle some corner cases. This section presents by tiny examples the main technical difficulties we had to overcome and the definitions we introduced to handle them. As such it provides a kind of road-map to the technicalities of Section~\ref{sec:language}.

\paragraph{Typing occurrences} As it should be clear by now, not only variables but also generic expression are given different types in the ``then'' and ``else'' branches of type tests. For instance, in \eqref{two} the expression $x_1x_2$ has type \Int{} in the positive branch and type \Bool{} in the negative one. In this specific case it is possible to deduce these typings from the types of the variables (in particular since$x_2$ has type \Int{} the positive and \Bool{} in the negative branches), but in general this cannot be done. For instance, consider $x_1:\Int\to(\Int\vee\Bool)$, $x_2:\Int$, and the expression

\paragraph{Typing occurrences} As it should be clear by now, not only variables but also generic expression are given different types in the ``then'' and ``else'' branches of type tests. For instance, in \eqref{two} the expression $x_1x_2$ has type \Int{} in the positive branch and type \Bool{} in the negative one. In this specific case it is possible to deduce these typings from the specialized types of the single variables (in particular, thanks to the fact that$x_2$ has type \Int{} the positive branch and \Bool{} in the negative one), but this is not possible in general. For instance, consider $x_1:\Int\to(\Int\vee\Bool)$, $x_2:\Int$, and the expression

\begin{equation}\label{twobis}

\ifty{x_1x_2}{\Int}{...x_1x_2...}{...x_1x_2...}

\end{equation}

...

...

@@ -321,15 +321,15 @@ shown by the following example

\end{equation}

If $e$ is an expression of type $\Int\to t$, then, as discussed before,

the positive branch will have type $(\Int\to t)\setminus(\Int\to\neg

t)$. If furthermore the negative branch is of the same type, then this

t)$. If furthermore the negative branch is of the same type (or of a subtype), then this

will also be the type of the whole expression in \eqref{bistwo}. Now imagine

that the application $e(42)$ reduces to an integer, then the whole

expression in \eqref{bistwo} reduces to $e$; but this has type

$\Int\to t$ which is \emph{not} a subtype of $(\Int\to

$\Int\to t$ which, in general, is \emph{not} a subtype of $(\Int\to

t)\setminus(\Int\to\neg t)$, and therefore type is not preserved by the reduction. To cope with this problem, in

Section~\ref{sec:language} we resort to \emph{type schemes} a

technique introduced by~\citet{Frisch2008} to type expressions by

sets of types, so that the expression in \eqref{bistwo} will have both these types.

sets of types, so that the expression in \eqref{bistwo} will have both the types at issue.

The second corner case is a slight modification of the example above