@@ -109,7 +109,7 @@ As usual we denote by $\Cx[e]$ the term obtained by replacing $e$ for

the hole in the context $\Cx$ and we have that $e\reduces e'$ implies

$\Cx[e]\reduces\Cx[e']$.

\subsection{Static semantics}

\subsection{Static semantics}\label{sec:static}

While the syntax and reduction semantics are, on the whole, pretty

standard, for the type system we will have to introduce several

...

...

@@ -339,7 +339,7 @@ These rules describe how to produce by occurrence typing the type

environments while checking that an expression $e$ has type $t$. They state that $(i)$ we can

deduce from $\Gamma$ all the hypothesis already in $\Gamma$ (rule

\Rule{Base}) and that $(ii)$ if we can deduce a given type $t'$ for a particular

occurrence $\varpi$ of the expression $e$ being checked, than we can add this

occurrence $\varpi$ of the expression $e$ being checked, then we can add this

hypothesis to the produced type environment (rule \Rule{Path}). The rule

\Rule{Path} uses a (last) auxiliary judgement $\pvdash{\Gamma} e t

\varpi:t'$ to deduce the type $t'$ of the occurrence $\occ e \varpi$ when

...

...

@@ -430,9 +430,9 @@ e$) is of type $t'$, then the type of $e$ must be of the form

$\pair{t'}\Any$ (respectively, $\pair\Any{t'}$).

This concludes the presentation of our type system, which satisfies

the property of soundness, deduced, as customary, from the properties

of progress and subject reduction, whose proofs are given in Appendix~\ref{app:soundness}.

\begin{theorem}[soundness]

the property of safety, deduced, as customary, from the properties

of progress and subject reduction (\emph{cf.} Appendix~\ref{app:soundness}).

\begin{theorem}[type safety]

For every expression $e$ such that $\varnothing\vdash e:t$ either $e$

diverges or there

exists a value $v$ of type $t$ such that $e\reduces^* v$.

...

...

@@ -446,7 +446,7 @@ exists a value $v$ of type $t$ such that $e\reduces^* v$.

\subsection{Algorithmic system}

\label{ssec:algorithm}

The system we defined in the previous section implements the ideas we

illustrated in the introduction and it is sound. Now the problem is to

illustrated in the introduction and it is safe. Now the problem is to

decide whether an expression is well typed or not, that is, to find an

algorithm that given a type environment $\Gamma$ and an expression $e$

decides whether there exists a type $t$ such that $\Gamma\vdash e:t$

...

...

@@ -469,7 +469,7 @@ to the presence of structural rules\footnote{\label{fo:rules}In logic, logical r

either $\to$, or $\times$, or $b$), while identity rules (e.g.,

axioms and cuts) and structural rules (e.g., weakening and

contraction) do not.} such as \Rule{Subs} and \Rule{Inter}. We

handle it in the classic way: we define an algorithmic system that

handle this presence in the classic way: we define an algorithmic system that

tracks the miminum type---actually, the minimum \emph{type scheme}---of an

expression; this system is obtained from the original system by removing

the two structural rules and by distributing suitable checks of the subtyping

...

...

@@ -500,7 +500,7 @@ We introduce the new syntactic category of \emph{types schemes} which are the te

\]

Type schemes denote sets of types, as formally stated by the following definition:

\begin{definition}[Interpretation of type schemes]

We define the function $\tsint{\_}$ that maps type schemes into sets of types.

We define the function $\tsint{\_}$ that maps type schemes into sets of types.\vspace{-3mm}

\begin{align*}

\begin{array}{lcl}

\tsint t &=&\{s\alt t \leq s\}\\

...

...

@@ -543,7 +543,7 @@ We also need to perform intersections of type schemes so as to intersect the sta

\end{lemma}

Finally, given a type scheme $\ts$ it is straightforward to choose in its interpretation a type $\tsrep\ts$ which serves as the canonical representative of the set (i.e., $\tsrep\ts\in\tsint\ts$):

\begin{definition}[Representative]

We define a function $\tsrep{\_}$ that maps every non-empty type scheme into a type, \textit{representative} of the set of types denoted by the scheme.

We define a function $\tsrep{\_}$ that maps every non-empty type scheme into a type, \textit{representative} of the set of types denoted by the scheme.\vspace{-3mm}

\begin{align*}

\begin{array}{lcllcl}

\tsrep t &=& t &\tsrep{\ts_1 \tstimes\ts_2}&=&\pair{\tsrep{\ts_1}}{\tsrep{\ts_2}}\\

...

...

@@ -577,12 +577,20 @@ checking that it has a type subtype of $\Empty{\to}\Any$. Determining

its domain and the type of the application is more complicated and needs the operators $\dom{}$ and $\circ$ that we informally described in Section~\ref{sec:ideas} where we also described the operator $\worra{}{}$. These three operators are used by our algorithm and are formally defined as follows:

\begin{eqnarray}

\dom t & = &\max\{ u \alt t\leq u\to\Any\}

\\[-.5mm]

\\[-.8mm]

\apply t s & = &\,\min\{ u \alt t\leq s\to u\}

\\[-.5mm]

\\[-.8mm]

\worra t s & = &\,\min\{u \alt t\circ(\dom t\setminus u)\leq\neg s\}\label{worra}

\end{eqnarray}

We need similar operators for projections since the type $t$ of $e$ in $\pi_i e$ may not be a single product type but, say, a union of products: all we know is that $t$ must be a subtype of $\pair\Any\Any$. So let $t$ be a type such that $t\leq\pair\Any\Any$, then we define:

%In short, $\dom t$ is the largest domain of any single arrow that

%subsumes $t$, $\apply t s$ is the smallest domain of an arrow type

%that subsumes $t$ and has domain $s$ and $\worra t s$ was explained

%before.

We need similar operators for projections since the type $t$

of $e$ in $\pi_i e$ may not be a single product type but, say, a union

of products: all we know is that $t$ must be a subtype of

$\pair\Any\Any$. So let $t$ be a type such that $t\leq\pair\Any\Any$,

then we define:

\begin{equation}

\begin{array}{lcrlcr}

\bpl t & = &\min\{ u \alt t\leq\pair u\Any\}\qquad&\qquad

...

...

@@ -703,7 +711,7 @@ above to an environment that already is the result of $\Refinef$, and so on. The

algorithm should compute the type environment as a fixpoint of the

function $X\mapsto\Refine{e,t}{X}$. Unfortunately, an iteration of $\Refinef$ may

not converge. As an example consider the (dumb) expression $\tcase

{x_1x_2}{\Any}{e_1}{e_2}$: if $x_1:\Any\to\Any$, then every iteration of

{x_1x_2}{\Any}{e_1}{e_2}$. If $x_1:\Any\to\Any$, then every iteration of

$\Refinef$ yields for $x_1$ a type strictly more precise than the type deduced in the

previous iteration.

...

...

@@ -733,7 +741,7 @@ While this is unsatisfactory from a formal point of view, in practice

the problem is a very mild one. Divergence may happen only when

refining the type of a function in an application: not only such a

refinement is meaningful only when the function is typed by a union

type (which is quite rare in practice)\footnote{The only impact of

type (which is quite rare in practice)\footnote{\label{foo:typecase}The only impact of

adding a negated arrow type to the type of a function is when we

test whether the function has a given arrow type: in practice this

never happens since programming languages test whether a value

...

...

@@ -846,3 +854,16 @@ for variables.

The system above satisfies the following properties:\beppe{State here

soundness and partial completeness}

The use of type schemes and the possible non convergence of iterations

yield a system that may seem overly complicated. But it is important

to stress that this systems is defined only to study the declarative

type inference system of Section~\ref{sec:static} and in particular to prod

how close we can get to a complete algorithm to it. But for the

practical application type schemes are not needed, since they are

necessary only when type cases may specify types with negative arrows

and this in practice never happens: see Footnote

\ref{foo:typecase}. This is why for our implementation we use the

CDuce library in which type schemes are absent and functiond are typed

only by intersections of positive arrows. We present the implementation in Section~\ref{sec:practical}