@@ -444,10 +444,28 @@ require two distinct technical solutions. The first origin is the rule

\Rule{Abs-} by which it is possible to deduce for every well-typed

lambda abstractions infinitely many types, that is the annotation of

the function intersected with as many negations of arrow types as it

is possible without making the type empty. To handle this multiplicity we use the technique of \emph{type schemes} defined by~\citet{Frisch2004}. Type schemes are canonical representations of the infinite set of types of $\lambda$-abstraction and they are presented in Section~\ref{sec:type-schemes}. The second origin is due to the presence of structural rules\footnote{In logic, logical rules refer to a particular connective

(here, a type constructor, that is, 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{Intersect}. We handle it in the classic way: we define an algorithmic system that tracks the miminum type (actually, type scheme) of an expression which is obtained from the original system by eliminating the two structural rules and distrubuting checks of the subtyping relation

is possible without making the type empty. To handle this multiplicity

we use the technique of \emph{type schemes} defined

by~\citet{Frisch2004}. Type schemes are canonical representations of

the infinite set of types of $\lambda$-abstraction and they are

presented in Section~\ref{sec:type-schemes}. The second origin is due

to the presence of structural rules\footnote{In logic, logical rules

refer to a particular connective (here, a type constructor, that is,

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{Intersect}. We

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

tracks the miminum type (actually, minimum type scheme) of an

expression which is obtained from the original system by eliminating

the two structural rules and distrubuting checks of the subtyping

relation in the remaining rules. To do that in the presence of

set-theoretic types we need to define some operators on types, given

in section~\ref{sec:typeops}.

For what concerns the use of the auxiliary derivation for the $$

judgments, we present in Section~\ref{sec:typenv} an algorithm that we

prove sound \beppe{and complete?}. All these notions are used in the

algorithmic typing system given in Section~\ref{sec:algorules}.

\begin{enumerate}

\item type of functions -> type schemes

...

...

@@ -477,5 +495,5 @@ change the definition of typeof to take into account type-schemes for lambda abs