@@ -10,9 +10,9 @@ In this section we formalize the ideas we outlined in the introduction. We start

\]

and that satisfy the following conditions

\begin{itemize}

\item (regularity) the term has a finite number of different sub-terms;

\item (contractivity) every infinite branch of a type contains an infinite number of occurrences of the

arrow type constructor.

\item (regularity) every term has a finite number of different sub-terms;

\item (contractivity) every infinite branch of a term contains an infinite number of occurrences of the

arrow or product type constructors.

\end{itemize}

\end{definition}

We use the following abbreviations for types: $

...

...

@@ -30,9 +30,9 @@ set).

It also ensures that the binary relation $\vartriangleright

\,\subseteq\!\types^{2}$ defined by $t_1\lor t_2\vartriangleright

t_i$, $t_1\land t_2\vartriangleright

t_i$, $\neg t \vartriangleright t$ is Noetherian.\footnote{In a nutshell, we can do proofs of induction on the structure of unions and negations---and, thus, intersections---but arrows, products, and basic types are the base cases for the induction.}

t_i$, $\neg t \vartriangleright t$ is Noetherian.

This gives an induction principle on $\types$ that we

will use without any further explicit reference to the relation.

will use without any further explicit reference to the relation.\footnote{In a nutshell, we can do proofs by induction on the structure of unions and negations---and, thus, intersections---but arrows, products, and basic types are the base cases for the induction.}

We refer to $ b $, $\times$, and $\to$ as \emph{type constructors}

and to $\lor$, $\land$, $\lnot$, and $\setminus$

as \emph{type connectives}.

...

...

@@ -89,7 +89,7 @@ values.

\subsection{Dynamic semantics}\label{sec:opsem}

The dynamic semantics is defined as a classic left-to-right cbv reduction for a $\lambda$-calculus with pairs enriched with a specific rule for type-cases. We have the following notions of reduction:

The dynamic semantics is defined as a classic left-to-right call-by-value reduction for a $\lambda$-calculus with pairs, enriched with specific rules for type-cases. We have the following notions of reduction:

\[

\begin{array}{rcll}

(\lambda^{\wedge_{i\in I}s_i\to t_i} x.e)v &\reduces& e\subst x v\\

...

...

@@ -100,7 +100,7 @@ The dynamic semantics is defined as a classic left-to-right cbv reduction for a

\]

The semantics of type-cases uses the relation $v\in t$ that we

informally defined in the previous section. We delay its formal

definition to Section~\ref{sec:type-schemes} (it deals with some corner cases for functional values). Context reductions are

definition to Section~\ref{sec:type-schemes} (where it deals with some corner cases for functional values). Context reductions are

\beppe{I have doubt: is this safe or should we play it safer and deduce $t\wedge\neg(t_1\to t_2)$? In other terms is is possible to deduce two separate negation of arrow types that when intersected with the interface are non empty, but by intersecting everything makes the type empty? It should be safe since otherwise intersection would not be admissible in semantic subtyping (see Theorem 6.15 in JACM), but I think we should doube ckeck it.}

As explained in Section~\ref{sec:challenges}, we need to be able to

deduce for, say, the function $\lambda^{\Int\to\Int} x.x$ a type such

as $(\Int\to\Int)\wedge\neg(\Bool\to\Bool)$ (in particular, if this is

To ease our analysis we used different directions for each kind of

term. So we have $0$ and $1$ for the function and argument of an

application, $l$ and $r$ for the $l$eft and $r$ight expressions forming a pair,

and $f$ and $s$ for the argument of a $f$irst or of a $s$econd projection. Note also that we do not consider occurrnces

under $\lambda$s (since their type is frozen in their annotations) and type-cases (since they reset the analysis).\beppe{Is it what I wrote here true?}

and $f$ and $s$ for the argument of a $f$irst or of a $s$econd projection. Note also that we do not consider occurrences

under $\lambda$'s (since their type is frozen in their annotations) and type-cases (since they reset the analysis).\beppe{Is it what I wrote here true?}

The judgments $\Gamma\evdash e t \Gamma'$ are then deduced by the following two rules:

\begin{mathpar}

...

...

@@ -412,7 +414,7 @@ since it states that if an application has type $t_2$ and the argument

of this application has type $t_1$, then the function in this

application cannot have type $t_1\to\neg t_2$. Rules \Rule{PPair\_}

are straightforward since they state that the $i$-th projection of a pair

of type $\pair{t_1}{t_2}$ must be of type $t_i$. So are the last two

that is of type $\pair{t_1}{t_2}$ must be of type $t_i$. So are the last two

rules that essentially state that if $\pi_1 e$ (respectively, $\pi_2

e$) is of type $t'$, then the type of $e$ must be of the form

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

...

...

@@ -573,7 +575,7 @@ denotes functions that will return an integer if applied to an integer,

and will return a Boolean if applied to a Boolean.

It is possible to compute the domain of such a type

(i.e., of the functions of this type), denoted by

\code{\(\texttt{dom}(t)=\Int\vee\Bool\)},

\(\dom{t}=\Int\vee\Bool\),

that is the union of all the possible

input types. But what is the precise return type of such a

function? It depends on what the argument of such a function is:

...

...

@@ -629,7 +631,7 @@ takes as input $\Gamma$, $e$, and $t$, and returns an environment that

extends $\Gamma$ with hypotheses on the occurrences of $e$ that are

the most general that can be deduced by assuming that $e\in t$ succeeds.

We start by defining the algorithm for each single occurrence, that is for the deduction of $\pvdash\Gamma e t \varpi:t'$. This is obtained by defining two mutually recursive functions:

We start by defining the algorithm for each single occurrence, that is for the deduction of $\pvdash\Gamma e t \varpi:t'$. This is obtained by defining two mutually recursive functions$\constrf$ and $\env{}{}$:

\newlength{\sk}

\setlength{\sk}{-1.3pt}

\begin{eqnarray}

...

...

@@ -677,7 +679,7 @@ We start by defining the algorithm for each single occurrence, that is for the d

All the functions above are defined if and only if so all their subexpressions are (i.e., $\occ e{\varpi.i}$ must be defined).

Each case of the definition of the $\constr{}{}$ function corresponds to the

Each case of the definition of the $\constrf$ function corresponds to the

application of a logical rule (\emph{cf.} Footnote~\ref{fo:rules}) in

the deduction system for $\vdashp$: case \eqref{uno} corresponds

to the application of \Rule{PEps}; case \eqref{due} implements \Rule{Pappl}

...

...

@@ -693,18 +695,18 @@ respectively.

The other recursive function, $\env{}{}$, implements the two structural

rules \Rule{PInter} and \Rule{PTypeof} by intersecting the type

obtained for $\varpi$ by the logical rules, with the static type

deduce by the type system of the expression occurring at $\varpi$. The

deduced by the type system of the expression occurring at $\varpi$. The

remaining structural rule, \Rule{Psubs}, is accounted for by the use

of the operators $\worra{}{}$ and $\boldsymbol{\pi}_i$ in

the definition of $\constr{}{}$.

The notation $\tyof{e}{\Gamma}$ denotes the type that can be deduced for the occurence $e$ under the type environment $\Gamma$ in the algorithmic type system given in Section~\ref{sec:algorules}.

That is, $\tyof{e}{\Gamma}=\ts$ if and only if $\Gamma\vdashA e:\ts$ is provable.

That is, $\tyof{e}{\Gamma}=\ts$ if and only if $\Gamma\vdashA e:\ts$ is provable.

\footnote{Note that the definition is well-founded.

This can be seen by analyzing the rule \Rule{Case\Aa}: the definition of $\Refine{e,t}\Gamma$ and $\Refine{e,\neg t}\Gamma$ use

$\tyof{\occ e{\varpi}}\Gamma$, and this is defined for all $\varpi$ since the first premisses of \Rule{Case\Aa} states that

$\Gamma\vdash e:\ts_0$ (and this is possible only if we were able to deduce under the hypothesis $\Gamma$ the type of every occurrence of $e$.)}

$\Gamma\vdash e:\ts_0$ (and this is possible only if we were able to deduce under the hypothesis $\Gamma$ the type of every occurrence of $e$.)} It extends the corresponding notation we gave for values in Section~\ref{sec:type-schemes}.

It remains to explain how to compute the environment $\Gamma'$ produced from $\Gamma$ by the deduction system for $\Gamma\evdash e t \Gamma'$. Alas, this is the most delicate part of our algorithm.

...

...

@@ -738,8 +740,8 @@ above to a result of $\Refinef$, and so on. Therefore, ideally our

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}$: if $x_1:\Any\to\Any$, then every iteration of

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

{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.

The solution we adopt here is to bound the number of iterations to some number $n_o$.

...

...

@@ -755,8 +757,8 @@ From a formal point of view, this means to give up the completeness of the algor

\end{array}\right.

\end{array}

\]

Note in particular that $\Refine{e,t}\Gamma$extends extends $\Gamma$ with hypotheses on the expressions occurring in $e$, since

$\dom{\Refine{e,t}\Gamma}=\dom{\RefineStep{e,t}}(\Gamma)=\dom{\Gamma}\cup\{e' \alt\exists\varpi.\ \occ e \varpi\equiv e'\}$.

Note in particular that $\Refine{e,t}\Gamma$ extends $\Gamma$ with hypotheses on the expressions occurring in $e$, since

$\dom{\Refine{e,t}\Gamma}=\dom{\RefineStep{e,t}(\Gamma)}=\dom{\Gamma}\cup\{e' \alt\exists\varpi.\ \occ e \varpi\equiv e'\}$.

In other terms, we try to find a fixpoint of $\RefineStep{e,t}$ but we

bound our search to $n_o$ iterations. Since $\RefineStep{e,t}$ is

...

...

@@ -774,17 +776,16 @@ type (which is quite rare in practice)\footnote{The only impact of

never happens since programming languages test whether a value

\emph{is} a function, rather than the type of a given function.},

but also we had to build the expression that causes the divergence in

quite an ad hoc way which makes divergence even more unlikely: setting

quite an \emph{ad hoc} way which makes divergence even more unlikely: setting

an $n_o$ twice the depth of the syntax tree of the outermost type case

should capture all realistic cases \beppe{can we give an estimate

based on benchmarking the protottype?}

should be enough to capture all realistic cases \beppe{can we give an estimate