{\pvdash\Gamma e t \varpi:t_1 \\\pvdash\Gamma e t \varpi:t_2 }
{\pvdash\Gamma e t \varpi:t_1\land t_2 }
{}
\vspace{-1.2mm}\\
\quad
\Infer[PTypeof]
{\Gamma\vdash\occ e \varpi:t' }
{\pvdash\Gamma e t \varpi:t' }
{}
\qquad
\vspace{-1.2mm}\\
\Infer[PEps]
{}
{\pvdash\Gamma e t \epsilon:t }
{}
\qquad
\vspace{-1.2mm}\\
\Infer[PAppR]
{\pvdash\Gamma e t \varpi.0:\arrow{t_1}{t_2}\\\pvdash\Gamma e t \varpi:t_2'}
{\pvdash\Gamma e t \varpi.1:\neg t_1 }
...
...
@@ -854,7 +853,7 @@ for variables.
The algorithmic system above is sound with respect to the deductive one of Section~\ref{sec:static}
\begin{theorem}[Soundness]
For every $\Gamma$, $e$, $t$, $n_o$, if $\tyof e \Gamma\leq t$, then $\Gamma\vdash e:t$.
For every $\Gamma$, $e$, $t$, $n_o$, if $\Gamma\vdashA e: t$, then $\Gamma\vdash e:t$.
\end{theorem}
We were not able to prove full completeness, just a partial form of it. As
anticipated, the problems are twofold: $(i)$ the recursive nature of
...
...
@@ -872,7 +871,7 @@ types, since, intuitively, it corresponds to typing a language in
which in the types used in dynamic tests, a negated arrow never occurs on the
left-hand side of another negated arrow.
\begin{theorem}[Partial Completeness]
For every $\Gamma$, $e$, $t$, if $\Gamma\vdash e:t$ is derivable by a rank-0 negated derivation, then there exists $n_o$ such that ${\tyof e \Gamma}\leq t$.
For every $\Gamma$, $e$, $t$, if $\Gamma\vdash e:t$ is derivable by a rank-0 negated derivation, then there exists $n_o$ such that $\Gamma\vdashA e: t'$ and $t'\leq t$.
\end{theorem}
\noindent The use of type schemes and of possibly diverging iterations
yield a system that may seem overly complicated. But it is important
@@ -163,7 +163,7 @@ since, \texttt{or\_} has type\\
(\lnot\True\to\lnot\True\to\False)$}
We consider \True, \Any and $\lnot\True$ as candidate types for
\texttt{x} which, in turn allows us to deduce a precise type given in the table. Finally, thanks to this rule it is no longer necessary to use a type case to force refinement. As a consequence we can define the functions \texttt{and\_} and \texttt{xor\_} more naturally as:
\begin{alltt}\color{darkblue}
\begin{alltt}\color{darkblue}\morecompact
let and_ = fun (x : Any) -> fun (y : Any) -> not_ (or_ (not_ x) (not_ y))
let xor_ = fun (x : Any) -> fun (y : Any) -> and_ (or_ x y) (not_ (and_ x y))