@@ -112,7 +112,7 @@ Depending on the actual $t$ and on the static types of $x_1$ and $x_2$, we

can make type assumptions for $x_1$, for $x_2$, \emph{and} for the application $x_1x_2$

when typing $e_1$ that are different from those we can make when typing

$e_2$. For instance, suppose $x_1$ is bound to the function \code{foo} defined in \eqref{foo2}. Thus $x_1$ has type $(\Int\to\Int)\wedge(\String\to\String)$ (we used the syntax of the types of Section~\ref{sec:language} where unions and intersections are denoted by $\vee$ and $\wedge$ and have priority over $\to$ and $\times$, but not over $\neg$).

Then it is not hard to see that the expression\footnote{This and most of the following expressions are just given for the sake of example. Determining the type of expressions other than variables is interesting for constructors but less so for destructors such as applications, projections, and selections: any reasonable programmer would not repeat the same application twice, (s)he would store its result in a variable. This becomes meaningful when we introduce constructor such as pairs, as we do for instance in the expression in~\eqref{pair}.}

Then it is not hard to see that the expression\footnote{This and most of the following expressions are just given for the sake of example. Determining the type \emph{in each branch}of expressions other than variables is interesting for constructors but less so for destructors such as applications, projections, and selections: any reasonable programmer would not repeat the same application twice, (s)he would store its result in a variable. This becomes meaningful with constructor such as pairs, as we do for instance in the expression in~\eqref{pair}.}

%

\begin{equation}\label{mezzo}

\texttt{let }x_1 \texttt{\,=\,}\code{foo}\texttt{ in }\ifty{x_1x_2}{\Int}{((x_1x_2)+x_2)}{\texttt{42}}