Commit 8907c4dc authored by Mickael Laurent's avatar Mickael Laurent
Browse files

new simpler type system

parent 34d69b94
\subsection{Types}
\begin{definition}[Type syntax]\label{def:types} The set of types are the terms $t$ coinductively produced by the following grammr
\begin{definition}[Type syntax]\label{def:types} The set of types are the terms $t$ coinductively produced by the following grammar
\[
\begin{array}{lrcl}
\textbf{Types} & t & ::= & b\alt t\to t\alt t\vee t \alt \neg t \alt \Empty
......@@ -170,23 +170,7 @@ Let $e$ be an expression, $t$ a type, $\Gamma$ a type environment, $\varpi\in\{0
\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,p)} \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^{\bigwedge_{i\in I} \arrow {s_i} {t_i}}x.e} \Gamma &=& \tsfun {\arrow {s_i} {t_i}}_{i\in I}\\
&\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 no other rule applies)}
\end{array}
\end{array}\right.
\end{align*}
}
......@@ -224,67 +208,63 @@ $s_2$ and thus their intersection $s_1{\wedge}s_2$.\\
\mick{
We define the following algorithmic type system. For every (expression, type environment, tests environment) triplet, 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).
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]
{
}
{ \tenv,\Gamma \vdash e: \Gamma(e) }
{ \Gamma\setminus\{e\} \vdash e : t }
{ \Gamma \vdash e: \Gamma(e) \tsand t }
{ e\in\dom\Gamma}
\qquad
\Infer[Const]
{ }
{\tenv,\Gamma\vdash c:\basic{c}}
{\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}
{\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\tsfun {\arrow {s_i} {t_i}}_{i\in 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]
{
\tenv,\Gamma \vdash e_1: \ts_1\\
\tenv,\Gamma \vdash e_2: \ts_2\\
\Gamma \vdash e_1: \ts_1\\
\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 }
{ \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\\
{\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\\
\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,
\cons {(e,t,-)} \tenv,\Genv {\cons {(e,t,-)} \tenv} \Gamma \vdash e_2 : \ts_2 & \text{ if } \ts_0 \not\leq t\\
\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}$}}
{\tenv,\Gamma\vdash \ite {e} t {e_1}{e_2}: \ts_1\tsor \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]
{\tenv,\Gamma \vdash e:\ts\and \ts\leq\pair\Any\Any}
{\tenv,\Gamma \vdash \pi_i e:\bpi_{\mathbf{i}}(\ts)}
{\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]
{\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}}
{\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}
......
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