Commit c6eda8ea authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

added comment on the new [Var] Rule

parent 2ec5e187
......@@ -801,7 +801,7 @@ We now have all notions needed for our typing algorithm, which is defined by th
\Infer[Env\Aa]
{ \Gamma\setminus\{e\} \vdashA e : \ts }
{ \Gamma \vdashA e: \Gamma(e) \tsand \ts }
{ e\in\dom\Gamma \text{ and } e \text{ not a variable}}
{ \begin{array}{c}e\in\dom\Gamma \text{ and }\\[-1mm] e \text{ not a variable}\end{array}}
\qquad
\Infer[Const\Aa]
{ }
......@@ -858,25 +858,29 @@ We now have all notions needed for our typing algorithm, which is defined by th
The side conditions of the rules ensure that the system is syntax
directed, that is, that at most one rule applies when typing a term:
priority is given to \Rule{Eqf\Aa} over all the other rules and to
\Rule{Env\Aa} over all remaining (logical) rules. Type schemes are
\Rule{Env\Aa} over all remaining logical rules. Type schemes are
used to account the type multiplicity stemming from
$\lambda$-abstractions as shown in particular by rule \Rule{Abs\Aa}
(in what follows we use the word ``type'' also for type schemes). The
subsumption rule is no longer in the system. It is replaced by: $(i)$
using a union type in \Rule{Case\Aa}, $(ii)$ checking in \Rule{Abs\Aa}
that the body of the function is typed by a subtype of the type declared
in the annotation, and $(iii)$ using type operators and checking subtyping
in the elimination rules \Rule{App\Aa,Proj\Aa}. In particular, for
\Rule{App\Aa} notice that it checks that the type of the function is a
functional type, that the type of the argument is a subtype of the
domain of the function, and then returns the result type of the application
of the two types. The intersection rule is replaced by the use of type
schemes in \Rule{Abs\Aa} and by the rule \Rule{Env\Aa}. The latter
intersects the type deduced for an expression $e$ by occurrence typing
and stored in $\Gamma$ with the type deduced for $e$ by the logical
rules: this is simply obtained by removing any hypothesis about $e$
from $\Gamma$, so that the deduction of the type $\ts$ for $e$ cannot
but end by a logical rule.
that the body of the function is typed by a subtype of the type
declared in the annotation, and $(iii)$ using type operators and
checking subtyping in the elimination rules \Rule{App\Aa,Proj\Aa}. In
particular, for \Rule{App\Aa} notice that it checks that the type of
the function is a functional type, that the type of the argument is a
subtype of the domain of the function, and then returns the result
type of the application of the two types. The intersection rule is
replaced by the use of type schemes in \Rule{Abs\Aa} and by the rule
\Rule{Env\Aa}. The latter intersects the type deduced for an
expression $e$ by occurrence typing and stored in $\Gamma$ with the
type deduced for $e$ by the logical rules: this is simply obtained by
removing any hypothesis about $e$ from $\Gamma$, so that the deduction
of the type $\ts$ for $e$ cannot but end by a logical rule. Of course
this does not apply when the expression $e$ is a variable, since
an hypothesis in $\Gamma$ is the only way to deduce the type of a
variable, which is a why the algorithm reintroduces the classic rules
for variables.
The system above satisfies the following properties:\beppe{State here
soundness and partial completeness}
......
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