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

trying some new rules... (wip)

parent 2a39f248
......@@ -350,4 +350,9 @@ The authors thank Paul-André Melliès for his help on type ranking.
\section{Full new system with normal form}
\input{new_system}
\newpage
\section{Full new system with normal form (experimentation)}
\input{new_system2}
\end{document}
......@@ -184,7 +184,7 @@ TODO: Algorithmic rules
let y = x in
let z = if y is True then (fun (z:True) -> true) else (fun (z:False) -> false)
in z x
\end{lstlisting}
\end{lstlisting}\vspace{1em}
The typing rules should return a list of pair (type, environments) in order to be
as precise as possible (= remember correlations). When typing a let, the candidates of $e_2$
......
\subsection{Syntax}
\[
\begin{array}{lrcl}
\textbf{Types} & t & ::= & b\alt t\to t\alt t\times t\alt t\vee t \alt \neg t \alt \Empty
\end{array}
\]
\begin{equation}\label{expressions2}
\begin{array}{lrclr}
\textbf{Atomic Expr} &a &::=& c\alt x\alt\lambda x:t.e\alt (a,a)\\[.3mm]
\textbf{U-Expr} &u &::=& a a\alt \tcase{x}{t}{e}{e}\alt \pi_i a\\[.3mm]
\textbf{P-Expr} &p &::=& u\alt a\\[.3mm]
\textbf{Expressions} &e &::=& \letexp{x}{p}{e}\alt p \\[.3mm]
\textbf{Values} &v &::=& c\alt\lambda x:t.e\alt (v,v)\\
\end{array}
\end{equation}
TODO: the then and else expressions of typecases have no associated variable,
altough the env refinement rules could refine their types...
Is this an issue? Should we require an atomic in the then and else branchs
(seems difficult: there would be no equivalent normal form)?
TODO: Which restrictions on types? (cannot test a precise arrow type, etc)
\subsection{Typing rules}
\begin{mathpar}
\Infer[Const]
{ }
{\Gamma\vdash c:\basic{c}}
{ }
\quad
\Infer[Var]
{ }
{ \Gamma \vdash x: \Gamma(x) }
{ x\in\dom\Gamma }
% \qquad
% \Infer[Inter]
% { \Gamma \vdash e:t_1\\\Gamma \vdash e:t_2 }
% { \Gamma \vdash e: t_1 \wedge t_2 }
% { }
\qquad
\Infer[Subs]
{ \Gamma \vdash e:t\\t\leq t' }
{ \Gamma \vdash e: t' }
{ }
\\
\Infer[Efq]
{ \exists x\in\dom{\Gamma}.\ \Gamma(x)=\Empty }
{ \Gamma \vdash e: t }
{ }
\qquad
\Infer[Proj]
{\Gamma \vdash a:\pair{t_1}{t_2}}
{\Gamma \vdash \pi_i a:t_i}
{ }
\qquad
\Infer[Pair]
{\Gamma \vdash a_1:t_1 \and \Gamma \vdash a_2:t_2}
{\Gamma \vdash (a_1,a_2):\pair {t_1} {t_2}}
{ }
\\
\Infer[App]
{
\Gamma \vdash a_1: \arrow {t_1}{t_2}\quad
\Gamma \vdash a_2: t_1
}
{ \Gamma \vdash {a_1}{a_2}: t_2 }
{ }
\qquad
\Infer[Split]
{
\Gamma,(x:t_1) \vdash e: t\quad
\Gamma,(x:t_2) \vdash e: t
}
{ \Gamma,(x:t_1\lor t_2) \vdash e: t }
{ }
\\
\Infer[Case]
{
x\in\dom\Gamma\\
\Gamma\subst{x}{\Gamma(x)\land t} \vdash e_1:t'\\
\Gamma\subst{x}{\Gamma(x)\land \neg t} \vdash e_2:t'}
{\Gamma\vdash \tcase {x} t {e_1}{e_2}: t'}
{ }
\\
\Infer[Abs]
{\Gamma,(x:s)\vdash e\triangleright_x \dt\\
\textstyle {\dt'=\dt\cup\left\{s\setminus\bigcup_{s'\in\dt}s'\right\}}\\
T=\{(s',t')\,|\,s'\in\dt' \text{ and } \Gamma,(x:s')\vdash e:t'\}}
{
\Gamma\vdash\lambda x:s.e:\textstyle \bigwedge_{(s',t')\in T}\arrow {s'} {t'}
}
{ }
\\
\Infer[Let]
{
\Gamma\bvdash{p}{u} (\Gamma_u^i)_{i\in I_u}\\
\forall i\in I_u.\ \Gamma_u^i,(x:u)\vdash e:t}
{
\Gamma\vdash_{u}\letexp x p e : t
}
{ }
\\
\Infer[LetSplit]
{
\Gamma,(x:t')\vdash e\triangleright_x\dt\\
\forall u\in \dt.\ \Gamma\vdash_{u}\letexp x p e : t}
{
\Gamma\vdash_{t'}\letexp x p e : t
}
{ }
\\
\Infer[Let]
{\Gamma\vdash p:t'\\
\Gamma\vdash_{t'}\letexp x p e : t}
{
\Gamma\vdash\letexp x p e : t
}
{ }
\end{mathpar}
TODO: Inter rule needed?
TODO: Algorithmic rules
NOTE: In the algorithmic system, the Split rule can be guaranteed by stronger
typing rules for the application and the typecase: it should return a list of
pair (typ, env). It allows us to consider the two possibilities of a typecase
without making any approximation (and similarly for the application of a union of arrows).
\subsection{Candidates generation rules}
\begin{mathpar}
\Infer[Var]
{
}
{ \Gamma \vdash y \triangleright_x \varnothing }
{}
\hfill
\Infer[Const]
{
}
{ \Gamma \vdash c \triangleright_x \varnothing }
{}
\hfill
\Infer[Abs]
{\Gamma,(y:s)\vdash e\triangleright_x\dt}
{
\Gamma\vdash\lambda y:s.\ e\triangleright_x\dt
}
{x\neq y}
\vspace{-2.3mm}\\
\Infer[Pair]
{\Gamma \vdash a_1\triangleright_x\dt_1 \and \Gamma \vdash a_2\triangleright_x\dt_2}
{\Gamma \vdash (a_1,a_2)\triangleright_x\dt_1\cup\dt_2}
{}
\hfill
\Infer[Proj]
{\Gamma \vdash a\triangleright_x\dt}
{\Gamma \vdash \pi_i a\triangleright_x\dt}
{}
\vspace{-2.3mm}\\
\Infer[Case]
{\Gamma\subst{y}{\Gamma(y)\land t}\vdash e_1\triangleright_x\dt_1\\
\Gamma\subst{y}{\Gamma(y)\land \neg t}\vdash e_2\triangleright_x\dt_2}
{\Gamma\vdash \tcase{y}{t}{e_1}{e_2}\triangleright_x\dt_1\cup\dt_2\cup
\left\{
\begin{array}{l}
\{\Gamma(x)\land t,\Gamma(x)\land\neg t\} \text{ if } y=x\arcr
\varnothing\text{ otherwise}
\end{array}
\right.}
{}
\vspace{-2.3mm}\\
\Infer[App]
{
\Gamma \vdash a_1 : \textstyle{\bigvee \bigwedge_{i \in I}s_i\to t_i}\\
\Gamma \vdash a_1\triangleright_x\dt_1\\
\forall i\in I.\ \Gamma\fvdash{a_2}{s_i}\{\Gamma_i^j\}_{j\in J_i}
}
{ \Gamma \vdash a_1 a_2\triangleright_x\dt_1\cup\textstyle{\bigcup_{i\in I}
\bigcup_{j\in J_i}\{\Gamma_i^j(x)\}} }
{}
\vspace{-2.3mm}\\
\Infer[Let]
{
\Gamma \vdash p: t\\
\Gamma, (y:t) \vdash e\triangleright_x\dt_x\\
\Gamma, (y:t) \vdash e\triangleright_y\dt_y\\
\forall u\in \dt_y.\ \Gamma\fvdash{p}{u}\{\Gamma_u^i\}_{i\in I_u}
}
{ \Gamma \vdash\letexp{y}{p}{e}\triangleright_x\dt_x\cup\textstyle{
\bigcup_{u\in \dt_y}\bigcup_{i\in I_u}\{\Gamma_u^i(x)\}
}}
{}
\end{mathpar}
TODO: example: application $x y$ with $x$ an union of arrow. Candidates
for $x$ should be all the different union of arrows of its type?
TODO: Candidates for a variable should be a special "all splits".
Otherwise, $\letexp{x}{\cdots}{x}$ will never be splitted.
TODO: Candidates should always be a partition of the initial type of $x$
\subsection{Forward refinement rules}
\subsection{Backward refinement rules}
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