@@ -49,7 +49,19 @@ Let $t$ be a functional type (i.e., $t\leq\Empty\to\Any$) then

Given an expression $e$ and a type $t$ we use $\Gamma^p_{\Gamma,e,t}$ to denote the environment that maps the expression $\occ e\pi$ to $\Gp p {\Gamma,e,t}(\pi)$ if $\pi$ is a subterm of $e$ and undefined otherwise. We define the following algorithmic system (we deduce at most one type for every expression, type environment pair, so that $\tyof{}{}$ is defined).

\begin{definition}

Given an expression $e$ and a type $t$ we use $\Gamma^p_{\Gamma,e,t}$ to denote the environment that maps every subterm $e'$ of $e$ to the type $\bigwedge_{\{\pi\alt\occ e\pi\equiv e'\}}\Gp p {\Gamma,e,t}(\pi)$ and is undefined otherwise.

\end{definition}

The reason for the definition above is that the same subterm of $e$

may occur several times in $e$ and therefore we can collect for every

occurrence a different type constraint. Since all the constraints must

hold, then we take their intersection. For instance if $f$ is a function

of type $(s_1\times s_2\to t)\wedge( s_3\to\neg t)$ and we test

whether $f(x,x)$ is of type $t$ then we know that the test succeed only if $(x,x)$ is of

type $s_1\times s_2$, that is that $x$ has both type $s_1$ and type

$s_2$ and thus their intersection.

We define the following algorithmic system (we deduce at most one type for every expression, type environment pair, so that $\tyof{}{}$ is defined).