Commit ae31184f authored by Mickael Laurent's avatar Mickael Laurent
Browse files

remove 'p' and fixpoint (iterate instead)

parent 324af6b1
......@@ -358,8 +358,8 @@ positive branch and \Bool{} in the negative one. To obtain that we
have to reiterate the typing of \eqref{nest1} to take into account
that at some point $x$ will get type \Int. To do that, instead of
deducing the type assumptions of the various branches in a top-down
manner, we will obtain them by iteration via a fix-point, and to define it
we introduce in Section~\ref{sec:language} the operator $\Gaux{}{}$
manner, we will obtain them by iteration\dots
\mick{The paragraph above is not up to date.}
Finally, a nested check may help refining the type assumption about some expression. For instance, when typing the positive branch $e$ of
......
......@@ -251,9 +251,9 @@ type-case:\beppe{Changed to \Rule{If} to \Rule{Case}}
\Infer[Case]
{\Gamma\vdash e:t_0\\
%t_0\not\leq \neg t \Rightarrow
\Gamma \evdash + e t \Gamma_1 \\ \Gamma_1 \vdash e_1:t'\\
\Gamma \evdash e t \Gamma_1 \\ \Gamma_1 \vdash e_1:t'\\
%t_0\not\leq t \Rightarrow
\Gamma \evdash - e t \Gamma_2 \\ \Gamma_2 \vdash e_2:t'}
\Gamma \evdash e {\neg t} \Gamma_2 \\ \Gamma_2 \vdash e_2:t'}
{\Gamma\vdash \tcase {e} t {e_1}{e_2}: t'}
{ }
\end{mathpar}
......@@ -261,15 +261,14 @@ The rule \Rule{Case} checks whether the expression $e$, whose type is being test
well-typed and then performs the occurrence typing analysis that produces
the environments $\Gamma_i$'s under whose hypothesis the expressions
$e_i$'s are typed. The production of these environments is represented by the judgment
$\Gamma \evdash p e t \Gamma_i$ (with $p$ either $+$ or $-$). The
intuition is that when $\Gamma \evdash p e t \Gamma_i$ is provable
$\Gamma \evdash e t \Gamma_i$. The
intuition is that when $\Gamma \evdash e t \Gamma_i$ is provable
then $\Gamma_i$ is a version of $\Gamma$ extended with type hypotheses for all
expressions occurring in $e$, type hypotheses that can be deduced
assuming that the test $e\in t$ succeeds (for $p=+$) or fails (for
$p=-$).
assuming that the test $e\in t$ succeeds.
All it remains to do is to show how to deduce judgments of the form
$\Gamma \evdash p e t \Gamma'$. For that we first have to define how
$\Gamma \evdash e t \Gamma'$. For that we first have to define how
to denote occurrences of an expression. These are identified by paths in the
syntax tree of the expressions, that is, by possibly empty strings of
characters denoting directions starting from the root of the tree (we
......@@ -294,7 +293,8 @@ undefined otherwise
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. The judgments $\Gamma \evdash p e t \Gamma'$ are then deduced by the following two rules:
and $f$ and $s$ for the argument of a $f$irst or of a $s$econd projection.
The judgments $\Gamma \evdash e t \Gamma'$ are then deduced by the following two rules:
\begin{mathpar}
% \Infer[Base]
% { \Gamma \vdash e':t' }
......@@ -307,12 +307,12 @@ and $f$ and $s$ for the argument of a $f$irst or of a $s$econd projection. The j
% { }
\Infer[Base]
{ }
{ \Gamma \evdash p e t \Gamma }
{ \Gamma \evdash e t \Gamma }
{ }
\qquad
\Infer[Path]
{ \pvdash {\Gamma'} p e t \varpi:t' \\ \Gamma \evdash p e t \Gamma' }
{ \Gamma \evdash p e t \Gamma',(\occ e \varpi:t') }
{ \pvdash {\Gamma'} e t \varpi:t' \\ \Gamma \evdash e t \Gamma' }
{ \Gamma \evdash e t \Gamma',(\occ e \varpi:t') }
{ }
\end{mathpar}
These rules describe how to produce by occurrence typing the type
......@@ -334,58 +334,54 @@ of rules.
\begin{mathpar}
\Infer[PSubs]
{ \pvdash \Gamma p e t \varpi:t_1 \\ t_1\leq t_2 }
{ \pvdash \Gamma p e t \varpi:t_2 }
{ \pvdash \Gamma e t \varpi:t_1 \\ t_1\leq t_2 }
{ \pvdash \Gamma e t \varpi:t_2 }
{ }
\qquad
\Infer[PIntersect]
{ \pvdash \Gamma p e t \varpi:t_1 \\ \pvdash \Gamma p e t \varpi:t_2 }
{ \pvdash \Gamma p e t \varpi:t_1\land t_2 }
{ \pvdash \Gamma e t \varpi:t_1 \\ \pvdash \Gamma e t \varpi:t_2 }
{ \pvdash \Gamma e t \varpi:t_1\land t_2 }
{ }
\\
\Infer[PTypeof]
{ \Gamma \vdash \occ e \varpi:t' }
{ \pvdash \Gamma p e t \varpi:t' }
{ \pvdash \Gamma e t \varpi:t' }
{ }
\qquad
\Infer[PEps+]
\Infer[PEps]
{ }
{ \pvdash \Gamma + e t \epsilon:t }
{ \pvdash \Gamma e t \epsilon:t }
{ }
\qquad
\Infer[PEps-]
{ }
{ \pvdash \Gamma - e t \epsilon:\neg t }
{ }
\\
\Infer[PAppR]
{ \pvdash \Gamma p e t \varpi.0:\arrow{t_1}{t_2} \\ \pvdash \Gamma p e t \varpi:t_2'}
{ \pvdash \Gamma p e t \varpi.1:\neg t_1 }
{ \pvdash \Gamma e t \varpi.0:\arrow{t_1}{t_2} \\ \pvdash \Gamma e t \varpi:t_2'}
{ \pvdash \Gamma e t \varpi.1:\neg t_1 }
{ t_2\land t_2' \simeq \Empty }
\\
\Infer[PAppL]
{ \pvdash \Gamma p e t \varpi.1:t_1 \\ \pvdash \Gamma p e t \varpi:t_2 }
{ \pvdash \Gamma p e t \varpi.0:\neg (\arrow {t_1} {\neg t_2}) }
{ \pvdash \Gamma e t \varpi.1:t_1 \\ \pvdash \Gamma e t \varpi:t_2 }
{ \pvdash \Gamma e t \varpi.0:\neg (\arrow {t_1} {\neg t_2}) }
{ }
\qquad
\Infer[PPairL]
{ \pvdash \Gamma p e t \varpi:\pair{t_1}{t_2} }
{ \pvdash \Gamma p e t \varpi.l:t_1 }
{ \pvdash \Gamma e t \varpi:\pair{t_1}{t_2} }
{ \pvdash \Gamma e t \varpi.l:t_1 }
{ }
\\
\Infer[PPairR]
{ \pvdash \Gamma p e t \varpi:\pair{t_1}{t_2} }
{ \pvdash \Gamma p e t \varpi.r:t_2 }
{ \pvdash \Gamma e t \varpi:\pair{t_1}{t_2} }
{ \pvdash \Gamma e t \varpi.r:t_2 }
{ }
\qquad
\Infer[PFst]
{ \pvdash \Gamma p e t \varpi:t' }
{ \pvdash \Gamma p e t \varpi.f:\pair {t'} \Any }
{ \pvdash \Gamma e t \varpi:t' }
{ \pvdash \Gamma e t \varpi.f:\pair {t'} \Any }
{ }
\qquad
\Infer[PSnd]
{ \pvdash \Gamma p e t \varpi:t' }
{ \pvdash \Gamma p e t \varpi.s:\pair \Any {t'} }
{ \pvdash \Gamma e t \varpi:t' }
{ \pvdash \Gamma e t \varpi.s:\pair \Any {t'} }
{ }
\qquad
\end{mathpar}
......@@ -396,11 +392,10 @@ the deduction $\vdashp$. The rule \Rule{PIntersect} combined with
\Rule{PTypeof} allows the system to deduce for an occurrence $\varpi$
the intersection of the static type of $\occ e \varpi$ (deduced by
\Rule{PTypeof}) and the type deduced for $\varpi$ by the other $\vdashp$ rules. The
rules \Rule{PEps\,$p$} are the starting points of the analysis: when
rule \Rule{PEps} is the starting point of the analysis: when
checking whether $e$ has type $t$ we can assume that $e$ (\emph{ie},
$\occ e\epsilon$) has type $t$ in the positive branch (rule
\Rule{PEps+}) and type $\neg t$ in the negative branch (rule
\Rule{PEps-}). The rule \Rule{PApprR} implements occurrence typing for
$\occ e\epsilon$) has type $t$.
The rule \Rule{PApprR} implements occurrence typing for
the arguments of applications, since it states that if a function maps
arguments of type $t_1$ in results of type $t_2$ and an application of
this function yields results (in $t'_2$) that cannot be in $t_2$
......@@ -592,9 +587,8 @@ In the example with \code{\(t=(\Int \to \Int)\) \(\wedge\) \((\Bool \to \Bool)\)
\\
\apply t s & = &\min \{ u \alt t\leq s\to u\}
\\
\worra t s & = &\min\{u\leq \dom t\alt t\circ(\dom t\setminus u)\leq \neg s\}\label{worra}
\worra t s = \min\{u \alt t\circ(\dom t\setminus u)\leq \neg s\}\label{worra}
\end{eqnarray}
\beppe{Wouldn't $\worra t s = \min\{u \alt t\circ(\dom t\setminus u)\leq \neg s\}$ be enough?}
The first two operators belongs to the theory of semantic subtyping while the last one is new and we described it in Section~\ref{sec:ideas}
......@@ -674,7 +668,7 @@ $s_2$ and thus their intersection $s_1{\wedge}s_2$.
{ \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]
\Infer[Env$_{\scriptscriptstyle\mathcal{A}}$]
{ \Gamma\setminus\{e\} \vdashA e : \ts }
{ \Gamma \vdashA e: \Gamma(e) \tsand \ts }
{ e\in\dom\Gamma}
......@@ -715,8 +709,8 @@ $s_2$ and thus their intersection $s_1{\wedge}s_2$.
% \ts_2 = \Empty & \text{ otherwise}
% \end{array}\right.
%\end{array}$}
\Refine + {e,t} \Gamma \vdashA e_1 : \ts_1\\
\Refine - {e,t} \Gamma \vdashA e_2 : \ts_2}
\Refine {e,t} \Gamma \vdashA e_1 : \ts_1\\
\Refine {e,\neg t} \Gamma \vdashA e_2 : \ts_2}
{\Gamma\vdashA \tcase {e} t {e_1}{e_2}: \ts_1\tsor \ts_2}
%{\ite {e} t {e_1}{e_2}\not\in\dom\Gamma}
{ \tcase {e} {t\!} {\!e_1\!}{\!e_2}\not\in\dom\Gamma}
......@@ -730,4 +724,37 @@ $s_2$ and thus their intersection $s_1{\wedge}s_2$.
{\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*}
......@@ -118,12 +118,11 @@
\newcommand{\Odd} {\textsf{Odd}}
\newcommand{\subst}[2]{\{#1 \mapsto #2\}}
\newcommand{\Genv}[2]{\textsf{Gamma}_{#1}(#2)}
\newcommand{\Ga}[1]{\textsf{Gamma}_{#1}}
\newcommand{\Gaux}[2]{\textsf{Aux}_{#1}(#2)}
\newcommand{\Gaa}[1]{\textsf{Aux}_{#1}}
\newcommand{\Refine}[3]{\textsf{Refine}^{#1}_{#2}(#3)}
\newcommand{\RefineStep}[2]{\textsf{RefineStep}^{#1}_{#2}}
\newcommand{\Refine}[2]{\textsf{Refine}_{#1}(#2)}
\newcommand{\RefineStep}[1]{\textsf{RefineStep}_{#1}}
\newcommand{\constr}[2]{\textsf{Constr}_{#2}(#1)}
\newcommand{\env}[1]{\textsf{Env}_{#1}}
\newcommand{\cons}[2]{{#1}\textsf{::}{#2}}
\newcommand{\fixpoint}{\textsf{gfp}}
......@@ -158,8 +157,8 @@
\newcommand{\vdashA}{\vdash_{\!\scriptscriptstyle\mathcal{A}}}
\newcommand{\vdashp}{\vdash^{\texttt{Path}}}
\newcommand{\pvdash}[4]{\vdashp_{#1,#3,#4,#2}}%\mathcal{P}
\newcommand{\evdash}[3]{\vdash^{\texttt{Env}}_{#2,#3,#1}}
\newcommand{\pvdash}[3]{\vdashp_{#1,#2,#3}}%\mathcal{P}
\newcommand{\evdash}[2]{\vdash^{\texttt{Env}}_{#1,#2}}
\DeclareMathSymbol{\qm}{\mathalpha}{operators}{"3F}
\DeclareMathAlphabet{\mathbbm}{U}{bbold}{m}{n}
......
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