Commit a00adb5d authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

more on the new version of the language section

parent eaf3651a
......@@ -113,7 +113,7 @@ $\Cx[e]\reduces\Cx[e']$.
While the syntax and reduction semantics are on the whole pretty
standard, for the type system we will have to introduce several
unconventional features that we anticipated in
Section~\ref{sec:challanges}: this system is the core of our work. Let
Section~\ref{sec:challenges}: this system is the core of our work. Let
us start with the standard part, that is the typing of the functional
core and the use of subtyping given by the following typing rules:
\begin{mathpar}
......@@ -124,14 +124,14 @@ core and the use of subtyping given by the following typing rules:
\quad
\Infer[App]
{
\Gamma \vdash e_1: \arrow {t_1}{t_2}\\
\Gamma \vdash e_1: \arrow {t_1}{t_2}\quad
\Gamma \vdash e_2: t_1
}
{ \Gamma \vdash {e_1}{e_2}: t_2 }
{ }
\quad
\Infer[Abs+]
{\forall i\in I\quad\Gamma,x:s_i\vdash e:t_i}
{{\scriptstyle\forall i\in I}\quad\Gamma,x:s_i\vdash e:t_i}
{
\Gamma\vdash\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\textstyle \bigwedge_{i\in I}\arrow {s_i} {t_i}
}
......@@ -215,18 +215,18 @@ integer returns its successor and applied to anything else returns
\[
\lambda^{(\Int\to\Int)\wedge(\neg\Int\to\Bool)} x.\tcase{x}{\Int}{x+1}{\textsf{true}}
\]
Clearly the expression above is well typed, but the rule \Rule{Abs+}
Clearly, the expression above is well typed, but the rule \Rule{Abs+}
is not enough to type it. In particular, according to \Rule{Abs+} we
have to prove that under the hypothesis that $x:\Int$ the expression
$\tcase{x}{\Int}{x+1}{\textsf{true}}$, that is that under the
have to prove that under the hypothesis that $x$ is of type $\Int$ the expression
$\tcase{x}{\Int}{x+1}{\textsf{true}}$ is of type $\Int$, too. That is that under the
hypothesis that x has type $\Int\wedge\Int$ (we apply occurrence
typing) then $x+1$ had type \Int (which is ok) and that under the
typing) the expression $x+1$ is of type \Int (which is ok) and that under the
hypothesis that $x$ has type $\Int\setminus\Int$, that is $\Empty$
(once more we apply occurrence typing), \textsf{true} is of type \Int
(which is not ok). The problem is that we are trying to type the
second case of a type case even if we now that there is no chance that
it will be selected. The fact that it is never selected is witnessed
by the fact that there is a type hypothesis with the $\Empty$ type. To
that case will be selected. The fact that it is never selected is witnessed
by the fact that there is a type hypothesis with $\Empty$ type. To
avoid this problem (and type the term above) we add the rule
\Rule{Efq} (\emph{ex falso quodlibet}) that allows to deduce any type
for an expression that will never be selected, that is for an
......@@ -239,19 +239,148 @@ expression whose type environment has an empty assumption:
\end{mathpar}
Once more, this kind of deduction was already present in~\cite{Frisch2008} to type full fledged overloaded functions, though it was embedded in the typing rule for the type-case. Here we need the more general \Rule{Efq} rule, to ensure the property of subject reduction.\beppe{Example?}
Finally the core of our type system is given by the following rule for the type-case.\beppe{Changed to If to Case}
Finally, there is one final rule that is missing in our type system and which is the core of our work, the rule for the type-case:\beppe{Changed to \Rule{If} to \Rule{Case}}
\begin{mathpar}
\Infer[Case]
{\Gamma\vdash e:t_0\\
%t_0\not\leq \neg t \Rightarrow
\Gamma \evdash + e t \Gamma^+ \\ \Gamma^+ \vdash e_1:t'\\
\Gamma \evdash + e t \Gamma_1 \\ \Gamma_1 \vdash e_1:t'\\
%t_0\not\leq t \Rightarrow
\Gamma \evdash - e t \Gamma^- \\ \Gamma^- \vdash e_2:t'}
\Gamma \evdash - e t \Gamma_2 \\ \Gamma_2 \vdash e_2:t'}
{\Gamma\vdash \tcase {e} t {e_1}{e_2}: t'}
{ }
\end{mathpar}
The rule checks wheter the expression $e$ whose type is tested is
well-typed and then performs the occurrence typing analysis that produces
the environments $\Gamma_i$'s under whose hypothesis the expressions
$e_i$'s are typed. The production of these environments is represented by the judgement
$\Gamma \evdash p e t \Gamma_i$ (with $p$ either $+$ or $-$). The
intuition is that when $\Gamma \evdash p e t \Gamma_i$ is provable
then $\Gamma_i$ is $\Gamma$ extended with type hypothesis for all
expressions occurring in $e$, type hypothesis that can be deduced
assuming that the test $e\in t$ succeeds (for $p=+$) or fails (for
$p=-$).
All it remains to do is to show how to deduce judgements of the form $\Gamma \evdash p e t \Gamma'$. For that we first have to define how to denote occurrences of an expressions. These are just paths in the syntax trees of the expressions.
Let $e$ be an expression and $\varpi\in\{0,1,l,r,f,s\}^*$ a \emph{path}; we denote $\occ e\varpi$ the occurrence of $e$ reached by the path $\varpi$, that is
\[
\begin{array}{r@{\downarrow}l@{\quad=\quad}l}
e&\epsilon & e\\
e_0e_1& i.\varpi & \occ{e_i}\varpi\qquad i=0,1\\
(e_0,e_1)& l.\varpi & \occ{e_0}\varpi\\
(e_0,e_1)& r.\varpi & \occ{e_1}\varpi\\
\pi_1 e& f.\varpi & \occ{e}\varpi\\
\pi_2 e& s.\varpi & \occ{e}\varpi\\
\end{array}
\]
undefined otherwise
To ease our analysis we used different directions for each kind of
term. So we have $0$ and $1$ for the function and argument of an
application, $l$ and $r$ for the $l$eft and $r$ight projections of a pair
and $f$ and $s$ for the argument of a $f$irst or a $s$econd projection. The the judgements $\Gamma \evdash p e t \Gamma'$ are deduced by these two rules:
\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' \\ \Gamma \evdash p e t \Gamma' }
{ \Gamma \evdash p e t \Gamma',(\occ e \varpi:t') }
{ }
\end{mathpar}
These rules describe how to deduce by occurrence typing the type
environts when checking that an expression $e$ has type $t$: we can
deduce $\Gamma$ all the hypothesis already in $\Gamma$ (rule
\Rule{Base}) and that if we can deduce a given for a particular
occurrence $\varpi$ of the $e$ checked, than we can add this
hypothesis to our type environment (rule \Rule{Path}). The rule
\Rule{Path} uses a (last) auxiliary judgement $\pvdash {\Gamma} p e t
\varpi:t'$ to deduce the type of the occurrence $\occ e \varpi$ when
checking $e$ against $t$. This rule is subtler than it appears at
first sight, insofar as the deduction of the type for $\varpi$ may use
some hypothesis on $\occ e \varpi$ (in $\Gamma'$) and from an
algorithmic viewpoint this will imply the computation of a fix-point
(see Section~\ref{}). The last ingredient is the deduction of the
judgements of the form $\pvdash {\Gamma} p e t \varpi:t'$ where
$\varpi$ is an occurrence of $e$. These is given by the following set
of rules.
\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}
Let us comment each rule in detail.
\subsection{Algorithmic system}
......
......@@ -175,11 +175,13 @@ Text of abstract \ldots.
\section{Language}
\label{sec:language}
\input{language}
\section{NEW LANGUAGE}
\input{language2}
{\color{gray}
\section{OLD LANGUAGE}
\input{language}
}
\section{Extensions}
\label{sec:extensions}
\input{extensions}
......
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