Commit 868ae1e4 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

started removing type schemes

parent df8d886d
......@@ -9,28 +9,37 @@ types for the same well-typed expression and $(ii)$~how to compute the
auxiliary deduction system for paths.
Multiple types have two distinct origins each requiring a distinct
technical solution. The first origin is the rule \Rule{Abs-} by which
it is possible to deduce for every well-typed lambda abstraction
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 and
adapt the technique of \emph{type schemes} defined
by~\citet{Frisch2008}. Type schemes---whose definition we recall in Section~\ref{sec:type-schemes}---are canonical representations of
the infinite sets of types of $\lambda$-abstractions. The second origin is due
to the presence of structural rules\footnote{\label{fo:rules}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{Inter}. We
handle this presence in the classic way: we define an algorithmic system that
tracks the miminum type---actually, the minimum \emph{type scheme}---of an
expression; this system is obtained from the original system by removing
the two structural rules and by distributing suitable 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, which are given
in Section~\ref{sec:typeops}.
technical solution. The first origin is the presence of structural
rules\footnote{\label{fo:rules}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{Inter}. We handle this presence
in the classic way: we define an algorithmic system that tracks the
miminum type of an expression; this system is obtained from the
original system by removing the two structural rules and by
distributing suitable 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, which are given in
Section~\ref{sec:typeops}. The second origin is the rule \Rule{Abs-}
by which it is possible to deduce for every well-typed lambda
abstraction infinitely many types, that is the annotation of the
function intersected with as many negations of arrow types as
possible without making the type empty. We do not handle this
multiplicity directly in the algorithmic system but only in the proof
its soundness by using and adapting the technique of \emph{type
schemes} defined by~\citet{Frisch2008}. Type schemes are canonical
representations of the infinite sets of types of
$\lambda$-abstractions which can be used to define an algorithmic
system that can be easily proved to be sound. The simpler algorithm
that we propose in this section implies the one with type schemes (cf
Theorem~\ref{????}) and it is thus sound, too. The algorithm of this
section is not only simpler but, as we discuss in Section~\ref{???},
is also the one that should be used in practice. This is why we preferred to
present it here and relegate the presentation of type schemes to
Appendix~\ref{???}.
For what concerns the use of the auxiliary derivation for the $ $
For what concerns the use of the auxiliary derivation for the $\Gamma \evdash e t \Gamma' $ and $\pvdash \Gamma e t \varpi:t'$
judgments, we present in Section~\ref{sec:typenv} an algorithm that is sound and satisfies a limited form of
completeness. All these notions are then used in the algorithmic typing
system given in Section~\ref{sec:algorules}.
......
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