Commit 9cd4ebdb authored by Mickael Laurent's avatar Mickael Laurent
Browse files

update algorithmic part

parent 44b5089b
......@@ -233,13 +233,8 @@ We suppose w.l.o.g that all variables abstracted in $\lambda$-abstractions are d
{ }
{ \Gamma \evdash p e t \Gamma }
{ }
\\
\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') }
{ }
\qquad
\Infer[Path(fixpoint)]
\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') }
{ }
......@@ -305,62 +300,110 @@ We suppose w.l.o.g that all variables abstracted in $\lambda$-abstractions are d
\qquad
\end{mathpar}
\subsection{Algorithmic type system (OLD VERSION)}
Let $e$ be an expression, $t$ a type, $\Gamma$ a type environment, $\varpi\in\{0,1\}^*$ and $p\in\{+,-\}$, we define $\typep p \varpi {\Gamma,e,t}$ and $\Gp p {\Gamma,e,t}(\varpi)$ as follows
\\
\mick
{
\subsection{Algorithmic type system}
\[
\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*}
&(\Refine 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.
\end{align*}
\begin{mathpar}
\Infer[EFQ]
{ }
{ \Gamma, (e:\Empty) \vdash e': \Empty }
{ \text{With priority over other rules} }
\\
\Infer[Occ]
{ \Gamma\setminus\{e\} \vdash e : t }
{ \Gamma \vdash e: \Gamma(e) \tsand t }
{ e\in\dom\Gamma}
\qquad
\Infer[Const]
{ }
{\Gamma\vdash c:\basic{c}}
{c\not\in\dom\Gamma}
\\
\Infer[Abs]
{\Gamma,x:s_i\vdash e:\ts_i'\\ \ts_i'\leq t_i}
{
\Gamma\vdash\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]
{
\Gamma \vdash e_1: \ts_1\\
\Gamma \vdash e_2: \ts_2\\
\ts_1 \leq \arrow \Empty \Any\\
\ts_2 \leq \dom {\ts_1}
}
{ \Gamma \vdash {e_1}{e_2}: \ts_1 \circ \ts_2 }
{ {e_1}{e_2}\not\in\dom\Gamma}
\\
\Infer[If]
{\Gamma\vdash e:\ts_0\\
%\makebox{$\begin{array}{l}
% \left\{
% \begin{array}{ll} %\Gamma,
% \Refine + {e,t} \Gamma \vdash e_1 : \ts_1 & \text{ if } \ts_0 \not\leq \neg t\\
% \ts_1 = \Empty & \text{ otherwise}
% \end{array}\right.\\
% \left\{
% \begin{array}{ll} %\Gamma,
% \Refine - {e,t} \Gamma \vdash e_2 : \ts_2 & \text{ if } \ts_0 \not\leq t\\
% \ts_2 = \Empty & \text{ otherwise}
% \end{array}\right.
%\end{array}$}
\Refine + {e,t} \Gamma \vdash e_1 : \ts_1\\
\Refine - {e,t} \Gamma \vdash e_2 : \ts_2}
{\Gamma\vdash \ite {e} t {e_1}{e_2}: \ts_1\tsor \ts_2}
%{\ite {e} t {e_1}{e_2}\not\in\dom\Gamma}
{\texttt{if}\dots\not\in\dom\Gamma}
\\
\Infer[Proj]
{\Gamma \vdash e:\ts\and \ts\leq\pair\Any\Any}
{\Gamma \vdash \pi_i e:\bpi_{\mathbf{i}}(\ts)}
{\pi_i e\not\in\dom\Gamma}
}
\Infer[Pair]
{\Gamma \vdash e_1:\ts_1 \and \Gamma \vdash e_2:\ts_2}
{\Gamma \vdash (e_1,e_2):{\ts_1}\tstimes{\ts_2}}%\pair{t_1}{t_2}}
{(e_1,e_2)\not\in\dom\Gamma}
\end{mathpar}
\[
\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{\tyof{\occ e{\varpi.0}}\Gamma}{\Gp p {\Gamma,e,t} (\varpi)}\\ \\
\Gp p {\Gamma,e,t}(\varpi) &=& \typep p \varpi{\Gamma,e,t} \wedge \tyof {\occ e\varpi}\Gamma\\
\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}
\]
All the functions above are defined iff all their subexpressions are (e.g., $\occ e{\varpi.i}$ must be defined).
Let $\Gamma$ be a type environment and $o$ an occurrence. We denote $\tyof{o}{\Gamma}$ the type that can be deduced for $o$ under the type envirenment $\Gamma$. That is, $\tyof{o}{\Gamma}=t$ if and only if $\Gamma\vdash o:t$ can be deduced by the rules below.\footnote{Note that the definition is well-founded. This can be seen by analyzing the rule \Rule{If}: the definition of $\Gamma^+_{\Gamma,e,t}$ and $\Gamma^-_{\Gamma,e,t}$ 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:t_\circ$ (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 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*}
In what follows we will omit the indexes $e$ and $\Gamma,e,t$ when they are clear from the context.
All the functions above are defined iff all their subexpressions are (e.g., $\occ e{\varpi.i}$ must be defined).
\begin{definition}
Given an expression $e$ and a type $t$ we use $\Gamma^p_{\Gamma,e,t}$ to denote the environment that maps every subterm $e'$ of $e$ such that $\exists \varpi. \occ e\varpi\equiv e'$
to the type $\bigwedge_{\{\varpi\alt \occ e\varpi\equiv e'\}}\Gp p {\Gamma,e,t}(\varpi)$, and is undefined otherwise.
\end{definition}
The reason for the definition above is that the same subterm of $e$
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$.)}
The reason for the definition of $\RefineStep p {e,t}$ is that the same subterm of $e$
may occur several times in $e$ and therefore we can collect for every
occurrence a different type constraint. Since all the constraints must
hold, then we take their intersection. For instance, if $f$ is a function
......@@ -369,117 +412,6 @@ 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$.\\
\mick{
We define the following algorithmic type system. For every (expression, type environment) pair, we can derive an unique type scheme that represents
the set of types that could be derived by a non-deterministic typing system (with subsomption). This set has no smallest type in general (that's why we need to use type schemes).
\begin{mathpar}
\Infer[Occ]
{ \Gamma\setminus\{e\} \vdash e : t }
{ \Gamma \vdash e: \Gamma(e) \tsand t }
{ e\in\dom\Gamma}
\qquad
\Infer[Const]
{ }
{\Gamma\vdash c:\basic{c}}
{c\not\in\dom\Gamma}
\\
\Infer[Abs]
{\Gamma,x:s_i\vdash e:\ts_i'\\ \ts_i'\leq t_i}
{
\Gamma\vdash\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]
{
\Gamma \vdash e_1: \ts_1\\
\Gamma \vdash e_2: \ts_2\\
\ts_1 \leq \arrow \Empty \Any\\
\ts_2 \leq \dom {\ts_1}
}
{ \Gamma \vdash {e_1}{e_2}: \ts_1 \circ \ts_2 }
{ {e_1}{e_2}\not\in\dom\Gamma}
\\
\Infer[If]
{\Gamma\vdash e:\ts_0\\
\makebox{$\begin{array}{l}
\left\{
\begin{array}{ll} %\Gamma,
\Refine + {e,t} \Gamma \vdash e_1 : \ts_1 & \text{ if } \ts_0 \not\leq \neg t\\
\ts_1 = \Empty & \text{ otherwise}
\end{array}\right.\\
\left\{
\begin{array}{ll} %\Gamma,
\Refine - {e,t} \Gamma \vdash e_2 : \ts_2 & \text{ if } \ts_0 \not\leq t\\
\ts_2 = \Empty & \text{ otherwise}
\end{array}\right.
\end{array}$}}
{\Gamma\vdash \ite {e} t {e_1}{e_2}: \ts_1\tsor \ts_2}
%{\ite {e} t {e_1}{e_2}\not\in\dom\Gamma}
{\texttt{if}\dots\not\in\dom\Gamma}
\\
\Infer[Proj]
{\Gamma \vdash e:\ts\and \ts\leq\pair\Any\Any}
{\Gamma \vdash \pi_i e:\bpi_{\mathbf{i}}(\ts)}
{\pi_i e\not\in\dom\Gamma}
\Infer[Pair]
{\Gamma \vdash e_1:\ts_1 \and \Gamma \vdash e_2:\ts_2}
{\Gamma \vdash (e_1,e_2):{\ts_1}\tstimes{\ts_2}}%\pair{t_1}{t_2}}
{(e_1,e_2)\not\in\dom\Gamma}
\end{mathpar}
}
We define the following algorithmic system (we deduce at most one type for every expression, type environment pair, so that $\tyof{}{}$ is defined).
\begin{mathpar}
\Infer[Empty]
{ }
{\Gamma\vdash e:\Empty}
{\exists e' \in \dom\Gamma.\ \Gamma(e') \leq \Empty}
\\
\Infer[Occ]
{
}
{ \Gamma \vdash e: \Gamma(e) }
{ e\in\dom\Gamma}
\qquad
\Infer[Const]
{ }
{\Gamma\vdash c:\basic{c}}
{c\not\in\dom\Gamma}
\\
\Infer[Abs]
{\Gamma,x:s_i\vdash e:t_i'\\t_i'\leq t_i}
{
\Gamma\vdash\lambda^{\wedge_{i\in I}s_i\to t_i}x.e:\textstyle\bigwedge_{i\in I}s_i\to t_i
}
{\lambda^{\wedge_{i\in I}s_i\to t_i}x.e\not\in\dom\Gamma}
\\
\Infer[App]
{
\Gamma \vdash e_1: t_1 \\
\Gamma\vdash e_2: t_2\\
t_1 \leq \Empty \to \Any\\
t_2 \leq \dom {t_1}
}
{ \Gamma \vdash {e_1}{e_2}: t_1 \circ t_2 }
{ {e_1}{e_2}\not\in\dom\Gamma}
\\
\Infer[If]
{\Gamma\vdash e:t_\circ\\
\Gamma, \Gamma^+_{\Gamma,e,t}\vdash e_1 : t_1\\
\Gamma, \Gamma^-_{\Gamma,e,t}\vdash e_2 : t_2}
{\Gamma\vdash \ite {e} t {e_1}{e_2}: t_1\vee t_2}
{\makebox[3cm][l]{$\ite {e} t {e_1}{e_2}\not\in\dom\Gamma$}}
\\\end{mathpar}
The side condition for constants is probably interesting only for functional constants that have union and/or intersection arrow types. Notice that we we can have a more precise typing discipline by not typing a branch whenever the corresponding $\Gamma^p_{\Gamma,e,t}$ maps some expression $e$ into $\Empty$, since this means that the branch could not be selected under the current typing hypotheses.
\subsection{Algorithms}
Define how to compute $t\circ s$ and $\worra t s$
......
......@@ -120,6 +120,7 @@
\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{\cons}[2]{{#1}\textsf{::}{#2}}
\newcommand{\fixpoint}{\textsf{gfp}}
......
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