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

add new typing/refinement rules

parent 2b71fee6
......@@ -146,6 +146,50 @@ We use $\Gamma_1,\Gamma_2$ for the type environment obtained by unioning the two
We suppose w.l.o.g that all variables abstracted in $\lambda$-abstractions are distincts (otherwise we can alpha-rename $\lambda$-abstractions).
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
{
\[
\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.\\&\\
&\Gaux {\varnothing} \Gamma = \Gamma\\
&\Gaux {\cons {(e,t)} \tenv} \Gamma = \Gaux \tenv {\Refine p {e,t} \Gamma}\\&\\
&\Genv \tenv \Gamma=\fixpoint_\Gamma (\Gaa \tenv)\qquad \text{(if defined)}
\end{align*}
\begin{align*}
\begin{array}{llclr}
\text{If } e \in \dom \Gamma \text{, } & \tyof x \Gamma &=& \Gamma(x)\\
& \tyof e \Gamma &=& \Gamma(e) \tsand \tyof e {\Gamma\setminus\{e\}}\\
\text{Otherwise,} & \tyof c \Gamma &=& \basic{c}\\
&\tyof {\lambda^{t}x.e} \Gamma &=& t\\
&\tyof {{e_1} {e_2}} \Gamma &=& \apply {\tyof {e_1} \Gamma} {\tyof {e_2} \Gamma} & \text{(if defined)}\\
&\tyof {\pi_i e} \Gamma &=& \bpi_{\mathbf{i}}(\tyof e \Gamma) & \text{(if defined)}\\
&\tyof {(e_1,e_2)} \Gamma &=& \tyof {e_1} \Gamma \tstimes \tyof {e_2} \Gamma\\%\pair{\tyof {e_1} \Gamma}{\tyof {e_2} \Gamma}
&\tyof {e} \Gamma &=& \tsempty & \text{(if other rules do not apply)}
\end{array}
\end{align*}
}
\[
\begin{array}{lcl}
......@@ -175,7 +219,74 @@ hold, then we take their intersection. For instance, if $f$ is a function
of type $(s_1\times s_2\to t)\wedge( s_3\to\neg t)$ and we test
whether $f(x,x)$ is of type $t$ or not, then the test succeed only if $(x,x)$ is of
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$,.
$s_2$ and thus their intersection $s_1{\wedge}s_2$.\\
\mick{
We define the following algorithmic system. For every (expression, type environment, tests environment) triplet, we deduce a type scheme that represents
the set of types that can be derived. This set has no smallest type in general (that's why we can't deduce a type directly without loosing completeness).
\begin{mathpar}
\Infer[Occ]
{
}
{ \tenv,\Gamma \vdash e: \Gamma(e) }
{ e\in\dom\Gamma}
\qquad
\Infer[Const]
{ }
{\tenv,\Gamma\vdash c:\basic{c}}
{c\not\in\dom\Gamma}
\\
\Infer[Abs]
{\tenv,\Gamma,x:s_i\vdash e:\ts_i'\\ \ts_i'\leq t_i}
{
\tenv,\Gamma\vdash\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\textstyle\bigwedge_{i\in I}\arrow {s_i} {t_i}
}
{\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e\not\in\dom\Gamma}
\\
\Infer[App]
{
\tenv,\Gamma \vdash e_1: \ts_1\\
\tenv,\Gamma \vdash e_2: \ts_2\\
\ts_1 \leq \arrow \Empty \Any\\
\ts_2 \leq \dom {\ts_1}
}
{ \tenv,\Gamma \vdash {e_1}{e_2}: \ts_1 \circ \ts_2 }
{ {e_1}{e_2}\not\in\dom\Gamma}
\\
\Infer[If]
{\tenv,\Gamma\vdash e:\ts_0\\
\makebox{$\begin{array}{l}
\left\{
\begin{array}{ll} %\Gamma,
\cons {(e,t,+)} \tenv,\Genv {\cons {(e,t,+)} \tenv} \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,
\cons {(e,t,-)} \tenv,\Genv {\cons {(e,t,-)} \tenv} \Gamma \vdash e_2 : \ts_2 & \text{ if } \ts_0 \not\leq t\\
\ts_2 = \Empty & \text{ otherwise}
\end{array}\right.
\end{array}$}}
{\tenv,\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]
{\tenv,\Gamma \vdash e:\ts\and \ts\leq\pair\Any\Any}
{\tenv,\Gamma \vdash \pi_i e:\bpi_{\mathbf{i}}(\ts)}
{\pi_i e\not\in\dom\Gamma}
\Infer[Pair]
{\tenv,\Gamma \vdash e_1:\ts_1 \and \tenv,\Gamma \vdash e_2:\ts_2}
{\tenv,\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).
......
......@@ -20,6 +20,7 @@
\definecolor{darkred}{rgb}{0.7,0.4,0.4}
\newcommand{\beppe}[1]{{\bf\color{blue}Beppe: #1}}
\newcommand{\mick}[1]{{\bf\color{gray}Mickael: #1}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Support macros
......
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