In this section we formalize the ideas we outlined in the introduction. We start by the definition of types followed by the language and its reduction semantics. The static semantics is the core of our work: we first present a declarative type system that deduces (possibly many) types for well-typed expressions and then the algorithms to decide whether an expression is well typed or not.

\subsection{Types}

...

...

@@ -293,7 +293,7 @@ root of the tree).

Let $e$ be an expression and $\varpi\in\{0,1,l,r,f,s\}^*$ a

\emph{path}; we denote $\occ e\varpi$ the occurrence of $e$ reached by

the path $\varpi$, that is (for $i=1,2$, and undefined otherwise)

the path $\varpi$, that is (for $i=1,2$, and undefined otherwise)\vspace{-1mm}

%% \[

%% \begin{array}{l}

%% \begin{array}{r@{\downarrow}l@{\quad=\quad}l}

...

...

@@ -311,7 +311,7 @@ the path $\varpi$, that is (for $i=1,2$, and undefined otherwise)

We introduce the new syntactic category of \emph{types schemes} which are the terms~$\ts$ inductively produced by the following grammar.

\[

\begin{array}{lrcl}

\textbf{Type schemes}&\ts& ::=& t \alt\tsfun{\arrow t t ; \cdots ; \arrow t t}\alt\ts\tstimes\ts\alt\ts\tsor\ts\alt\tsempty

...

...

@@ -578,14 +577,14 @@ things are more difficult since a function can be typed by, say, a

union of intersection of arrows and negations of types. Checking that

the function has a functional type is easy since it corresponds to

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:

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:\vspace{-2mm}

\begin{eqnarray}

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

\\[-.8mm]

\\[-1mm]

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

\\[-.8mm]

\\[-1mm]

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

\end{eqnarray}

\end{eqnarray}\vspace{-6mm}\\

%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

...

...

@@ -594,12 +593,12 @@ 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:

then we define:\vspace{-1.2mm}

\begin{equation}

\begin{array}{lcrlcr}

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

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

\end{array}

\end{array}\vspace{-1.2mm}

\end{equation}

All the operators above but $\worra{}{}$ are already present in the

theory of semantic subtyping: the reader can find how to compute them

...

...

@@ -612,10 +611,10 @@ furthermore $t\leq\Empty\to\Any$, then $t \simeq \bigvee_{i\in

N_i}\neg(s_n'\to t_n')\right)$ with $\bigwedge_{p\in P_i}(s_p\to

t_p)\bigwedge_{n\in N_i}\neg(s_n'\to t_n')\not\simeq\Empty$ for all

$i$ in $I$. For such a $t$ and any type $s$ then we have:

$i$ in $I$. For such a $t$ and any type $s$ then we have:\vspace{-1.7mm}

%

\begin{equation}

\worra t s = \dom t \wedge\bigvee_{i\in I}\left(\bigwedge_{\{P\subseteq P_i\alt s\leq\bigvee_{p \in P}\neg t_p\}}\left(\bigvee_{p \in P}\neg s_p\right) \right)

\worra t s = \dom t \wedge\bigvee_{i\in I}\left(\bigwedge_{\{P\subseteq P_i\alt s\leq\bigvee_{p \in P}\neg t_p\}}\left(\bigvee_{p \in P}\neg s_p\right) \right)\vspace{-1.7mm}

\end{equation}

The formula considers only the positive arrows of each summand that

forms $t$ and states that, for each summand, whenever you take a subset

...

...

@@ -637,7 +636,7 @@ 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. For that we need the notation $\tyof{e}{\Gamma}$ which denotes the type scheme deduced for $e$ under the type environment $\Gamma$ in the algorithmic type system of Section~\ref{sec:algorules}.

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

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{}{}$:

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{}{}$:\vspace{-1.7mm}

\env{\Gamma,e,t} (\varpi) & = &\constr\varpi{\Gamma,e,t}\land\tsrep{\tyof{\occ e \varpi}\Gamma}\label{otto}

\end{eqnarray}

\end{eqnarray}\vspace{-5.2mm}\\

All the functions above are defined if and only if the initial path

$\varpi$ is valid for $e$ (i.e., $\occ e{\varpi}$ is defined) and $e$

is well-typed (which implies that all $\tyof{\occ e{\varpi}}\Gamma$

...

...

@@ -718,7 +717,7 @@ $\Refinef$ yields for $x_1$ a type strictly more precise than the type deduced i

previous iteration.

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

From a formal point of view, this means to give up the completeness of the algorithm: $\Refinef$ will be complete (i.e., it will find all solutions) for the deductions of $\Gamma\evdash e t \Gamma'$ of depth at most $n_o$. This is obtained by the following definition of $\Refinef$

From a formal point of view, this means to give up the completeness of the algorithm: $\Refinef$ will be complete (i.e., it will find all solutions) for the deductions of $\Gamma\evdash e t \Gamma'$ of depth at most $n_o$. This is obtained by the following definition of $\Refinef$\vspace{-2mm}

\[

\begin{array}{rcl}

\Refinef_{e,t}\eqdef(\RefineStep{e,t})^{n_o}\\

...

...

@@ -729,7 +728,7 @@ From a formal point of view, this means to give up the completeness of the algor

\Gamma(e')&\text{otherwise, if } e'\in\dom\Gamma\\

\text{undefined}&\text{otherwise}

\end{array}\right.

\end{array}

\end{array}\vspace{-1.5mm}

\]

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'\}$.