language.tex 22.7 KB
Newer Older
1
\newlength{\sk}
Giuseppe Castagna's avatar
space    
Giuseppe Castagna committed
2
\setlength{\sk}{-1.9pt}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
3
\iflongversion
Giuseppe Castagna's avatar
Giuseppe Castagna committed
4
In this section we formalize the ideas we outlined in the introduction. We start by the definition of types followed by the language and its reduction semantics. The static semantics is the core of our work: we first present a declarative type system that deduces (possibly many) types for well-typed expressions and then the algorithms to decide whether an expression is well typed or not. 
Giuseppe Castagna's avatar
Giuseppe Castagna committed
5
\fi
6
7

\subsection{Types}
8
9
\begin{definition}[Types]\label{def:types}
%\iflongversion%%%%%%%
Kim Nguyễn's avatar
Kim Nguyễn committed
10
The set of types \types{} is formed by the terms $t$ coinductively produced by the grammar:\svvspace{-1.45mm}
11
12
13
14
15
\[
\begin{array}{lrcl}
\textbf{Types} & t & ::= & b\alt t\to t\alt t\times t\alt t\vee t \alt \neg t \alt \Empty 
\end{array}
\]
Giuseppe Castagna's avatar
Giuseppe Castagna committed
16
17
and that satisfy the following conditions
\begin{itemize}[nosep]
Giuseppe Castagna's avatar
Giuseppe Castagna committed
18
19
\item (regularity) every term has a finite number of different sub-terms;
\item (contractivity) every infinite branch of a term contains an infinite number of occurrences of the
Kim Nguyễn's avatar
Kim Nguyễn committed
20
arrow or product type constructors.\svvspace{-1mm}
21
\end{itemize}
22
\iffalse%%%%%%%%%%%%%%%%%%%%%%%%%%
Kim Nguyễn's avatar
Kim Nguyễn committed
23
A type $t\in\types{}$ is a term coinductively produced by the grammar:\svvspace{-1.45mm}
24
25
26
27
28
29
30
\[
\begin{array}{lrcl}
\textbf{Types} & t & ::= & b\alt t\to t\alt t\times t\alt t\vee t \alt \neg t \alt \Empty 
\end{array}
\]
that satisfies the following conditions: $(1)$\emph{Regularity}: the
term has a finite number of different sub-terms; $(2)$ \emph{Contractivity}: every infinite branch of the term contains an infinite number of occurrences of the
Kim Nguyễn's avatar
Kim Nguyễn committed
31
arrow or product type constructors.\svvspace{-1mm}
32
\fi%%%%%%%%%%%%%%%%%%%
33
\end{definition}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
34
We use the following abbreviations: $
35
36
    t_1 \land t_2 \eqdef \neg (\neg t_1 \vee \neg t_2)$, 
    $t_ 1 \setminus t_2 \eqdef t_1 \wedge \neg t_2$, $\Any \eqdef \neg \Empty$.
Giuseppe Castagna's avatar
Giuseppe Castagna committed
37
$b$ ranges over basic types
Giuseppe Castagna's avatar
Giuseppe Castagna committed
38
(e.g., \Int, \Bool),
39
40
41
42
43
44
45
$\Empty$ and $\Any$ respectively denote the empty (that types no value)
and top (that types all values) types. Coinduction accounts for
recursive types and the condition on infinite branches bars out
ill-formed types such as 
$t = t \lor t$ (which does not carry any information about the set
denoted by the type) or $t = \neg t$ (which cannot represent any
set). 
46
\iflongversion%%%%%%%%%%%%%%%%%%
47
It also ensures that the binary relation $\vartriangleright
Giuseppe Castagna's avatar
typos    
Giuseppe Castagna committed
48
\,\subseteq\!\types{\times}\types$ defined by $t_1 \lor t_2 \vartriangleright
49
t_i$, $t_1 \land t_2 \vartriangleright
Giuseppe Castagna's avatar
Giuseppe Castagna committed
50
t_i$, $\neg t \vartriangleright t$ is Noetherian.
51
This gives an induction principle on $\types$ that we
Giuseppe Castagna's avatar
Giuseppe Castagna committed
52
will use without any further explicit reference to the relation.\footnote{In a nutshell, we can do proofs by induction on the structure of unions and negations---and, thus, intersections---but arrows, products, and basic types are the base cases for the induction.} 
53
\fi%%%%%%%%%%%%%%%%%%%%%%
54
55
56
57
58
We refer to $ b $, $\times$, and $ \to $ as \emph{type constructors}
and to $ \lor $, $ \land $, $ \lnot $, and $ \setminus $
as \emph{type connectives}.

The subtyping relation for these types, noted $\leq$, is the one defined
Giuseppe Castagna's avatar
Giuseppe Castagna committed
59
by~\citet{Frisch2008} to which the reader may refer for the formal
Giuseppe Castagna's avatar
bla    
Giuseppe Castagna committed
60
definition (we recall it in Appendix~\ref{sec:subtyping} for the
Giuseppe Castagna's avatar
typos    
Giuseppe Castagna committed
61
62
reader's convenience). A detailed description of the algorithm to
decide this relation can be found in~\cite{Cas15}.
63
For this presentation it suffices to consider that
Giuseppe Castagna's avatar
Giuseppe Castagna committed
64
types are interpreted as sets of \emph{values} ({i.e., either
Victor Lanvin's avatar
Fixes    
Victor Lanvin committed
65
constants, $\lambda$-abstractions, or pairs of values: see
66
Section~\ref{sec:syntax} right below) that have that type, and that subtyping is set
Giuseppe Castagna's avatar
Giuseppe Castagna committed
67
containment (i.e., a type $s$ is a subtype of a type $t$ if and only if $t$
68
69
contains all the values of type $s$). In particular, $s\to t$
contains all $\lambda$-abstractions that when applied to a value of
70
type $s$, if their computation terminates, then they return a result of
Giuseppe Castagna's avatar
Giuseppe Castagna committed
71
type $t$ (e.g., $\Empty\to\Any$ is the set of all
72
73
74
75
functions\footnote{\label{allfunctions}Actually, for every type $t$,
all types of the form $\Empty{\to}t$ are equivalent and each of them
denotes the set of all functions.} and $\Any\to\Empty$ is the set
of functions that diverge on every argument). Type connectives
Giuseppe Castagna's avatar
Giuseppe Castagna committed
76
77
(i.e., union, intersection, negation) are interpreted as the
corresponding set-theoretic operators (e.g.,~$s\vee t$ is the
78
union of the values of the two types). We use $\simeq$ to denote the
Giuseppe Castagna's avatar
Giuseppe Castagna committed
79
symmetric closure of $\leq$: thus $s\simeq t$ (read, $s$ is equivalent to $t$) means that $s$ and $t$ denote the same set of values and, as such, they are semantically the same type.
80
81

\subsection{Syntax}\label{sec:syntax}
Kim Nguyễn's avatar
Kim Nguyễn committed
82
The expressions $e$ and values $v$ of our language are inductively generated by the following grammars:\svvspace{-1mm}
83
\begin{equation}\label{expressions}
84
\begin{array}{lrclr}  
Giuseppe Castagna's avatar
Giuseppe Castagna committed
85
86
  \textbf{Expr} &e &::=& c\alt x\alt ee\alt\lambda^{\wedge_{i\in I}s_i\to t_i} x.e\alt \pi_j e\alt(e,e)\alt\tcase{e}{t}{e}{e}\\[.3mm]
  \textbf{Values} &v &::=& c\alt\lambda^{\wedge_{i\in I}s_i\to t_i} x.e\alt (v,v)\\[-1mm]
87
88
\end{array}
\end{equation}
Giuseppe Castagna's avatar
wording    
Giuseppe Castagna committed
89
for $j=1,2$. In~\eqref{expressions}, $c$ ranges over constants
Giuseppe Castagna's avatar
Giuseppe Castagna committed
90
(e.g., \texttt{true}, \texttt{false}, \texttt{1}, \texttt{2},
91
92
...) which are values of basic types (we use $\basic{c}$ to denote the
basic type of the constant $c$); $x$ ranges over variables; $(e,e)$
Kim Nguyễn's avatar
typos.    
Kim Nguyễn committed
93
denotes pairs and $\pi_i e$ their projections; $\tcase{e}{t}{e_1}{e_2}$
94
95
96
97
98
99
100
101
102
103
denotes the type-case expression that evaluates either $e_1$ or $e_2$
according to whether the value returned by $e$ (if any) is of type $t$
or not; $\lambda^{\wedge_{i\in I}s_i\to t_i} x.e$ is a value of type
$\wedge_{i\in I}s_i\to t_i$ and denotes the function of parameter $x$
and body $e$. An expression has an intersection type if and only if it
has all the types that compose the intersection. Therefore,
intuitively, $\lambda^{\wedge_{i\in I}s_i\to t_i} x.e$ is a well-typed
value if for all $i{\in} I$ the hypothesis that $x$ is of type $s_i$
implies that the body $e$ has type $t_i$, that is to say, it is well
typed if $\lambda^{\wedge_{i\in I}s_i\to t_i} x.e$ has type $s_i\to
Giuseppe Castagna's avatar
typos    
Giuseppe Castagna committed
104
t_i$ for all $i\in I$. Every value is associated to a most specific type (mst): the mst of $c$ is $\basic c$; the mst of
105
 $\lambda^{\wedge_{i\in I}s_i\to t_i} x.e$ is $\wedge_{i\in I}s_i\to t_i$; and, inductively,
Giuseppe Castagna's avatar
Giuseppe Castagna committed
106
107
the mst of a pair of values is the product of the mst's of the
values. We write $v\in t$ if the most specific type of $v$ is a subtype of $t$ (see Appendix~\ref{app:typeschemes} for the formal definition of $v\in t$ which  deals with some corner cases for negated arrow types).
108
109
110



111
\subsection{Dynamic semantics}\label{sec:opsem}
112

Kim Nguyễn's avatar
Kim Nguyễn committed
113
The dynamic semantics is defined as a classic left-to-right call-by-value reduction for a $\lambda$-calculus with pairs, enriched with specific rules for type-cases. We have the following  notions of reduction:\svvspace{-1.2mm}
114
115
\[
\begin{array}{rcll}
Kim Nguyễn's avatar
Kim Nguyễn committed
116
  (\lambda^{\wedge_{i\in I}s_i\to t_i} x.e)\,v &\reduces& e\subst x v\\[-.4mm]
Giuseppe Castagna's avatar
Giuseppe Castagna committed
117
118
  \pi_i(v_1,v_2) &\reduces& v_i & i=1,2\\[-.4mm]
  \tcase{v}{t}{e_1}{e_2} &\reduces& e_1 &v\in t\\[-.4mm] 
Giuseppe Castagna's avatar
Giuseppe Castagna committed
119
  \tcase{v}{t}{e_1}{e_2} &\reduces& e_2 &v\not\in t\\[-1.3mm]
120
121
\end{array}
\]
Giuseppe Castagna's avatar
Giuseppe Castagna committed
122
Contextual reductions are
Giuseppe Castagna's avatar
Giuseppe Castagna committed
123
124
125
defined by the following evaluation contexts:\\[1mm]
\centerline{\(
%\[
126
\Cx[] ::= [\,]\alt \Cx e\alt v\Cx \alt (\Cx,e)\alt (v,\Cx)\alt \pi_i\Cx\alt \tcase{\Cx}tee
Giuseppe Castagna's avatar
Giuseppe Castagna committed
127
128
%\]
\)}\\[1mm]
129
130
131
As usual we denote by $\Cx[e]$ the term obtained by replacing $e$ for
the hole in the context $\Cx$ and we have that $e\reduces e'$ implies
$\Cx[e]\reduces\Cx[e']$.
132

Giuseppe Castagna's avatar
Giuseppe Castagna committed
133
\subsection{Static semantics}\label{sec:static}
134

135
While the syntax and reduction semantics are, on the whole, pretty
Giuseppe Castagna's avatar
bla    
Giuseppe Castagna committed
136
standard, for what concerns the type system we will have to introduce several
137
unconventional features that we anticipated in
Giuseppe Castagna's avatar
Giuseppe Castagna committed
138
Section~\ref{sec:challenges} and are at the core of our work. Let
139
us start with the standard part, that is the typing of the functional
Kim Nguyễn's avatar
Kim Nguyễn committed
140
core and the use of subtyping, given by the following typing rules:\svvspace{-1mm}
141
142
143
144
145
146
147
148
\begin{mathpar}
  \Infer[Const]
      { }
      {\Gamma\vdash c:\basic{c}}
      { }
  \quad
  \Infer[App]
      {
149
        \Gamma \vdash e_1: \arrow {t_1}{t_2}\quad
150
151
152
153
154
155
        \Gamma \vdash e_2: t_1
      }
      { \Gamma \vdash {e_1}{e_2}: t_2 }
      { }
  \quad
  \Infer[Abs+]
156
      {{\scriptstyle\forall i\in I}\quad\Gamma,x:s_i\vdash e:t_i}
157
158
159
160
161
162
163
164
165
166
167
168
      {
      \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'}
%            { }
Giuseppe Castagna's avatar
Giuseppe Castagna committed
169
\end{mathpar}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
170
\begin{mathpar}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
171
      \Infer[Sel]
172
173
174
175
176
177
178
179
180
181
182
183
184
  {\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' }
      { }
Kim Nguyễn's avatar
Kim Nguyễn committed
185
  \qquad\svvspace{-3mm}
186
\end{mathpar}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
187
These rules are quite standard and do not need any particular explanation besides those already given in Section~\ref{sec:syntax}. Just notice subtyping is embedded in the system by the classic \Rule{Subs} subsumption rule. Next we focus on the unconventional aspects of our system, from the simplest to the hardest.
188

Giuseppe Castagna's avatar
Giuseppe Castagna committed
189
The first unconventional aspect is that, as explained in
190
Section~\ref{sec:challenges}, our type assumptions are about
Giuseppe Castagna's avatar
Giuseppe Castagna committed
191
expressions. Therefore, in our rules the type environments, ranged over
192
by $\Gamma$, map \emph{expressions}---rather than just variables---into
Kim Nguyễn's avatar
Kim Nguyễn committed
193
types. This explains why the classic typing rule for variables is replaced by a more general \Rule{Env} rule defined below:\svvspace{-1mm}
194
195
196
197
198
199
\begin{mathpar}
  \Infer[Env]
      { }
      { \Gamma \vdash e: \Gamma(e) }
      { e\in\dom\Gamma }
  \qquad
200
  \Infer[Inter]
201
202
      { \Gamma \vdash e:t_1\\\Gamma \vdash e:t_2 }
      { \Gamma \vdash e: t_1 \wedge t_2 }
Kim Nguyễn's avatar
Kim Nguyễn committed
203
      { }\svvspace{-3mm}
204
\end{mathpar}
205
The \Rule{Env} rule is coupled with the standard intersection introduction rule \Rule{Inter}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
206
which allows us to deduce for a complex expression the intersection of
207
208
209
210
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
211
system, that is, the fact that $\lambda$-abstractions can have negated
Kim Nguyễn's avatar
Kim Nguyễn committed
212
arrow types, as long as these negated types do not make the type deduced for the function empty:\svvspace{-.5mm}
213
214
\begin{mathpar}
  \Infer[Abs-]
Mickael Laurent's avatar
Mickael Laurent committed
215
216
    {\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:\neg(t_1\to t_2)  }
Kim Nguyễn's avatar
Kim Nguyễn committed
217
    { ((\wedge_{i\in I}\arrow {s_i} {t_i})\wedge\neg(t_1\to t_2))\not\simeq\Empty }\svvspace{-1.2mm}
218
\end{mathpar}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
219
220
221
222
223
224
225
%\beppe{I have doubt: is this safe or should we play it safer and
%  deduce $t\wedge\neg(t_1\to t_2)$? In other terms is is possible to
%  deduce two separate negation of arrow types that when intersected
%  with the interface are non empty, but by intersecting everything
%  makes the type empty? It should be safe since otherwise intersection
%  would not be admissible in semantic subtyping (see Theorem 6.15 in
%  JACM), but I think we should doube ckeck it.}
226
As explained in Section~\ref{sec:challenges}, we need to be able to
227
228
229
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
Giuseppe Castagna's avatar
Giuseppe Castagna committed
230
231
type $(\Int\to t)\wedge\neg(\Int\to\neg\Bool)$, that is,
$(\Int\to t)\setminus(\Int\to\neg\Bool)$ ). But the sole rule \Rule{Abs+}
232
233
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
Giuseppe Castagna's avatar
typos    
Giuseppe Castagna committed
234
of deduction is already present in the system by~\citet{Frisch2008}
Kim Nguyễn's avatar
typo.    
Kim Nguyễn committed
235
though in that system this presence was motivated by the semantics of types rather than, as in our case,
236
237
238
239
240
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
Giuseppe Castagna's avatar
Giuseppe Castagna committed
241
instance, consider this simple example of a function that applied to an
242
integer returns its successor and applied to anything else returns
Giuseppe Castagna's avatar
Giuseppe Castagna committed
243
244
245
\textsf{true}:\\[1mm]
\centerline{\(
%\[
246
\lambda^{(\Int\to\Int)\wedge(\neg\Int\to\Bool)} x\,.\,\tcase{x}{\Int}{x+1}{\textsf{true}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
247
%\]
Giuseppe Castagna's avatar
spacing    
Giuseppe Castagna committed
248
\)}\\[.6mm]
249
Clearly, the expression above is well typed, but the rule \Rule{Abs+} alone
250
is not enough to type it. In particular, according to \Rule{Abs+} we
251
have to prove that under the hypothesis that $x$ is of type $\Int$ the expression
252
$(\tcase{x}{\Int}{x+1}{\textsf{true}})$ is of type $\Int$, too.  That is, that under the
Giuseppe Castagna's avatar
Giuseppe Castagna committed
253
hypothesis that $x$ has type $\Int\wedge\Int$ (we apply occurrence
254
typing) the expression $x+1$ is of type \Int{} (which holds) and that under the
255
hypothesis that $x$ has type $\Int\setminus\Int$, that is $\Empty$
256
257
(we apply once more occurrence typing), \textsf{true} is of type \Int{}
(which \emph{does not} hold). The problem is that we are trying to type the
258
second case of a type-case even if we know that there is no chance that, when $x$ is bound to an integer,
259
260
that case will be ever selected. The fact that it is never selected is witnessed
by the presence of a type hypothesis with  $\Empty$ type. To
261
avoid this problem (and type the term above) we add the rule
262
263
264
\Rule{Efq} (\emph{ex falso quodlibet}) that allows the system to deduce any type
for an expression that will never be selected, that is, for an
expression whose type environment contains an empty assumption:
265
266
267
268
\begin{mathpar}
  \Infer[Efq]
  { }
  { \Gamma, (e:\Empty) \vdash e': t }
Kim Nguyễn's avatar
Kim Nguyễn committed
269
  { }\svvspace{-3mm}
270
\end{mathpar}
271
272
Once more, this kind of deduction was already present in the system
by~\citet{Frisch2008} to type full fledged overloaded functions,
Giuseppe Castagna's avatar
typos    
Giuseppe Castagna committed
273
though it was embedded in the typing rule for the type-case.
Giuseppe Castagna's avatar
Giuseppe Castagna committed
274
Here we
Giuseppe Castagna's avatar
Giuseppe Castagna committed
275
need the rule \Rule{Efq}, which is more general, to ensure the
Giuseppe Castagna's avatar
Giuseppe Castagna committed
276
277
property of subject reduction.
%\beppe{Example?}
278

Giuseppe Castagna's avatar
Giuseppe Castagna committed
279
Finally, there remains one last rule in our type system, the one that
280
implements occurrence typing, that is, the rule for the
Kim Nguyễn's avatar
Kim Nguyễn committed
281
type-case:\svvspace{-1mm}
282
283
284
285
\begin{mathpar}
    \Infer[Case]
        {\Gamma\vdash e:t_0\\
        %t_0\not\leq \neg t \Rightarrow
286
        \Gamma \evdash e t \Gamma_1 \\ \Gamma_1 \vdash e_1:t'\\
287
        %t_0\not\leq t \Rightarrow
288
        \Gamma \evdash e {\neg t} \Gamma_2 \\ \Gamma_2 \vdash e_2:t'}
289
        {\Gamma\vdash \tcase {e} t {e_1}{e_2}: t'}
Kim Nguyễn's avatar
Kim Nguyễn committed
290
        { }\svvspace{-3mm}
291
\end{mathpar}
292
293
294
295
296
297
298
299
300
301
302
303
The rule \Rule{Case} checks whether the expression $e$, whose type is
being 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 judgments $\Gamma \evdash e
{(\neg)t} \Gamma_i$. The intuition is that when $\Gamma \evdash e t
\Gamma_1$ is provable then $\Gamma_1$ is a version of $\Gamma$
extended with type hypotheses for all expressions occurring in $e$,
type hypotheses that can be deduced assuming that the test $e\in t$
succeeds. Likewise, $\Gamma \evdash e {\neg t} \Gamma_2$ (notice the negation on $t$) extends
$\Gamma$ with the hypothesis deduced assuming that $e\in\neg t$, that
is, for when the test $e\in t$ fails.
304

305
All it remains to do is to show how to deduce judgments of the form
Giuseppe Castagna's avatar
Giuseppe Castagna committed
306
$\Gamma \evdash e t \Gamma'$. For that we first define how
Giuseppe Castagna's avatar
Giuseppe Castagna committed
307
308
to denote occurrences of an expression. These are identified by paths in the
syntax tree of the expressions, that is, by possibly empty strings of
309
310
311
312
313
314
characters denoting directions starting from the root of the tree (we
use $\epsilon$ for the empty string/path, which corresponds to the
root of the tree).

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
Kim Nguyễn's avatar
Kim Nguyễn committed
315
the path $\varpi$, that is (for $i=0,1$, and undefined otherwise)\svvspace{-.4mm}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
316
317
318
319
320
321
322
323
324
325
326
327
328
%% \[
%% \begin{array}{l}
%% \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}\\
%% \text{undefined otherwise}
%% \end{array}
%% \]
329
\[
Giuseppe Castagna's avatar
Giuseppe Castagna committed
330
\begin{array}{r@{\downarrow}l@{\quad=\quad}lr@{\downarrow}l@{\quad=\quad}lr@{\downarrow}l@{\quad=\quad}l}
Kim Nguyễn's avatar
Kim Nguyễn committed
331
332
e&\epsilon & e & (e_1,e_2)& l.\varpi & \occ{e_1}\varpi &\pi_1 e& f.\varpi & \occ{e}\varpi\\
e_0\,e_1& i.\varpi & \occ{e_i}\varpi \quad\qquad& (e_1,e_2)& r.\varpi & \occ{e_2}\varpi \quad\qquad&
Giuseppe Castagna's avatar
spaces    
Giuseppe Castagna committed
333
\pi_2 e& s.\varpi & \occ{e}\varpi\\[-.4mm]
334
335
336
337
\end{array}
\]
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
338
application, $l$ and $r$ for the $l$eft and $r$ight expressions forming a pair,
Giuseppe Castagna's avatar
Giuseppe Castagna committed
339
and $f$ and $s$ for the argument of a $f$irst or of a $s$econd projection. Note also that we do not consider occurrences
Giuseppe Castagna's avatar
Giuseppe Castagna committed
340
under $\lambda$'s (since their type is frozen in their annotations) and type-cases (since they reset the analysis).
Giuseppe Castagna's avatar
space    
Giuseppe Castagna committed
341
%
Kim Nguyễn's avatar
Kim Nguyễn committed
342
The judgments  $\Gamma \evdash e t \Gamma'$ are then deduced by the following two rules:\svvspace{-1mm} \begin{mathpar}
343
344
345
346
347
348
349
350
351
352
353
%        \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]
      { }
354
      { \Gamma \evdash e t \Gamma }
355
356
357
      { }
    \qquad
    \Infer[Path]
358
359
      { \pvdash {\Gamma'} e t \varpi:t' \\ \Gamma \evdash e t \Gamma' }
      { \Gamma \evdash e t \Gamma',(\occ e \varpi:t') }
Kim Nguyễn's avatar
Kim Nguyễn committed
360
      { }\svvspace{-1.5mm}
361
\end{mathpar}
362
363
364
365
These rules describe how to produce by occurrence typing the type
environments while checking that an expression $e$ has type $t$. They state that $(i)$ we can
deduce from $\Gamma$ all the hypothesis already in $\Gamma$ (rule
\Rule{Base}) and that $(ii)$ if we can deduce a given type $t'$ for a particular
Giuseppe Castagna's avatar
Giuseppe Castagna committed
366
occurrence $\varpi$ of the expression $e$ being checked, then we can add this
367
hypothesis to the produced type environment (rule \Rule{Path}). The rule
368
\Rule{Path} uses a (last) auxiliary judgement $\pvdash {\Gamma}  e t
Giuseppe Castagna's avatar
Giuseppe Castagna committed
369
\varpi:t'$ to deduce the type $t'$ of the occurrence $\occ e \varpi$ when
370
371
372
373
374
checking $e$ against $t$ under the hypotheses $\Gamma$. This rule \Rule{Path} is subtler than it may appear at
first sight, insofar as the deduction of the type for $\varpi$ may already 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{sec:typenv}). The last ingredient for our type system is the deduction of the
375
judgements of the form $\pvdash {\Gamma}  e t \varpi:t'$ where
376
$\varpi$ is a path to an expression occurring in $e$. This is given by the following set
377
378
379
of rules.
\begin{mathpar}
    \Infer[PSubs]
380
381
        { \pvdash \Gamma e t \varpi:t_1 \\ t_1\leq t_2 }
        { \pvdash \Gamma e t \varpi:t_2 }
382
        { }
383
        \quad
384
    \Infer[PInter]
385
386
        { \pvdash \Gamma e t \varpi:t_1 \\ \pvdash \Gamma e t \varpi:t_2 }
        { \pvdash \Gamma e t \varpi:t_1\land t_2 }
387
        { }
388
        \quad
389
390
    \Infer[PTypeof]
        { \Gamma \vdash \occ e \varpi:t' }
391
        { \pvdash \Gamma e t \varpi:t' }
392
        { }
Kim Nguyễn's avatar
Kim Nguyễn committed
393
\svvspace{-1.2mm}\\
394
    \Infer[PEps]
395
        { }
396
        { \pvdash \Gamma e t \epsilon:t }
397
398
399
        { }
        \qquad
    \Infer[PAppR]
400
401
        { \pvdash \Gamma e t \varpi.0:\arrow{t_1}{t_2} \\ \pvdash \Gamma e t \varpi:t_2'}
        { \pvdash \Gamma e t \varpi.1:\neg t_1 }
402
        { t_2\land t_2' \simeq \Empty  }
Kim Nguyễn's avatar
Kim Nguyễn committed
403
\end{mathpar}\begin{mathpar}\svvspace{-2mm}
404
    \Infer[PAppL]
405
406
        { \pvdash \Gamma e t \varpi.1:t_1 \\ \pvdash \Gamma e t \varpi:t_2 }
        { \pvdash \Gamma e t \varpi.0:\neg (\arrow {t_1} {\neg t_2}) }
407
408
409
        { }
        \qquad
    \Infer[PPairL]
410
411
        { \pvdash \Gamma e t \varpi:\pair{t_1}{t_2} }
        { \pvdash \Gamma e t \varpi.l:t_1 }
412
        { }
Kim Nguyễn's avatar
Kim Nguyễn committed
413
\svvspace{-1.2mm}\\
414
    \Infer[PPairR]
415
416
        { \pvdash \Gamma e t \varpi:\pair{t_1}{t_2} }
        { \pvdash \Gamma e t \varpi.r:t_2 }
417
418
419
        { }
        \qquad
    \Infer[PFst]
420
421
        { \pvdash \Gamma e t \varpi:t' }
        { \pvdash \Gamma e t \varpi.f:\pair {t'} \Any }
422
423
424
        { }
        \qquad
    \Infer[PSnd]
425
426
        { \pvdash \Gamma e t \varpi:t' }
        { \pvdash \Gamma e t \varpi.s:\pair \Any {t'} }
Kim Nguyễn's avatar
Kim Nguyễn committed
427
        { }\svvspace{-0.9mm}
428
\end{mathpar}
429
430
431
These rules implement the analysis described in
Section~\ref{sec:ideas} for functions and extend it to products.  Let
us comment each rule in detail. \Rule{PSubs} is just subsumption for
432
the deduction $\vdashp$. The rule \Rule{PInter} combined with
433
434
\Rule{PTypeof} allows the system to deduce for an occurrence $\varpi$
the intersection of the static type of $\occ e \varpi$ (deduced by
435
\Rule{PTypeof}) with the type deduced for $\varpi$ by the other $\vdashp$ rules. The
Giuseppe Castagna's avatar
Giuseppe Castagna committed
436
rule \Rule{PEps} is the starting point of the analysis: if we are assuming that the test $e\in t$ succeeds, then we can assume that $e$ (i.e.,
437
$\occ e\epsilon$) has type $t$ (recall that assuming that the test $e\in t$ fails corresponds to having $\neg t$ at the index of the turnstyle).
Giuseppe Castagna's avatar
Giuseppe Castagna committed
438
The rule \Rule{PAppR} implements occurrence typing for
439
440
441
the arguments of applications, since it states that if a function maps
arguments of type $t_1$ in results of type $t_2$ and an application of
this function yields results (in $t'_2$) that cannot be in $t_2$
Giuseppe Castagna's avatar
Giuseppe Castagna committed
442
(since $t_2\land t_2' \simeq \Empty$), then the argument of this application cannot be of type $t_1$. \Rule{PAppL} performs the
443
444
445
446
occurrence typing analysis for the function part of an application,
since it states that if an application has type $t_2$ and the argument
of this application has type $t_1$, then the function in this
application cannot have type $t_1\to\neg t_2$. Rules \Rule{PPair\_}
447
are straightforward since they state that the $i$-th projection of a pair
Giuseppe Castagna's avatar
Giuseppe Castagna committed
448
that is of type $\pair{t_1}{t_2}$ must be of type $t_i$. So are the last two
449
450
451
452
rules that essentially state that if $\pi_1 e$ (respectively, $\pi_2
e$) is of type $t'$, then the type of $e$ must be of the form
$\pair{t'}\Any$ (respectively, $\pair\Any{t'}$).

Giuseppe Castagna's avatar
typos    
Giuseppe Castagna committed
453
454
This concludes the presentation of all the rules of our type system
(they are summarized for the reader's convenience in Appendix~\ref{sec:declarative}), which satisfies
Giuseppe Castagna's avatar
Giuseppe Castagna committed
455
the property of safety, deduced, as customary, from the properties
Kim Nguyễn's avatar
Kim Nguyễn committed
456
of progress and subject reduction (\emph{cf.} Appendix~\ref{app:soundness}).\svvspace{-.5mm}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
457
\begin{theorem}[type safety]
Giuseppe Castagna's avatar
Giuseppe Castagna committed
458
459
460
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$.
461
\end{theorem}
Kim Nguyễn's avatar
Kim Nguyễn committed
462
\svvspace{-2.1mm}
463
464
465
466