Commit 655397e2 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

final touches to section 2

parent bdce70de
......@@ -569,7 +569,7 @@ 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}, together with the description of 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:
\begin{eqnarray}
\dom t & = & \max \{ u \alt t\leq u\to \Any\}
\\[-.5mm]
......@@ -611,9 +611,7 @@ The last step for our presentation is to define the algorithm for the
deduction of $\Gamma \evdash e t \Gamma'$, that is an algorithm that
takes as input $\Gamma$, $e$, and $t$, and returns an environment that
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.
The notation $\tyof{e}{\Gamma}$ denotes the type that can be deduced for the occurence $e$ under the type environment $\Gamma$ in the algorithmic type system given in Section~\ref{sec:algorules}.
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{}{}$:
......@@ -662,8 +660,17 @@ We start by defining the algorithm for each single occurrence, that is for the d
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 (so that all $\tyof {\occ e{\varpi}} \Gamma$ encountered are defined).
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$
in the definition are defined).\footnote{Note that the definition is
well-founded. This can be seen by analyzing the rule
\Rule{Case\Aa}: the definition of $\Refine {e,t} \Gamma$ and
$\Refine {e,\neg t} \Gamma$ use $\tyof{\occ e{\varpi}}\Gamma$, and
this is defined for all $\varpi$ since the first premisses of
\Rule{Case\Aa} states that $\Gamma\vdash e:\ts_0$ (and this is
possible only if we were able to deduce under the hypothesis
$\Gamma$ the type of every occurrence of $e$.)}
Each case of the definition of the $\constrf$ function corresponds to the
application of a logical rule (\emph{cf.} Footnote~\ref{fo:rules}) in
......@@ -681,18 +688,13 @@ respectively.
The other recursive function, $\env{}{}$, implements the two structural
rules \Rule{PInter} and \Rule{PTypeof} by intersecting the type
obtained for $\varpi$ by the logical rules, with the static type
deduced by the type system of the expression occurring at $\varpi$. The
deduced by the type system for the expression occurring at $\varpi$. The
remaining structural rule, \Rule{Psubs}, is accounted for by the use
of the operators $\worra{}{}$ and $\boldsymbol{\pi}_i$ in
the definition of $\constrf$.
\footnote{Note that the definition is well-founded.
This can be seen by analyzing the rule \Rule{Case\Aa}: the definition of $\Refine {e,t} \Gamma$ and $\Refine {e,\neg t} \Gamma$ use
$\tyof{\occ e{\varpi}}\Gamma$, and this is defined for all $\varpi$ since the first premisses of \Rule{Case\Aa} states that
$\Gamma\vdash e:\ts_0$ (and this is possible only if we were able to deduce under the hypothesis $\Gamma$ the type of every occurrence of $e$.)} It extends the corresponding notation we gave for values in Section~\ref{sec:type-schemes}.
It remains to explain how to compute the environment $\Gamma'$ produced from $\Gamma$ by the deduction system for $\Gamma \evdash e t \Gamma'$. Alas, this is the most delicate part of our algorithm.
%
In a nutshell what we want to do is to define a function
$\Refine{\_,\_}{\_}$ that takes a type environment $\Gamma$, an
expression $e$ and a type $t$ and returns the best type environment
......@@ -707,7 +709,7 @@ then the definition of $\Refinef$ would be pretty easy: it must map
each subexpression of $e$ to the intersection of the types deduced by
$\vdashp$ (i.e., by $\env{}{}$) for each of its occurrences. That
is, for each expression $e'$ occurring in $e$, $\Refine {e,t}\Gamma$
is a type environment that maps $e'$ into $\bigwedge_{\{\varpi \alt
would be the type environment that maps $e'$ into $\bigwedge_{\{\varpi \alt
\occ e \varpi \equiv e'\}} \env {\Gamma,e,t} (\varpi)$. As we
explained in Section~\ref{sec:challenges} the intersection is needed
to apply occurrence typing to expression such as
......@@ -719,7 +721,7 @@ the rule \Rule{Path} allows the deduction of the type of some
occurrence $\varpi$ to use a type environment $\Gamma'$ that may
contain information about some suboccurrences of $\varpi$. On the
algorithm this would correspond to apply the $\Refinef$ defined
above to a result of $\Refinef$, and so on. Therefore, ideally our
above to an environment that already is the result of $\Refinef$, and so on. Therefore, ideally our
algorithm should compute the type environment as a fixpoint of the
function $X\mapsto\Refine{e,t}{X}$. Unfortunately, an iteration of $\Refinef$ may
not converge. As an example consider the (dumb) expression $\tcase
......@@ -746,9 +748,8 @@ $\dom{\Refine{e,t}\Gamma} = \dom{\RefineStep {e,t}(\Gamma)} = \dom{\Gamma} \cup
In other terms, we try to find a fixpoint of $\RefineStep{e,t}$ but we
bound our search to $n_o$ iterations. Since $\RefineStep {e,t}$ is
monotone\footnote{\beppe{explain here the order on $\Gamma$.}}, then
every iteration yields a better solution. \beppe{Does it make
sense?}
monotone (w.r.t.\ the subtyping pre-order extended to type environments pointwise), then
every iteration yields a better solution.
While this is unsatisfactory from a formal point of view, in practice
the problem is a very mild one. Divergence may happen only when
......@@ -769,7 +770,7 @@ should be enough to capture all realistic cases \beppe{can we give an estimate
\subsubsection{Algorithmic typing rules}\label{sec:algorules}
We now have all notions needed for our typing algorithm, which is defined by the following rules.
We now have all the notions we need for our typing algorithm, which is defined by the following rules.
\begin{mathpar}
\Infer[Efq\Aa]
{ }
......@@ -841,10 +842,10 @@ 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
used to account the type multiplicity stemming from
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)$
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
......
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