Commit 362bbf8c authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

bla bla bla

parent 84ab2472
......@@ -420,9 +420,9 @@ the property of soundness, deduced, as customary, from the properties
of progress and subject reduction, whose proof is given in the
appendix.
\begin{theorem}[soundness]
For every expression $e$ such that $\varnothing\vdash e:t$ either there
exists a value $v$ of type $t$ such that $e\reduces^* v$ or $e$
diverges.
For every expression $e$ such that $\varnothing\vdash e:t$ either $e$
diverges or there
exists a value $v$ of type $t$ such that $e\reduces^* v$.
\end{theorem}
......@@ -470,13 +470,13 @@ judgments, we present in Section~\ref{sec:typenv} an algorithm that we
prove sound \beppe{and complete?}. All these notions are used in the
algorithmic typing system given in Section~\ref{sec:algorules}.
\beppe{\begin{enumerate}
\item type of functions -> type schemes
\item elimination rules (app, proj,if) ->operations on types and how to compute them
\item not syntax directed: rules Subs, Intersect, Env.
\item Compute the environments for occurrence typing. Algorithm to compute $\Gamma\vdash\Gamma$
\end{enumerate}
}
%% \beppe{\begin{enumerate}
%% \item type of functions -> type schemes
%% \item elimination rules (app, proj,if) ->operations on types and how to compute them
%% \item not syntax directed: rules Subs, Intersect, Env.
%% \item Compute the environments for occurrence typing. Algorithm to compute $\Gamma\vdash\Gamma$
%% \end{enumerate}
%% }
\subsubsection{Type schemes}\label{sec:type-schemes}
......@@ -523,8 +523,14 @@ the value. By induction on the definition of values: $\tyof c {} =
\tsfun{s_i\to t_i}_{i\in I}$, $\tyof {(v_1,v_2)}{} = \tyof
{v_1}{}\tstimes\tyof {v_1}{}$. Then we have $v\in t\iffdef \tyof
v{}\leq t$.
We also need to perform intersections of type schemes so as to intersect the static type of an expression with the one deduced by occurrence typing. For our algorithmic system (see \Rule{Env$_{\scriptscriptstyle\mathcal{A}}$} in Section~\ref{sec:algorules}) all we need to define is the intersection of a type with a type scheme:
\begin{lemma}
Let $\ts$ be a type scheme and $t$ a type. We can compute a type scheme, written $t \tsand \ts$, such that
\(\tsint {t \tsand \ts} = \{s \alt \exists t' \in \tsint \ts.\ t \land t' \leq s \}\)
\end{lemma}
\beppe{Do we need the next definition and lemma here or they can go in the appendix?
\beppe{Do we need the next definition or it can go in the appendix?
\begin{definition}[Representative]
We define a function $\tsrep {\_}$ that maps every non-empty type scheme into a type, \textit{representative} of the set of types denoted by the scheme.
......@@ -540,10 +546,7 @@ the value. By induction on the definition of values: $\tyof c {} =
\end{align*}
\end{definition}
Note that $\tsrep \ts \in \tsint \ts$.
\begin{lemma}
Let $\ts$ be a type scheme and $t$ a type. We can compute a type scheme, written $t \tsand \ts$, such that:
\[\tsint {t \tsand \ts} = \{s \alt \exists t' \in \tsint \ts.\ t \land t' \leq s \}\]
\end{lemma}
}
......@@ -561,3 +564,67 @@ Note that $\tsrep \ts \in \tsint \ts$.
\subsection{Algorithmic typing rules}\label{sec:algorules}
\begin{mathpar}
\Infer[Efq$_{\scriptscriptstyle\mathcal{A}}$]
{ }
{ \Gamma, (e:\Empty) \vdashA e': \Empty }
{ \begin{array}{c}\text{\tiny with priority over}\\[-1.8mm]\text{\tiny all the other rules}\end{array}}
\\
\Infer[Env]
{ \Gamma\setminus\{e\} \vdashA e : \ts }
{ \Gamma \vdashA e: \Gamma(e) \tsand \ts }
{ e\in\dom\Gamma}
\qquad
\Infer[Const$_{\scriptscriptstyle\mathcal{A}}$]
{ }
{\Gamma\vdashA c:\basic{c}}
{c\not\in\dom\Gamma}
\\
\Infer[Abs$_{\scriptscriptstyle\mathcal{A}}$]
{\Gamma,x:s_i\vdashA e:\ts_i'\\ \ts_i'\leq t_i}
{
\Gamma\vdashA\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$_{\scriptscriptstyle\mathcal{A}}$]
{
\Gamma \vdashA e_1: \ts_1\\
\Gamma \vdashA e_2: \ts_2\\
\ts_1 \leq \arrow \Empty \Any\\
\ts_2 \leq \dom {\ts_1}
}
{ \Gamma \vdashA {e_1}{e_2}: \ts_1 \circ \ts_2 }
{ {e_1}{e_2}\not\in\dom\Gamma}
\\
\Infer[Case$_{\scriptscriptstyle\mathcal{A}}$]
{\Gamma\vdashA e:\ts_0\\
%\makebox{$\begin{array}{l}
% \left\{
% \begin{array}{ll} %\Gamma,
% \Refine + {e,t} \Gamma \vdashA 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 \vdashA 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 \vdashA e_1 : \ts_1\\
\Refine - {e,t} \Gamma \vdashA e_2 : \ts_2}
{\Gamma\vdashA \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$_{\scriptscriptstyle\mathcal{A}}$]
{\Gamma \vdashA e:\ts\and \ts\leq\pair\Any\Any}
{\Gamma \vdashA \pi_i e:\bpi_{\mathbf{i}}(\ts)}
{\pi_i e\not\in\dom\Gamma}
\Infer[Pair$_{\scriptscriptstyle\mathcal{A}}$]
{\Gamma \vdashA e_1:\ts_1 \and \Gamma \vdashA e_2:\ts_2}
{\Gamma \vdashA (e_1,e_2):{\ts_1}\tstimes{\ts_2}}%\pair{t_1}{t_2}}
{(e_1,e_2)\not\in\dom\Gamma}
\end{mathpar}
......@@ -156,6 +156,7 @@
\newcommand{\tsint}[1]{\textbf{\textup{\{}}#1\textbf{\textup{\}}}}
\newcommand{\tsrep}[1]{\textsf{Repr}(#1)}
\newcommand{\vdashA}{\vdash_{\!\scriptscriptstyle\mathcal{A}}}
\newcommand{\vdashp}{\vdash^{\texttt{Path}}}
\newcommand{\pvdash}[4]{\vdashp_{#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