Commit 04bc435d authored by Mickael Laurent's avatar Mickael Laurent
Browse files

Add declarative type system

parent 8907c4dc
......@@ -142,7 +142,166 @@ It is necessary to map alpha-equivalent expressions to the same type in order fo
We use $\Gamma_1,\Gamma_2$ for the type environment obtained by unioning the two type environments giving priority to $\Gamma_2$ (define formally).
We suppose w.l.o.g that all variables abstracted in $\lambda$-abstractions are distincts (otherwise we can alpha-rename $\lambda$-abstractions).
We suppose w.l.o.g that all variables abstracted in $\lambda$-abstractions are distincts (otherwise we can alpha-rename $\lambda$-abstractions).
\subsection{Declarative type system}
\begin{mathpar}
\Infer[Occ]
{ }
{ \Gamma \vdash e: \Gamma(e) }
{ e\in\dom\Gamma }
\qquad
\Infer[Intersect]
{ \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' }
{ }
\qquad
\\
\Infer[EFQ]
{ }
{ \Gamma, (e:\Empty) \vdash e': t }
{ }
\qquad
\Infer[Const]
{ }
{\Gamma\vdash c:\basic{c}}
{ }
\qquad
\Infer[App]
{
\Gamma \vdash e_1: \arrow {t_1}{t_2}\\
\Gamma \vdash e_2: t_1
}
{ \Gamma \vdash {e_1}{e_2}: t_2 }
{ }
\\
\Infer[Abs]
{\Gamma,x:s_i\vdash e:t_i\\t\simeq \left(\bigwedge_{i\in I} \arrow {s_i} {t_i}\right)
\land \left(\bigwedge_{j\in J} \neg (\arrow {s'_j} {t'_j})\right)\\t\not\simeq\Empty}
{
\Gamma\vdash\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\textstyle t
}
{ }
\\
% \Infer[If]
% {\Gamma\vdash e:t_0\\
% %t_0\not\leq \neg t \Rightarrow
% \Gamma \cvdash + e t e_1:t'\\
% %t_0\not\leq t \Rightarrow
% \Gamma \cvdash - e t e_2:t'}
% {\Gamma\vdash \ite {e} t {e_1}{e_2}: t'}
% { }
\Infer[If]
{\Gamma\vdash e:t_0\\
%t_0\not\leq \neg t \Rightarrow
\Gamma \evdash + e t \Gamma^+ \\ \Gamma^+ \vdash e_1:t'\\
%t_0\not\leq t \Rightarrow
\Gamma \evdash - e t \Gamma^- \\ \Gamma^- \vdash e_2:t'}
{\Gamma\vdash \ite {e} t {e_1}{e_2}: t'}
{ }
\\
\Infer[Proj]
{\Gamma \vdash e:(t_1,t_2)}
{\Gamma \vdash \pi_i e:t_i}
{ }
\qquad
\Infer[Pair]
{\Gamma \vdash e_1:t_1 \and \Gamma \vdash e_2:t_2}
{\Gamma \vdash (e_1,e_2):\pair {t_1} {t_2}}
{ }
\end{mathpar}
\begin{center} \line(1,0){300} \end{center}
\begin{mathpar}
% \Infer[Base]
% { \Gamma \vdash e':t' }
% { \Gamma \cvdash p e t e':t' }
% { }
% \qquad
% \Infer[Path]
% { \pvdash \Gamma p e t \varpi:t_1 \\ \Gamma,(\occ e \varpi:t_1) \cvdash p e t e':t_2 }
% { \Gamma \cvdash p e t e':t_2 }
% { }
\Infer[Base]
{ }
{ \Gamma \evdash p e t \Gamma }
{ }
\qquad
\Infer[Path]
{ \pvdash \Gamma p e t \varpi:t_1 \\ \Gamma \evdash p e t \Gamma' }
{ \Gamma \evdash p e t \Gamma',(\occ e \varpi:t_1) }
{ }
\end{mathpar}
\begin{center} \line(1,0){300} \end{center}
\begin{mathpar}
\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 }
{ }
\qquad
\Infer[PSubs]
{ \pvdash \Gamma p e t \varpi:t_1 \\ t_1\leq t_2 }
{ \pvdash \Gamma p e t \varpi:t_2 }
{ }
\\
\Infer[PTypeof]
{ \Gamma \vdash \occ e \varpi:t' }
{ \pvdash \Gamma p e t \varpi:t' }
{ }
\qquad
\Infer[PEps+]
{ }
{ \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' \\ t_2\land t_2' \simeq \Empty }
{ \pvdash \Gamma p e t \varpi.1:\neg t_1 }
{ }
\\
\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}) }
{ }
\qquad
\Infer[PPairL]
{ \pvdash \Gamma p e t \varpi:\pair{t_1}{t_2} }
{ \pvdash \Gamma p 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 }
{ }
\qquad
\Infer[PFst]
{ \pvdash \Gamma p e t \varpi:t' }
{ \pvdash \Gamma p 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'} }
{ }
\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
\\
......
......@@ -150,3 +150,6 @@
\newcommand{\ts}{\mathbbm{t}}
\newcommand{\tsint}[1]{\textbf{\textup{\{}}#1\textbf{\textup{\}}}}
\newcommand{\tsrep}[1]{\textsf{Repr}(#1)}
\newcommand{\pvdash}[4]{\vdash^{\texttt{Path}}_{#1,#3,#4,#2}}%\mathcal{P}
\newcommand{\evdash}[3]{\vdash^{\texttt{Env}}_{#2,#3,#1}}
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