Commit 956044cc authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

new version of the language

parent a8778d48
......@@ -278,7 +278,7 @@ that always diverge on \String{} arguments).
This is essentially what we formalize in Section~\ref{sec:language}.
\subsection{Technical challenges}
\subsection{Technical challenges}\label{sec:challenges}
In the previous section we outlined the main ideas of our approach to occurrence typing. However, devil is in the details. So the formalization we give in Section~\ref{sec:language} is not so smooth as we just outlined: we must introduce several auxiliary definitions to handle some corner cases. This section presents by tiny examples the main technical difficulties we had to overcome and the definitions we introduced to handle them. As such it provides a kind of road-map to the technicalities of Section~\ref{sec:language}.
......
......@@ -2,7 +2,7 @@ In this section we present the formalization of the ideas we hinted in the intro
\subsection{Types}
\begin{definition}[Type syntax]\label{def:types} The set of types \types{} are the terms $t$ coinductively produced by the following grammar
\begin{definition}[Type syntax]\label{def:types} The set of types \types{} is formed by the terms $t$ coinductively produced by the following grammar
\[
\begin{array}{lrcl}
\textbf{Types} & t & ::= & b\alt t\to t\alt t\times t\alt t\vee t \alt \neg t \alt \Empty
......@@ -42,7 +42,7 @@ by~\citet{Frisch2008} to which the reader may refer for more details. Its formal
For this presentation it suffices to consider that
types are interpreted as sets of \emph{values} ({\emph{ie}, either
constants, $\lambda$-abstractions, or pair of values: see
Section~\ref{}) that have that type, and that subtyping is set
Section~\ref{sec:syntax} right below) that have that type, and that subtyping is set
containment (\emph{ie}, a type $s$ is a subtype of a type $t$ if and only if $t$
contains all the values of type $s$). In particular, $s\to t$
contains all $\lambda$-abstractions that when applied to a value of
......@@ -59,9 +59,9 @@ union of the values of the two types).
\subsection{Syntax}\label{sec:syntax}
The expressions $e$ and values $v$ of our language are the terms inductively generated by the following grammars:
\begin{equation}\label{expressions}
\begin{array}{rclr}
e &::=& c\alt x\alt ee\alt\lambda^{\wedge_{i\in I}s_i\to t_i} x.e\alt \pi_i e\alt(e,e)\alt\tcase{e}{t}{e}{e}\\
v &::=& c\alt\lambda^{\wedge_{i\in I}s_i\to t_i} x.e\alt (v,v)
\begin{array}{lrclr}
\textbf{Expr} &e &::=& c\alt x\alt ee\alt\lambda^{\wedge_{i\in I}s_i\to t_i} x.e\alt \pi_i e\alt(e,e)\alt\tcase{e}{t}{e}{e}\\[1mm]
\textbf{Values} &v &::=& c\alt\lambda^{\wedge_{i\in I}s_i\to t_i} x.e\alt (v,v)
\end{array}
\end{equation}
for $i=1,2$. In~\eqref{expressions}, $c$ ranges over constants
......@@ -110,6 +110,148 @@ $\Cx[e]\reduces\Cx[e']$.
\subsection{Static semantics}
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
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}
\Infer[Const]
{ }
{\Gamma\vdash c:\basic{c}}
{ }
\quad
\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 }
{ }
\quad
\Infer[Abs+]
{\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}
}
{ }
% \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[Proj]
{\Gamma \vdash e:\pair{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}}
{ }
\qquad
\Infer[Subs]
{ \Gamma \vdash e:t\\t\leq t' }
{ \Gamma \vdash e: t' }
{ }
\qquad
\end{mathpar}
These rules are quite standard and do not need any particular explanation. Just notice that we used a classic subsumption rule to embed subtyping in the type system.
Let us now focus on the unconventional aspects of our system. starting
from the simplest ones. The first one is that, as explained in
Section~\ref{sec:challenges}, our assumptions are about
expressions. Therefore the type environments of our rules, ranged over
by $\Gamma$ map \emph{expressions}---rather than just variables---into
types. This explains why the classic typing rule for variables is replace by the more general \Rule{Env} rule below:\beppe{Changed the name of Occ into Env since it seems more appropriate}
\begin{mathpar}
\Infer[Env]
{ }
{ \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 }
{ }
\end{mathpar}
The rule is coupled with the classic intersection introduction rule
which allow us to deduce for a complex expression the intersection of
the types recorded by the occurrence typing analysis in the
environment $\Gamma$ with the static type deduced for the same
expression by using the other typing rules. This same intersection
rule is also used to infer the second unconventional aspect of our
system, that is the fact that $\lambda$ abstractions can have negated
arrow types as long as this negation does not make their type empty:
\begin{mathpar}
\Infer[Abs-]
{\Gamma \vdash \lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:t}
{ \Gamma \vdash\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:t\wedge\neg(t_1\to t_2) }
{ (t\wedge\neg(t_1\to t_2))\not\simeq\Empty }
\end{mathpar}
As explained in Section~\ref{sec:challenges} we need to be able to
deduce for, say, the function $\lambda^{\Int\to\Int} x.x$ a type such
as $(\Int\to\Int)\wedge\neg(\Bool\to\Bool)$ (in particular, if this is
the term $e$ in equation \eqref{bistwo} we need to deduce for it the
type $(\Int\to\Int)\wedge\neg(\Int\to\neg\Int)$, that is,
$(\Int\to\Int)\setminus(\Int\to\neg\Int)$ ). But the rule \Rule{Abs+}
above does not allow us to deduce negations of
arrows for abstractions: the rule \Rule{Abs-} makes this possible. As an aside, note that this kind
of deduction was already present in the system by~\cite{Frisch2008}
though it that system was motivated by the type semantics rather than
by the soundness of the type system.
Rules \Rule{Abs+} and \Rule{Abs-} are not enough to deduce for
$\lambda$-abstractions all the types we wish. In particular, these
rules alone are not enough to type general overloaded functions. For
example, consider this simple example of a function that applied to an
integer returns its successor and applied to anything else returns
\textsf{true}
\[
\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+}
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
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
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
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
expression whose type environment has an empty assumption:
\begin{mathpar}
\Infer[Efq]
{ }
{ \Gamma, (e:\Empty) \vdash e': t }
{ }
\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}
\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'\\
%t_0\not\leq t \Rightarrow
\Gamma \evdash - e t \Gamma^- \\ \Gamma^- \vdash e_2:t'}
{\Gamma\vdash \tcase {e} t {e_1}{e_2}: t'}
{ }
\end{mathpar}
\subsection{Algorithmic system}
......
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