As we explained in the introduction, both TypeScript and Flow deduce the type

\code{(number$\vee$string) $\to$ (number$\vee$string)} for the first definition of the function \code{foo} in~\eqref{foo}, and the more precise type\vspace{-3pt}

can be deduced by these languages only if they are instructed to do so: the

programmer has to explicitly annotate \code{foo} with the

type \eqref{tyinter}: we did it in \eqref{foo2} using Flow---the TypeScript annotation for it is much heavier. But this seems like overkill, since a simple

analysis of the body of \code{foo} in \eqref{foo} shows that its execution may have

two possible behaviors according to whether the parameter \code{x} has

type \code{number} or not (i.e., or \code{(number$\vee$string)$\setminus$number}, that is \code{string}), and this is

should be enough for the system to deduce the type \eqref{tyinter}

even in the absence the annotation given in \eqref{foo2}.

%

In this section we show how to do it by using the theory of occurrence

typing we developed in the first part of the paper. In particular, we

collect the different types that are assigned to the parameter of a function

in its body, and use this information to partition the domain of the function

and to re-type its body. Consider a more involved example in a pseudo

Whenever a function parameter is the argument of an

overloaded function, we record as possible types for this parameter

all the domains $t_i$ of the arrows that type the overloaded

function, restricted (via intersection) by the static type $t$ of the parameter and provided that the type is not empty ($t\wedge t_i\not\simeq\Empty$). We show the remarkable power of this rule on some practical examples in Section~\ref{sec:practical}.

\ignore{\color{darkred} RANDOM THOUGHTS:

A delicate point is the definition of the union

$\psi_1\cup\psi_2$. The simplest possible definition is the

component-wise union. This definition is enough to avoid the problem

of typecases on casted values and it is also enough to type our case

study, as we showed before. However if we want a more precise typing

discipline we may want to consider a more sophisticated way of

combining the information collected by the various $\psi$. For

instance, consider the following pair

\[\code{(\ite x s {e_1}{e_2} , \ite x t {e_3}{e_4})}\]

Then we have $x:\Any\vdash\code{(\ite x s {e_1}{e_2} , \ite x t

{e_3}{e_4})}\triangleright x\mapsto\{s,\neg s, t, \neg t\}$. However if this

code is the body of a function with parameter $x$, then it may be

tempting to try to produce a finer-grained analysis: for example,

instead of checking as input type just $s$ and $t$ one could check

instead $s\setminus t$, $t\setminus s$, and $s\wedge t$, whenever these

three types are not empty. This can be obtained by defining the union

operation as follows:

\[(\psi_0\cup\psi_1)(x)=\{ t \alt\exists t_1\in\psi_1(x), t_2\in\psi_2(x), t=t_1\setminus t_2\text{ or } t=t_2\setminus t_1\text{ or } t=t_1\wedge t_2\text{ and } t\not\simeq\Empty\}\]

Do we really gain in precision? I think the gain is minimum. All we may obtain just come from a polymorphic use of the variable, but we can hardly gain more. Probably it is not worth the effort. As a concrete case consider

\[\code{function x \{(\ite x {\texttt{String|Bool}}{x}{x} , \ite x {\texttt{Bool|Int}}{x}{x})}\}\]

So what?

A simple solution would be to define the union as follows

\begin{equation}

(\psi_0\cup\psi_1)(x)=

\left\{\begin{array}{ll}

\psi_i(x) &\text{ if }\psi_i(x)\subseteq\psi_{((i+1)\,\text{mod}\,2)}(x)\\

\psi_0(x)\cup\psi_1(x) &\text{ otherwise}

\end{array}\right.

\end{equation}

and $\psi_1(x)\subseteq\psi_2(x)\iff\forall\tau\in\psi_1(x),\exists\tau'\in\psi_2(x),\tau\leq\tau'$

This would be interesting to avoid to use as domains those in

$\psi_\circ$ that would be split in two in the $\psi_1$ and $\psi_2$

of the ``if'' ... but it is probably better to check it by modifying

the rule of ``if'' (that is, add $\psi_\circ$ only for when it brings new