Commit 7b71a387 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

explanation for most of the algorithm

parent 80e69565
......@@ -299,7 +299,9 @@ e_0e_1& i.\varpi & \occ{e_i}\varpi\qquad i=0,1\\
To ease our analysis we used different directions for each kind of
term. So we have $0$ and $1$ for the function and argument of an
application, $l$ and $r$ for the $l$eft and $r$ight expressions forming a pair,
and $f$ and $s$ for the argument of a $f$irst or of a $s$econd projection.
and $f$ and $s$ for the argument of a $f$irst or of a $s$econd projection. Note also that we do not consider occurrnces
under $\lambda$s (since their type is frozen in their annotations) and type-cases (since they reset the analysis).\beppe{Is it what I wrote here true?}
The judgments $\Gamma \evdash e t \Gamma'$ are then deduced by the following two rules:
\begin{mathpar}
% \Infer[Base]
......@@ -451,7 +453,7 @@ without making the type empty. To handle this multiplicity we use and
extend 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 set of types of $\lambda$-abstractions. The second origin is due
to the presence of structural rules\footnote{In logic, logical rules
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
......@@ -614,44 +616,105 @@ The proof that this type satisfies \eqref{worra} is given in the Appendix~\ref{}
\subsubsection{Type environments for occurrence typing}\label{sec:typenv}
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 enviromnt 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.
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:
\newlength{\sk}
\setlength{\sk}{-1.3pt}
\begin{eqnarray}
\constr\epsilon{\Gamma,e,t} & = & t\\[\sk]\label{uno}
\constr{\varpi.0}{\Gamma,e,t} & = & \neg(\arrow{\env {\Gamma,e,t}{(\varpi.1)}}{\neg \env {\Gamma,e,t} (\varpi)})\\[\sk]\label{due}
\constr{\varpi.1}{\Gamma,e,t} & = & \worra{\tsrep {\tyof{\occ e{\varpi.0}}\Gamma}}{\env {\Gamma,e,t} (\varpi)}\\[\sk]\label{tre}
\constr{\varpi.l}{\Gamma,e,t} & = & \bpl{\env {\Gamma,e,t} (\varpi)}\\[\sk]\label{quattro}
\constr{\varpi.r}{\Gamma,e,t} & = & \bpr{\env {\Gamma,e,t} (\varpi)}\\[\sk]\label{cinque}
\constr{\varpi.f}{\Gamma,e,t} & = & \pair{\env {\Gamma,e,t} (\varpi)}\Any\\[\sk]\label{sei}
\constr{\varpi.s}{\Gamma,e,t} & = & \pair\Any{\env {\Gamma,e,t} (\varpi)}\\[1.5mm]\label{sette}
\env {\Gamma,e,t} (\varpi) & = & \constr \varpi {\Gamma,e,t} \land \tsrep {\tyof {\occ e \varpi} \Gamma}\label{otto}
\end{eqnarray}
\[
\begin{array}{lcl}
\typep+\epsilon{\Gamma,e,t} & = & t\\
\typep-\epsilon{\Gamma,e,t} & = & \neg t\\
\typep{p}{\varpi.0}{\Gamma,e,t} & = & \neg(\arrow{\Gp p{\Gamma,e,t}{(\varpi.1)}}{\neg \Gp p {\Gamma,e,t} (\varpi)})\\
\typep{p}{\varpi.1}{\Gamma,e,t} & = & \worra{\tsrep {\tyof{\occ e{\varpi.0}}\Gamma}}{\Gp p {\Gamma,e,t} (\varpi)}\\
\typep{p}{\varpi.l}{\Gamma,e,t} & = & \bpl{\Gp p {\Gamma,e,t} (\varpi)}\\
\typep{p}{\varpi.r}{\Gamma,e,t} & = & \bpr{\Gp p {\Gamma,e,t} (\varpi)}\\
\typep{p}{\varpi.f}{\Gamma,e,t} & = & \pair{\Gp p {\Gamma,e,t} (\varpi)}\Any\\
\typep{p}{\varpi.s}{\Gamma,e,t} & = & \pair\Any{\Gp p {\Gamma,e,t} (\varpi)}\\ \\
\Gp p {\Gamma,e,t} (\varpi) & = & \typep p \varpi {\Gamma,e,t} \land \tsrep {\tyof {\occ e \varpi} \Gamma}\\
%\underbrace{\land \tyof {\occ e \varpi} {\Gamma\setminus\{\occ e \varpi\}}}_{\text{if $\occ e \varpi$ is not a variable}}}\\
\end{array}
\]
\begin{align*}
&(\RefineStep p {e,t} (\Gamma))(e') =
\left\{\begin{array}{ll}
%\tyof {e'} \Gamma \tsand
\bigwedge_{\{\varpi \alt \occ e \varpi \equiv e'\}}
\Gp p {\Gamma,e,t} (\varpi) & \text{if } \exists \varpi.\ \occ e \varpi \equiv e' \\
\Gamma(e') & \text{otherwise, if } e' \in \dom \Gamma\\
\text{undefined} & \text{otherwise}
\end{array}\right.\\
&\Refine p {e,t} \Gamma=\fixpoint_\Gamma (\RefineStep p {e,t})\qquad \text{(for the order $\leq$ on environments, defined in the proofs section)}
\end{align*}
%% \[
%% \begin{array}{lcl}
%% \typep+\epsilon{\Gamma,e,t} & = & t\\
%% \typep-\epsilon{\Gamma,e,t} & = & \neg t\\
%% \typep{p}{\varpi.0}{\Gamma,e,t} & = & \neg(\arrow{\Gp p{\Gamma,e,t}{(\varpi.1)}}{\neg \Gp p {\Gamma,e,t} (\varpi)})\\
%% \typep{p}{\varpi.1}{\Gamma,e,t} & = & \worra{\tsrep {\tyof{\occ e{\varpi.0}}\Gamma}}{\Gp p {\Gamma,e,t} (\varpi)}\\
%% \typep{p}{\varpi.l}{\Gamma,e,t} & = & \bpl{\Gp p {\Gamma,e,t} (\varpi)}\\
%% \typep{p}{\varpi.r}{\Gamma,e,t} & = & \bpr{\Gp p {\Gamma,e,t} (\varpi)}\\
%% \typep{p}{\varpi.f}{\Gamma,e,t} & = & \pair{\Gp p {\Gamma,e,t} (\varpi)}\Any\\
%% \typep{p}{\varpi.s}{\Gamma,e,t} & = & \pair\Any{\Gp p {\Gamma,e,t} (\varpi)}\\ \\
%% \Gp p {\Gamma,e,t} (\varpi) & = & \typep p \varpi {\Gamma,e,t} \land \tsrep {\tyof {\occ e \varpi} \Gamma}\\
%% %\underbrace{\land \tyof {\occ e \varpi} {\Gamma\setminus\{\occ e \varpi\}}}_{\text{if $\occ e \varpi$ is not a variable}}}\\
%% \end{array}
%% \]
%% \begin{align*}
%% &(\RefineStep p {e,t} (\Gamma))(e') =
%% \left\{\begin{array}{ll}
%% %\tyof {e'} \Gamma \tsand
%% \bigwedge_{\{\varpi \alt \occ e \varpi \equiv e'\}}
%% \Gp p {\Gamma,e,t} (\varpi) & \text{if } \exists \varpi.\ \occ e \varpi \equiv e' \\
%% \Gamma(e') & \text{otherwise, if } e' \in \dom \Gamma\\
%% \text{undefined} & \text{otherwise}
%% \end{array}\right.\\
%% &\Refine p {e,t} \Gamma=\fixpoint_\Gamma (\RefineStep p {e,t})\qquad \text{(for the order $\leq$ on environments, defined in the proofs section)}
%% \end{align*}
All the functions above are defined if and only if so all their subexpressions are (i.e., $\occ e{\varpi.i}$ must be defined).
Each case of the definition of the $\constr{}{}$ function corresponds to the
application of a logical rule (\emph{cf.} Footnote~\ref{fo:rules}) in
the deduction system for $\vdashp$: case \eqref{uno} corresponds
to the application of \Rule{PEps}; case \eqref{due} implements \Rule{Pappl}
straightforwardly; the implementation of rule \Rule{PAppR} is subtler:
instead of finding the best $t_1$ to subtract (by intersection) to the
static type of the argument, \eqref{tre} finds directly this type by
applying the operator $\worra{}{}$ to the static types of the function
and of the application. The remaining (\ref{quattro}--\ref{sette})
cases are the straightforward implementations of the rules
\Rule{PPairL}, \Rule{PPairR}, \Rule{PFst}, and \Rule{PSnd},
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
deduce by the type system of the expression occurring at $\varpi$. The
remaining structural rule, \Rule{Psubs}, is accounted for by the use
of the different operators $\worra{}{}$ and $\boldsymbol{\pi}_i$ in
the definition of $\constr{}{}$.
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}.
That is, $\tyof{e}{\Gamma}=\ts$ if and only if $\Gamma\vdashA e:\ts$ is provable.
\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 remains to explain how to compute the best 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.
All the functions above are defined iff all their subexpressions are (e.g., $\occ e{\varpi.i}$ must be defined).
\beppe{TODO
The notation $\tyof{o}{\Gamma}$ denotes the type that can be deduced for the occurence $o$ under the type envirenment $\Gamma$.
That is, $\tyof{o}{\Gamma}=\ts$ if and only if $\Gamma\vdash o:\ts$ can be deduced by the typing rules.
\footnote{Note that the definition is well-founded.
This can be seen by analyzing the rule \Rule{If}: the definition of $\Refine + {e,t} \Gamma$ and $\Refine - {e,t} \Gamma$ use
$\tyof{\occ e{\varpi}}\Gamma$, and this is defined for all $\varpi$ since the first premisses of \Rule{If} 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$.)}
\begin{align*}
&\RefineStep {e,t} (\Gamma) = \Gamma' \text{ with:}\\
&\dom{\Gamma'}=\dom{\Gamma} \cup \{e' \alt \exists \varpi.\ \occ e \varpi \equiv e'\}\\
&\Gamma'(e') =
\left\{\begin{array}{ll}
%\tyof {e'} \Gamma \tsand
\bigwedge_{\{\varpi \alt \occ e \varpi \equiv e'\}}
\env {\Gamma,e,t} (\varpi) & \text{if } \exists \varpi.\ \occ e \varpi \equiv e' \\
\Gamma(e') & \text{otherwise}
\end{array}\right.\\&\\
&\Refine {e,t} \Gamma={\RefineStep {e,t}}^n(\Gamma)\qquad\text{with $n$ a global parameter}
\end{align*}
The reason for the definition of $\RefineStep p {e,t}$ is that the same subterm of $e$
......@@ -663,34 +726,34 @@ whether $f(x,x)$ is of type $t$ or not, then the test succeed only if $(x,x)$ is
type $s_1\times s_2$, that is, that $x$ has both type $s_1$ and type
$s_2$ and thus their intersection $s_1{\wedge}s_2$.
}
\subsection{Algorithmic typing rules}\label{sec:algorules}
\begin{mathpar}
\Infer[Efq$_{\scriptscriptstyle\mathcal{A}}$]
\Infer[Efq\Aa]
{ }
{ \Gamma, (e:\Empty) \vdashA e': \Empty }
{ \begin{array}{c}\text{\tiny with priority over}\\[-1.8mm]\text{\tiny all the other rules}\end{array}}
\\
\Infer[Env$_{\scriptscriptstyle\mathcal{A}}$]
\Infer[Env\Aa]
{ \Gamma\setminus\{e\} \vdashA e : \ts }
{ \Gamma \vdashA e: \Gamma(e) \tsand \ts }
{ e\in\dom\Gamma}
\qquad
\Infer[Const$_{\scriptscriptstyle\mathcal{A}}$]
\Infer[Const\Aa]
{ }
{\Gamma\vdashA c:\basic{c}}
{c\not\in\dom\Gamma}
\\
\Infer[Abs$_{\scriptscriptstyle\mathcal{A}}$]
\Infer[Abs\Aa]
{\Gamma,x:s_i\vdashA e:\ts_i'\\ \ts_i'\leq t_i}
{
\Gamma\vdashA\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\textstyle\tsfun {\arrow {s_i} {t_i}}_{i\in I}
}
{\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e\not\in\dom\Gamma}
\\
\Infer[App$_{\scriptscriptstyle\mathcal{A}}$]
\Infer[App\Aa]
{
\Gamma \vdashA e_1: \ts_1\\
\Gamma \vdashA e_2: \ts_2\\
......@@ -700,7 +763,7 @@ $s_2$ and thus their intersection $s_1{\wedge}s_2$.
{ \Gamma \vdashA {e_1}{e_2}: \ts_1 \circ \ts_2 }
{ {e_1}{e_2}\not\in\dom\Gamma}
\\
\Infer[Case$_{\scriptscriptstyle\mathcal{A}}$]
\Infer[Case\Aa]
{\Gamma\vdashA e:\ts_0\\
%\makebox{$\begin{array}{l}
% \left\{
......@@ -720,46 +783,16 @@ $s_2$ and thus their intersection $s_1{\wedge}s_2$.
%{\ite {e} t {e_1}{e_2}\not\in\dom\Gamma}
{ \tcase {e} {t\!} {\!e_1\!}{\!e_2}\not\in\dom\Gamma}
\\
\Infer[Proj$_{\scriptscriptstyle\mathcal{A}}$]
\Infer[Proj\Aa]
{\Gamma \vdashA e:\ts\and \ts\leq\pair\Any\Any}
{\Gamma \vdashA \pi_i e:\bpi_{\mathbf{i}}(\ts)}
{\pi_i e\not\in\dom\Gamma}
\Infer[Pair$_{\scriptscriptstyle\mathcal{A}}$]
\Infer[Pair\Aa]
{\Gamma \vdashA e_1:\ts_1 \and \Gamma \vdashA e_2:\ts_2}
{\Gamma \vdashA (e_1,e_2):{\ts_1}\tstimes{\ts_2}}%\pair{t_1}{t_2}}
{(e_1,e_2)\not\in\dom\Gamma}
\end{mathpar}
\mick{
New algorithmic type system below.
TODO: Comments and explanation for the new parameter n.
}
\[
\begin{array}{lcl}
\constr\epsilon{\Gamma,e,t} & = & t\\
\constr{\varpi.0}{\Gamma,e,t} & = & \neg(\arrow{\env {\Gamma,e,t}{(\varpi.1)}}{\neg \env {\Gamma,e,t} (\varpi)})\\
\constr{\varpi.1}{\Gamma,e,t} & = & \worra{\tsrep {\tyof{\occ e{\varpi.0}}\Gamma}}{\env {\Gamma,e,t} (\varpi)}\\
\constr{\varpi.l}{\Gamma,e,t} & = & \bpl{\env {\Gamma,e,t} (\varpi)}\\
\constr{\varpi.r}{\Gamma,e,t} & = & \bpr{\env {\Gamma,e,t} (\varpi)}\\
\constr{\varpi.f}{\Gamma,e,t} & = & \pair{\env {\Gamma,e,t} (\varpi)}\Any\\
\constr{\varpi.s}{\Gamma,e,t} & = & \pair\Any{\env {\Gamma,e,t} (\varpi)}\\ \\
\env {\Gamma,e,t} (\varpi) & = & \constr \varpi {\Gamma,e,t} \land \tsrep {\tyof {\occ e \varpi} \Gamma}\\
%\underbrace{\land \tyof {\occ e \varpi} {\Gamma\setminus\{\occ e \varpi\}}}_{\text{if $\occ e \varpi$ is not a variable}}}\\
\end{array}
\]
\begin{align*}
&\RefineStep {e,t} (\Gamma) = \Gamma' \text{ with:}\\
&\dom{\Gamma'}=\dom{\Gamma} \cup \{e' \alt \exists \varpi.\ \occ e \varpi \equiv e'\}\\
&\Gamma'(e') =
\left\{\begin{array}{ll}
%\tyof {e'} \Gamma \tsand
\bigwedge_{\{\varpi \alt \occ e \varpi \equiv e'\}}
\env {\Gamma,e,t} (\varpi) & \text{if } \exists \varpi.\ \occ e \varpi \equiv e' \\
\Gamma(e') & \text{otherwise}
\end{array}\right.\\&\\
&\Refine {e,t} \Gamma={\RefineStep {e,t}}^n(\Gamma)\qquad\text{with $n$ a global parameter}
\end{align*}
......@@ -122,7 +122,8 @@
\newcommand{\RefineStep}[1]{\textsf{RefineStep}_{#1}}
\newcommand{\constr}[2]{\textsf{Constr}_{#2}(#1)}
\newcommand{\env}[1]{\textsf{Env}_{#1}}
%\newcommand{\env}[1]{\textsf{Env}_{#1}}
\newcommand{\env}[1]{\textsf{Inter}_{#1}}
\newcommand{\cons}[2]{{#1}\textsf{::}{#2}}
\newcommand{\fixpoint}{\textsf{gfp}}
......@@ -163,3 +164,4 @@
\DeclareMathSymbol{\qm}{\mathalpha}{operators}{"3F}
\DeclareMathAlphabet{\mathbbm}{U}{bbold}{m}{n}
\newcommand{\dyn}{\ensuremath{\mathbbm{\qm}}}
\newcommand{\Aa}{\ensuremath{_{\scriptscriptstyle\mathcal{A}}}}
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