Commit 0b80f66d authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

added reference to completeness corollary

parent 0a76220e
......@@ -873,15 +873,14 @@ 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$.
\end{theorem}
The use of type schemes and the possible non convergence of iterations
The use of type schemes and of possibly non convergencing 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
how close we can get to a complete algorithm for 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
and this in practice never happens (see Footnote~\ref{foo:typecase} and Corollary~\ref{app:completeness}). This is why for our implementation we use the
CDuce library in which type schemes are absent and functions are typed
only by intersections of positive arrows. We present the implementation in Section~\ref{sec:practical}
but before let us study some extensions.
......@@ -14,7 +14,7 @@ we want to type-check in practice. Indeed, if we restrict the language
so that the only functional type $t$ allowed in a test $\ifty{e}t{e_1}{e_2}$
is $\Empty{\to}\Any$---i.e., if we allow to check whether a value is a
function but not whether it has a specific function type (\emph{cf.}, Footnote~\ref{foo:typecase})---, then our
implementation becomes complete.
implementation becomes complete (see Corollary~\ref{app:completeness} in the appendix for a formal proof).
Our implementation is written in OCaml and uses CDuce as a library to
provide the semantic sub-typing machinery. Besides a type-checking
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment