language2.tex 45.7 KB
Newer Older
1
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 according to it an expression is well typed or not. 
2
3
4

\subsection{Types}

5
\begin{definition}[Types]\label{def:types} The set of types \types{} is formed by the terms $t$ coinductively produced by the following grammar
6
7
8
9
10
11
12
\[
\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}
\]
and that satisfy the following conditions
\begin{itemize}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
13
14
15
\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
arrow or product type constructors.
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
\end{itemize}
\end{definition}
We use the following abbreviations for types: $
    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$.
In the definition, $b$ ranges over basic types
(\emph{eg}, \Int, \Bool),
$\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). 
It also ensures that the binary relation $\vartriangleright
\,\subseteq\!\types^{2}$ defined by $t_1 \lor t_2 \vartriangleright
t_i$, $t_1 \land t_2 \vartriangleright
Giuseppe Castagna's avatar
Giuseppe Castagna committed
33
t_i$, $\neg t \vartriangleright t$ is Noetherian.
34
This gives an induction principle on $\types$ that we
Giuseppe Castagna's avatar
Giuseppe Castagna committed
35
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.} 
36
37
38
39
40
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
41
by~\citet{Frisch2008} to which the reader may refer for more details. Its formal definition is recalled in Appendix~\ref{} and a detailed description of the algorithm to decide it can be found in~\cite{Cas15}.
42
43
44
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
45
Section~\ref{sec:syntax} right below) that have that type, and that subtyping is set
46
47
48
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
49
type $s$, if their computation terminates, then they return a result of
50
51
52
53
54
55
56
type $t$ (\emph{eg}, $\Empty\to\Any$ is the set of all
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
(\emph{ie}, union, intersection, negation) are interpreted as the
corresponding set-theoretic operators (\emph{eg},~$s\vee t$ is the
57
58
union of the values of the two types). We use $\simeq$ to denote the
symmetric closure of $\leq$: thus $s\simeq t$ means that $s$ and $t$ denote the same set of values and, as such, they are semantically the same type.
59
60
61
62

\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}
63
64
65
\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)
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
\end{array}
\end{equation}
for $i=1,2$. In~\eqref{expressions}, $c$ ranges over constants
(\emph{eg}, \texttt{true}, \texttt{false}, \texttt{1}, \texttt{2},
...) 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)$
denote pairs and $\pi_i e$ their projections; $\tcase{e}{t}{e_1}{e_2}$
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
83
84
t_i$ for all $i\in I$. Every value is associated to a type: the type of $c$ is $\basic c$; the type of
 $\lambda^{\wedge_{i\in I}s_i\to t_i} x.e$ is $\wedge_{i\in I}s_i\to t_i$; and, inductively,
85
86
the type of a pair of values is the product of the types of the
values.
87
88
89



90
\subsection{Dynamic semantics}\label{sec:opsem}
91

Giuseppe Castagna's avatar
Giuseppe Castagna committed
92
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:
93
94
95
96
97
98
99
100
101
102
\[
\begin{array}{rcll}
  (\lambda^{\wedge_{i\in I}s_i\to t_i} x.e)v &\reduces& e\subst x v\\
  \pi_i(v_1,v_2) &\reduces& v_i & i=1,2\\
  \tcase{v}{t}{e_1}{e_2} &\reduces& e_1 &v\in t\\ 
  \tcase{v}{t}{e_1}{e_2} &\reduces& e_2 &v\not\in t\\ 
\end{array}
\]
The semantics of type-cases uses the relation $v\in t$ that we
informally defined in the previous section. We delay its formal
Giuseppe Castagna's avatar
Giuseppe Castagna committed
103
definition to Section~\ref{sec:type-schemes} (where it deals with some corner cases for functional values). Context reductions are
104
105
106
107
108
109
110
defined by the following reduction contexts:
\[
\Cx[] ::= [\,]\alt \Cx e\alt v\Cx \alt (\Cx,e)\alt (v,\Cx)\alt \pi_i\Cx\alt \tcase{\Cx}tee
\]
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']$.
111
112
113

\subsection{Static semantics}

114
While the syntax and reduction semantics are, on the whole, pretty
115
116
standard, for the type system we will have to introduce several
unconventional features that we anticipated in
Giuseppe Castagna's avatar
Giuseppe Castagna committed
117
Section~\ref{sec:challenges} and are at the core of our work. Let
118
119
120
121
122
123
124
125
126
127
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]
      {
128
        \Gamma \vdash e_1: \arrow {t_1}{t_2}\quad
129
130
131
132
133
134
        \Gamma \vdash e_2: t_1
      }
      { \Gamma \vdash {e_1}{e_2}: t_2 }
      { }
  \quad
  \Infer[Abs+]
135
      {{\scriptstyle\forall i\in I}\quad\Gamma,x:s_i\vdash e:t_i}
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
      {
      \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}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
165
These rules are quite standard and do not need any particular explanation besides those already given in Section~\ref{sec:syntax}. Just notice that we used a classic subsumption rule (\emph{ie}, \Rule{Subs}) to embed subtyping in the type system. Let us next focus on the unconventional aspects of our system, from the simplest to the hardest.
166

Giuseppe Castagna's avatar
Giuseppe Castagna committed
167
The first one is that, as explained in
168
169
170
Section~\ref{sec:challenges}, our type assumptions are about
expressions. Therefore, the type environments in our rules, ranged over
by $\Gamma$, map \emph{expressions}---rather than just variables---into
Giuseppe Castagna's avatar
Giuseppe Castagna committed
171
types. This explains why the classic typing rule for variables is replaced by a more general \Rule{Env} rule defined below:\beppe{Changed the name of Occ into Env since it seems more appropriate}
172
173
174
175
176
177
\begin{mathpar}
  \Infer[Env]
      { }
      { \Gamma \vdash e: \Gamma(e) }
      { e\in\dom\Gamma }
  \qquad
178
  \Infer[Inter]
179
180
181
182
      { \Gamma \vdash e:t_1\\\Gamma \vdash e:t_2 }
      { \Gamma \vdash e: t_1 \wedge t_2 }
      { }
\end{mathpar}
183
The \Rule{Env} rule is coupled with the standard intersection introduction rule \Rule{Inter}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
184
which allows us to deduce for a complex expression the intersection of
185
186
187
188
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
189
system, that is, the fact that $\lambda$-abstractions can have negated
Giuseppe Castagna's avatar
Giuseppe Castagna committed
190
arrow types, as long as these negated types do not make the type deduced for the function empty:
191
192
193
\begin{mathpar}
  \Infer[Abs-]
      {\Gamma \vdash \lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:t}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
194
      { \Gamma \vdash\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\neg(t_1\to t_2)  }
195
196
      { (t\wedge\neg(t_1\to t_2))\not\simeq\Empty }
\end{mathpar}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
197
198
199
200
201
202
203
%\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.}
204
As explained in Section~\ref{sec:challenges}, we need to be able to
205
206
207
208
209
210
211
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
Giuseppe Castagna's avatar
Giuseppe Castagna committed
212
of deduction was already present in the system by~\citet{Frisch2008}
213
though it that system this deduction was motivated by the semantics of types rather than, as in our case,
214
215
216
217
218
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
219
instance, consider this simple example of a function that applied to an
220
integer returns its successor and applied to anything else returns
221
\textsf{true}:
222
\[
223
\lambda^{(\Int\to\Int)\wedge(\neg\Int\to\Bool)} x\,.\,\tcase{x}{\Int}{x+1}{\textsf{true}}
224
\]
225
Clearly, the expression above is well typed, but the rule \Rule{Abs+} alone
226
is not enough to type it. In particular, according to \Rule{Abs+} we
227
have to prove that under the hypothesis that $x$ is of type $\Int$ the expression
228
$(\tcase{x}{\Int}{x+1}{\textsf{true}})$ is of type $\Int$, too.  That is, that under the
229
hypothesis that x has type $\Int\wedge\Int$ (we apply occurrence
230
typing) the expression $x+1$ is of type \Int{} (which holds) and that under the
231
hypothesis that $x$ has type $\Int\setminus\Int$, that is $\Empty$
232
233
(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
234
second case of a type-case even if we know that there is no chance that, when $x$ is bound to an integer,
235
236
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
237
avoid this problem (and type the term above) we add the rule
238
239
240
\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:
241
242
243
244
245
246
\begin{mathpar}
  \Infer[Efq]
  { }
  { \Gamma, (e:\Empty) \vdash e': t }
  { }
\end{mathpar}
247
248
249
Once more, this kind of deduction was already present in the system
by~\citet{Frisch2008} to type full fledged overloaded functions,
though it was embedded in the typing rule for the type-case. Here we
Giuseppe Castagna's avatar
Giuseppe Castagna committed
250
need the rule \Rule{Efq}, which is more general, to ensure the
251
property of subject reduction.\beppe{Example?}
252

253
254
255
Finally, there is one last rule in our type system, the one that
implements occurrence typing, that is, the rule for the
type-case:\beppe{Changed to \Rule{If} to \Rule{Case}}
256
257
258
259
260

\begin{mathpar}
    \Infer[Case]
        {\Gamma\vdash e:t_0\\
        %t_0\not\leq \neg t \Rightarrow
261
        \Gamma \evdash e t \Gamma_1 \\ \Gamma_1 \vdash e_1:t'\\
262
        %t_0\not\leq t \Rightarrow
263
        \Gamma \evdash e {\neg t} \Gamma_2 \\ \Gamma_2 \vdash e_2:t'}
264
265
        {\Gamma\vdash \tcase {e} t {e_1}{e_2}: t'}
        { }
266
\end{mathpar}
267
268
269
270
271
272
273
274
275
276
277
278
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.
279

280
All it remains to do is to show how to deduce judgments of the form
281
$\Gamma \evdash e t \Gamma'$. For that we first have to define how
Giuseppe Castagna's avatar
Giuseppe Castagna committed
282
283
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
284
285
286
287
288
289
290
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
the path $\varpi$, that is
291
\[
292
\begin{array}{l}
293
294
295
296
297
298
299
\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\\
300
301
\end{array}\\
\text{undefined otherwise}
302
303
\end{array}
\]
304

305

306
307
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
308
application, $l$ and $r$ for the $l$eft and $r$ight expressions forming a pair,
Giuseppe Castagna's avatar
Giuseppe Castagna committed
309
310
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
under $\lambda$'s (since their type is frozen in their annotations) and type-cases (since they reset the analysis).\beppe{Is it what I wrote here true?}
311

312
The judgments  $\Gamma \evdash e t \Gamma'$ are then deduced by the following two rules: 
313
314
315
316
317
318
319
320
321
322
323
324
\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]
      { }
325
      { \Gamma \evdash e t \Gamma }
326
327
328
      { }
    \qquad
    \Infer[Path]
329
330
      { \pvdash {\Gamma'} e t \varpi:t' \\ \Gamma \evdash e t \Gamma' }
      { \Gamma \evdash e t \Gamma',(\occ e \varpi:t') }
331
      { }
332
\end{mathpar}
333
334
335
336
337
338
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
occurrence $\varpi$ of the expression $e$ being checked, than we can add this
hypothesis to the produced type environment (rule \Rule{Path}). The rule
339
\Rule{Path} uses a (last) auxiliary judgement $\pvdash {\Gamma}  e t
Giuseppe Castagna's avatar
Giuseppe Castagna committed
340
\varpi:t'$ to deduce the type $t'$ of the occurrence $\occ e \varpi$ when
341
342
343
344
345
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
346
judgements of the form $\pvdash {\Gamma}  e t \varpi:t'$ where
347
$\varpi$ is a path to an expression occurring in $e$. This is given by the following set
348
349
350
351
of rules.

\begin{mathpar}
    \Infer[PSubs]
352
353
        { \pvdash \Gamma e t \varpi:t_1 \\ t_1\leq t_2 }
        { \pvdash \Gamma e t \varpi:t_2 }
354
        { }
355
        \qquad
356
    \Infer[PInter]
357
358
        { \pvdash \Gamma e t \varpi:t_1 \\ \pvdash \Gamma e t \varpi:t_2 }
        { \pvdash \Gamma e t \varpi:t_1\land t_2 }
359
        { }
360
361
362
        \\
    \Infer[PTypeof]
        { \Gamma \vdash \occ e \varpi:t' }
363
        { \pvdash \Gamma e t \varpi:t' }
364
365
        { }
        \qquad
366
    \Infer[PEps]
367
        { }
368
        { \pvdash \Gamma e t \epsilon:t }
369
370
371
372
        { }
        \qquad
        \\
    \Infer[PAppR]
373
374
        { \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 }
375
        { t_2\land t_2' \simeq \Empty  }
376
377
        \\
    \Infer[PAppL]
378
379
        { \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}) }
380
381
382
        { }
        \qquad
    \Infer[PPairL]
383
384
        { \pvdash \Gamma e t \varpi:\pair{t_1}{t_2} }
        { \pvdash \Gamma e t \varpi.l:t_1 }
385
386
387
        { }
        \\
    \Infer[PPairR]
388
389
        { \pvdash \Gamma e t \varpi:\pair{t_1}{t_2} }
        { \pvdash \Gamma e t \varpi.r:t_2 }
390
391
392
        { }
        \qquad
    \Infer[PFst]
393
394
        { \pvdash \Gamma e t \varpi:t' }
        { \pvdash \Gamma e t \varpi.f:\pair {t'} \Any }
395
396
397
        { }
        \qquad
    \Infer[PSnd]
398
399
        { \pvdash \Gamma e t \varpi:t' }
        { \pvdash \Gamma e t \varpi.s:\pair \Any {t'} }
400
401
402
        { }
        \qquad
\end{mathpar}
403
404
405
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
406
the deduction $\vdashp$. The rule \Rule{PInter} combined with
407
408
\Rule{PTypeof} allows the system to deduce for an occurrence $\varpi$
the intersection of the static type of $\occ e \varpi$ (deduced by
409
410
411
\Rule{PTypeof}) with the type deduced for $\varpi$ by the other $\vdashp$ rules. The
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$ (\emph{ie},
$\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).
412
The rule \Rule{PApprR} implements occurrence typing for
413
414
415
416
417
418
419
420
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$
(since $t_2\land t_2' \simeq \Empty$), then the argument of this application cannot be of type $t_1$. \Rule{PAppR} performs the
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\_}
421
are straightforward since they state that the $i$-th projection of a pair
Giuseppe Castagna's avatar
Giuseppe Castagna committed
422
that is of type $\pair{t_1}{t_2}$ must be of type $t_i$. So are the last two
423
424
425
426
427
428
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'}$).

This concludes the presentation of our type system, which satisfies
the property of soundness, deduced, as customary, from the properties
429
of progress and subject reduction, whose proofs are given in Appendix~\ref{app:soundness}.
430
\begin{theorem}[soundness]
Giuseppe Castagna's avatar
Giuseppe Castagna committed
431
432
433
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$.
434
\end{theorem}
435
436
437
438
439





440
441
442

\subsection{Algorithmic system}

Giuseppe Castagna's avatar
Giuseppe Castagna committed
443
444
445
446
447
The system we defined in the previous section implements the ideas we
illustrated in the introduction and it is sound. Now the problem is to
decide whether an expression is well typed or not, that is, to find an
algorithm that given a type environment $\Gamma$ and an expression $e$
decides whether there exists a type $t$ such that $\Gamma\vdash e:t$
448
449
is provable. For that we need to solve essentially two problems:
$(i)$~how to handle the fact that it is possible to deduce several
450
types for the same well-typed expression and $(ii)$~how to compute the
451
452
453
454
455
456
457
458
auxiliary deduction system for paths.

Multiple types have two distinct origins each requiring a distinct
technical solution.  The first origin is the rule \Rule{Abs-} by which
it is possible to deduce for every well-typed lambda abstractions
infinitely many types, that is the annotation of the function
intersected with as many negations of arrow types as it is possible
without making the type empty. To handle this multiplicity we use and
459
adapt the technique of \emph{type schemes} defined
460
by~\citet{Frisch2008}. Type schemes---whose definition we recall in  Section~\ref{sec:type-schemes}---are canonical representations of
461
the infinite sets of types of $\lambda$-abstractions. The second origin is due
462
to the presence of structural rules\footnote{\label{fo:rules}In logic, logical rules
Giuseppe Castagna's avatar
Giuseppe Castagna committed
463
464
465
  refer to a particular connective (here, a type constructor, that is,
  either $\to$, or $\times$, or $b$), while identity rules (e.g.,
  axioms and cuts) and structural rules (e.g., weakening and
466
  contraction) do not.} such as \Rule{Subs} and \Rule{Inter}. We
Giuseppe Castagna's avatar
Giuseppe Castagna committed
467
handle it in the classic way: we define an algorithmic system that
468
tracks the miminum type---actually, the minimum \emph{type scheme}---of an
469
470
expression; this system is obtained from the original system by eliminating
the two structural rules and by distributing suitable checks of the subtyping
Giuseppe Castagna's avatar
Giuseppe Castagna committed
471
relation in the remaining rules. To do that in the presence of
472
473
set-theoretic types we need to define some operators on types, which are given
in Section~\ref{sec:typeops}.
Giuseppe Castagna's avatar
Giuseppe Castagna committed
474
475

For what concerns the use of the auxiliary derivation for the $ $
476
477
478
479
judgments, we present in Section~\ref{sec:typenv} an algorithm for
which we prove the property of soundness and a limited form of
completeness. All these notions are then used in the algorithmic typing
system given in Section~\ref{sec:algorules}.
480

Giuseppe Castagna's avatar
Giuseppe Castagna committed
481
482
483
%% \beppe{\begin{enumerate}
%%  \item type of functions -> type schemes
%%   \item elimination rules (app, proj,if) ->operations on types and how to compute them
484
%%   \item not syntax directed: rules Subs, Inter, Env.
Giuseppe Castagna's avatar
Giuseppe Castagna committed
485
486
487
%%   \item Compute the environments for occurrence typing. Algorithm to compute $\Gamma\vdash\Gamma$
%% \end{enumerate}
%% }
488
489


490
\subsubsection{Type schemes}\label{sec:type-schemes}
491
We introduce the new syntactic category of \emph{types schemes} which are the terms~$\ts$ inductively produced by the following grammar.
492
493
494
495
496
\[
\begin{array}{lrcl}
  \textbf{Type schemes} & \ts & ::= & t \alt \tsfun {\arrow t t ; \cdots ; \arrow t t} \alt \ts \tstimes \ts \alt \ts \tsor \ts \alt \tsempty
\end{array}
\]
Giuseppe Castagna's avatar
Giuseppe Castagna committed
497
Type schemes denote sets of types, as formally stated by the following definition:
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
\begin{definition}[Interpretation of type schemes]
  We define the function $\tsint {\_}$ that maps type schemes into sets of types.
  \begin{align*}
    \begin{array}{lcl}
    \tsint t &=& \{s\alt t \leq s\}\\
    \tsint {\tsfunone {t_i} {s_i}_{i=1..n}} &=& \{s\alt
    \exists s_0 = \bigwedge_{i=1..n} \arrow {t_i} {s_i}
    \land \bigwedge_{j=1..m} \neg (\arrow {t_j'} {s_j'}).\ 
    \Empty \not\simeq s_0 \leq s \}\\
    \tsint {\ts_1 \tstimes \ts_2} &=& \{s\alt \exists t_1 \in \tsint {\ts_1}\ 
    \exists t_2 \in \tsint {\ts_2}.\ \pair {t_1} {t_2} \leq s\}\\
    \tsint {\ts_1 \tsor \ts_2} &=& \{s\alt \exists t_1 \in \tsint {\ts_1}\ 
    \exists t_2 \in \tsint {\ts_2}.\ {t_1} \vee {t_2} \leq s\}\\
    \tsint \tsempty &=& \varnothing
    \end{array}
  \end{align*}
\end{definition}
Note that $\tsint \ts$ is closed under subsumption and intersection
516
 and that $\tsempty$, which denotes the
Giuseppe Castagna's avatar
Giuseppe Castagna committed
517
empty set of types is different from $\Empty$ whose interpretation is
518
519
the set of all types.

520
\begin{lemma}[\cite{Frisch2008}]
521
522
523
524
525
526
527
528
529
530
531
532
533
  Let $\ts$ be a type scheme and $t$ a type. It is possible to decide the assertion $t \in \tsint \ts$,
  which we also write $\ts \leq t$.
\end{lemma}

We can now formally define the relation $v\in t$ used in
Section~\ref{sec:opsem} to define the dynamic semantics of
the language. First, we associate each (possibly, not well-typed)
value to a type schema representing the best type information about
the value. By induction on the definition of values: $\tyof c {} =
\basic c$, $\tyof {\lambda^{\wedge_{i\in I}s_i\to t_i} x.e}{}=
\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$.
Giuseppe Castagna's avatar
Giuseppe Castagna committed
534
      
Giuseppe Castagna's avatar
Giuseppe Castagna committed
535
We also need to perform intersections of type schemes so as to intersect the static type of an expression (\emph{ie}, the one deduced by conventional rules) with the one deduced by occurrence typing (\emph{ie}, the one derived by $\vdashp$). 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 scheme with a type: 
536
\begin{lemma}[\cite{Frisch2008}]
Giuseppe Castagna's avatar
Giuseppe Castagna committed
537
538
539
  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}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
540
Finally, given a type schema it is straightforward to choose in its interpretation a type which serves as the canonical representative of the set:
541
542
543
544
545
546
547
548
549
550
551
552
553
554
\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.

  \begin{align*}
    \begin{array}{lcl}
    \tsrep t &=& t\\
    \tsrep {\tsfunone {t_i} {s_i}_{i\in I}} &=& \bigwedge_{i\in I} \arrow {t_i} {s_i}\\
    \tsrep {\ts_1 \tstimes \ts_2} &=& \pair {\tsrep {\ts_1}} {\tsrep {\ts_2}}\\
    \tsrep {\ts_1 \tsor \ts_2} &=& \tsrep {\ts_1} \vee \tsrep {\ts_2}\\
    \tsrep \tsempty && \textit{undefined}
    \end{array}
  \end{align*}
\end{definition}
Note that $\tsrep \ts \in \tsint \ts$.
Giuseppe Castagna's avatar
Giuseppe Castagna committed
555

556

557
\beppe{The explaination that follows is redundant with Section~\ref{sec:ideas}. Harmonize!}
558

Giuseppe Castagna's avatar
bla bla    
Giuseppe Castagna committed
559
\subsubsection{Operators for  type constructors}\label{sec:typeops}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
560
561

In order to define the algorithmic typing of expressions like
562
applications and projections we need to define the operators on
Giuseppe Castagna's avatar
Giuseppe Castagna committed
563
564
565
566
567
568
569
570
571
572
573
574
575
576
types we used in Section~\ref{sec:ideas}. Consider the rule \Rule{App} for applications. It essentially
does three things: $(1)$ it checks that the function has functional
type; $(2)$ it checks that the argument is in the domain of the
function, and $(3)$ it returns the type of the application. In systems
without set-theoretic types these operations are quite
straightforward: $(1)$ corresponds to checking that the function has
an arrow type, $(2)$ corresponds to checking that the argument is in
the domain of the arrow deduced for the function and $(3)$ corresponds
to returning the codomain of that same arrow. With set-theoretic types
things are more difficult since a function can be typed by, say, a
union of intersection of arrows and negations of types. Checking that
the function has a functional type is easy since it corresponds to
checking that it has a type subtype of $\Empty\to\Any$. Determining
its domain and the type of the application is more complicated. For
577
instance, imagine  we have a function of type \code{\(t=(\Int \to \Int)\) \(\wedge\) \((\Bool \to \Bool)\)}, which 
Giuseppe Castagna's avatar
Giuseppe Castagna committed
578
579
580
581
denotes functions that will return an integer if applied to an integer,
and will return a Boolean if applied to a Boolean. 
It is possible to compute the domain of such a type 
(i.e., of the functions of this type), denoted by
Giuseppe Castagna's avatar
Giuseppe Castagna committed
582
\( \dom{t} = \Int \vee \Bool \), 
Giuseppe Castagna's avatar
Giuseppe Castagna committed
583
584
585
586
587
588
589
590
591
592
that is the union of all the possible
input types. But what is the precise return type of such a 
function? It depends on what the argument of such a function is:
either an integer or a Boolean---or both, denoted by the union type
\(\Int\vee\Bool\). This is computed by an operator  we denote by \( \circ \). 
More precisely, we denote by \( t_1\circ t_2\) the type of 
an application of a function of type \(t_1\) to an argument of 
type \(t_2\).
In the example with \code{\(t=(\Int \to \Int)\) \(\wedge\) \((\Bool \to \Bool)\)}, it gives \code{\( t \circ \Int = \Int \)},
\code{\( t \circ \Bool = \Bool \)}, and 
593
\code{\( t \circ (\Int\vee\Bool) = \Int \vee \Bool \)}. In summary, given a functional type $t$ (\emph{ie}, a type $t$ such that $t\leq\Empty\to\Any$) our algorithms will use the following three operators
Giuseppe Castagna's avatar
bla bla    
Giuseppe Castagna committed
594
595
596
\begin{eqnarray}
\dom t & = & \max \{ u \alt t\leq u\to \Any\} 
\\
597
\apply t s & = &\,\min \{ u \alt t\leq s\to u\}
Giuseppe Castagna's avatar
bla bla    
Giuseppe Castagna committed
598
\\
599
\worra t s  & = &\,\min\{u \alt t\circ(\dom t\setminus u)\leq \neg s\}\label{worra}
Giuseppe Castagna's avatar
bla bla    
Giuseppe Castagna committed
600
\end{eqnarray}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
601
602

The first two operators belongs to the theory of semantic subtyping while the last one is new and we described it in Section~\ref{sec:ideas}
Giuseppe Castagna's avatar
bla bla    
Giuseppe Castagna committed
603

Giuseppe Castagna's avatar
Giuseppe Castagna committed
604
We need similar operators for projections since the type $t$ of $e$ in $\pi_i e$ may not be a single product type but, say,  a union of products: all we know is that $t$ must be a subtype of $\pair\Any\Any$. So let $t$ be a type such that $t\leq\pair\Any\Any$, then we define:
Giuseppe Castagna's avatar
bla bla    
Giuseppe Castagna committed
605
606
607
608
\begin{eqnarray}
  \bpl t & = & \min \{ u \alt t\leq \pair u\Any\}\\
  \bpr t & = & \min \{ u \alt t\leq \pair \Any u\}
\end{eqnarray}
609
610
611
612
613
614
615
616
617
618
619
620
All the operators above but $\worra{}{}$ are already present in the
theory of semantic subtyping: the reader can find how to compute them
and how to extend their definition to type schemes in~\cite[Section
  6.11]{Frisch2008}. Below we just show the formula that computes
$\worra t s$ for a $t$ subtype of $\Empty\to\Any$. For that, we use a
result of semantic subtyping that states that every type $t$ is
equivalent to a type in disjunctive normal form and that if
furthermore $t\leq\Empty\to\Any$, then $t \simeq \bigvee_{i\in
  I}\left(\bigwedge_{p\in P_i}(s_p\to t_p)\bigwedge_{n\in
  N_i}\neg(s_n'\to t_n')\right)$ with $\bigwedge_{p\in P_i}(s_p\to
t_p)\bigwedge_{n\in N_i}\neg(s_n'\to t_n') \not\simeq \Empty$ for all
$i$ in $I$. For such a $t$ and any type $s$ then we have:
Giuseppe Castagna's avatar
Giuseppe Castagna committed
621
622
623
624
625
%
\begin{equation}
\worra t s  =  \dom t \wedge\bigvee_{i\in I}\left(\bigwedge_{\{P\subset P_i\alt s\leq \bigvee_{p \in P} \neg t_p\}}\left(\bigvee_{p \in P} \neg s_p\right) \right)
\end{equation}
\beppe{Explain the formula?}
626
The proof that this type satisfies \eqref{worra} is given in the Appendix~\ref{app:worra}.
Giuseppe Castagna's avatar
bla bla    
Giuseppe Castagna committed
627
628
629



630
\subsubsection{Type environments for occurrence typing}\label{sec:typenv}
631

632
633
The last step for our presentation is to define the algorithm for the
deduction of $\Gamma \evdash e t \Gamma'$, that is an algorithm that
634
takes as input $\Gamma$, $e$, and $t$, and returns an environment that
635
636
637
extends $\Gamma$ with hypotheses on the occurrences of $e$ that are
the most general that can be deduced by assuming that $e\in t$ succeeds.

Mickael Laurent's avatar
Mickael Laurent committed
638
639
640
The notation $\tyof{e}{\Gamma}$ denotes the type that can be deduced for the occurence $e$ under the type environment $\Gamma$ in the algorithmic type system given in Section~\ref{sec:algorules}.
That is, $\tyof{e}{\Gamma}=\ts$ if and only if $\Gamma\vdashA e:\ts$ is provable. 

Giuseppe Castagna's avatar
Giuseppe Castagna committed
641
We start by defining the algorithm for each single occurrence, that is for the deduction of $\pvdash \Gamma e t \varpi:t'$. This is obtained by defining two mutually recursive functions $\constrf$ and $\env{}{}$:
642
643
644
645
646
647
648
649
650
651
652
653
\newlength{\sk}
\setlength{\sk}{-1.3pt}
  \begin{eqnarray}
    \constr\epsilon{\Gamma,e,t} & = & t\\[\sk]\label{uno}
    \constr{\varpi.0}{\Gamma,e,t} & = & \neg(\arrow{\env {\Gamma,e,t}{(\varpi.1)}}{\neg \env {\Gamma,e,t} (\varpi)})\\[\sk]\label{due}
    \constr{\varpi.1}{\Gamma,e,t} & = & \worra{\tsrep {\tyof{\occ e{\varpi.0}}\Gamma}}{\env {\Gamma,e,t} (\varpi)}\\[\sk]\label{tre}
    \constr{\varpi.l}{\Gamma,e,t} & = & \bpl{\env {\Gamma,e,t} (\varpi)}\\[\sk]\label{quattro}
    \constr{\varpi.r}{\Gamma,e,t} & = & \bpr{\env {\Gamma,e,t} (\varpi)}\\[\sk]\label{cinque}
    \constr{\varpi.f}{\Gamma,e,t} & = & \pair{\env {\Gamma,e,t} (\varpi)}\Any\\[\sk]\label{sei}
    \constr{\varpi.s}{\Gamma,e,t} & = & \pair\Any{\env {\Gamma,e,t} (\varpi)}\\[1.5mm]\label{sette}
    \env {\Gamma,e,t} (\varpi) & = & \constr \varpi {\Gamma,e,t} \land \tsrep {\tyof {\occ e \varpi} \Gamma}\label{otto}
  \end{eqnarray}
654

655
  
Giuseppe Castagna's avatar
bla bla    
Giuseppe Castagna committed
656
657


658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
%% \[
%% \begin{array}{lcl}
%%   \typep+\epsilon{\Gamma,e,t} & = & t\\
%%   \typep-\epsilon{\Gamma,e,t} & = & \neg t\\
%%   \typep{p}{\varpi.0}{\Gamma,e,t} & = & \neg(\arrow{\Gp p{\Gamma,e,t}{(\varpi.1)}}{\neg \Gp p {\Gamma,e,t} (\varpi)})\\
%%   \typep{p}{\varpi.1}{\Gamma,e,t} & = & \worra{\tsrep {\tyof{\occ e{\varpi.0}}\Gamma}}{\Gp p {\Gamma,e,t} (\varpi)}\\
%%   \typep{p}{\varpi.l}{\Gamma,e,t} & = & \bpl{\Gp p {\Gamma,e,t} (\varpi)}\\
%%   \typep{p}{\varpi.r}{\Gamma,e,t} & = & \bpr{\Gp p {\Gamma,e,t} (\varpi)}\\
%%   \typep{p}{\varpi.f}{\Gamma,e,t} & = & \pair{\Gp p {\Gamma,e,t} (\varpi)}\Any\\
%%   \typep{p}{\varpi.s}{\Gamma,e,t} & = & \pair\Any{\Gp p {\Gamma,e,t} (\varpi)}\\ \\
%%   \Gp p {\Gamma,e,t} (\varpi) & = & \typep p \varpi {\Gamma,e,t} \land \tsrep {\tyof {\occ e \varpi} \Gamma}\\
%%   %\underbrace{\land \tyof {\occ e \varpi} {\Gamma\setminus\{\occ e \varpi\}}}_{\text{if $\occ e \varpi$ is not a variable}}}\\
%% \end{array}
%% \]

%% \begin{align*}
%%   &(\RefineStep p {e,t} (\Gamma))(e') = 
%%     \left\{\begin{array}{ll}
%%       %\tyof {e'} \Gamma \tsand
%%       \bigwedge_{\{\varpi \alt \occ e \varpi \equiv e'\}}
%%       \Gp p {\Gamma,e,t} (\varpi) & \text{if } \exists \varpi.\ \occ e \varpi \equiv e' \\
%%       \Gamma(e') & \text{otherwise, if } e' \in \dom \Gamma\\
%%       \text{undefined} & \text{otherwise}
%%     \end{array}\right.\\
%%   &\Refine p {e,t} \Gamma=\fixpoint_\Gamma (\RefineStep p {e,t})\qquad \text{(for the order $\leq$ on environments, defined in the proofs section)}
%% \end{align*}



Mickael Laurent's avatar
Mickael Laurent committed
687
688
All the functions above are defined if and only if the initial path $\varpi$ is valid for $e$ (i.e. $\occ e{\varpi}$ is defined)
and $e$ is well-typed (so that all $\tyof {\occ e{\varpi}} \Gamma$ encountered are defined).
689

Giuseppe Castagna's avatar
Giuseppe Castagna committed
690
Each case of the definition of the $\constrf$ function corresponds to the
691
692
693
694
application of a logical rule (\emph{cf.} Footnote~\ref{fo:rules}) in
the deduction system for $\vdashp$: case \eqref{uno} corresponds
to the application of \Rule{PEps}; case \eqref{due} implements \Rule{Pappl}
straightforwardly; the implementation of rule \Rule{PAppR} is subtler:
Giuseppe Castagna's avatar
wording    
Giuseppe Castagna committed
695
696
instead of finding the best $t_1$ to subtract (by intersection) from the
static type of the argument, \eqref{tre} finds directly the best type for the argument by
697
applying the $\worra{}{}$ operator to the static types of the function
Giuseppe Castagna's avatar
wording    
Giuseppe Castagna committed
698
and the refined type of the application. The remaining (\ref{quattro}--\ref{sette})
699
700
701
702
cases are the straightforward implementations of the rules
\Rule{PPairL}, \Rule{PPairR}, \Rule{PFst}, and \Rule{PSnd},
respectively.

703
The other recursive function, $\env{}{}$, implements the two structural
704
705
rules \Rule{PInter} and \Rule{PTypeof} by intersecting the type
obtained for $\varpi$ by the logical rules, with the static type
Giuseppe Castagna's avatar
Giuseppe Castagna committed
706
deduced by the type system of the expression occurring at $\varpi$. The
707
remaining structural rule, \Rule{Psubs}, is accounted for by the use
708
of the operators $\worra{}{}$ and $\boldsymbol{\pi}_i$ in
Giuseppe Castagna's avatar
Giuseppe Castagna committed
709
the definition of $\constrf$.
710
711
712
713

\footnote{Note that the definition is well-founded.
This can be seen by analyzing the rule \Rule{Case\Aa}: the definition of $\Refine {e,t} \Gamma$ and  $\Refine {e,\neg t} \Gamma$ use
$\tyof{\occ e{\varpi}}\Gamma$, and this is defined for all $\varpi$ since the first premisses of \Rule{Case\Aa} states that
Giuseppe Castagna's avatar
Giuseppe Castagna committed
714
$\Gamma\vdash e:\ts_0$ (and this is possible only if we were able to deduce under the hypothesis $\Gamma$ the type of every occurrence of $e$.)} It extends the corresponding notation we gave for values in Section~\ref{sec:type-schemes}.
Giuseppe Castagna's avatar
bla bla    
Giuseppe Castagna committed
715

716
717
718
719
720
721
722
723
724
725
726
727
It remains to explain how to compute the environment $\Gamma'$ produced from $\Gamma$ by the deduction system for $\Gamma \evdash e t \Gamma'$. Alas, this is the most delicate part of our algorithm.

In a nutshell what we want to do is to define a function
$\Refine{\_,\_}{\_}$ that takes a type environment $\Gamma$, an
expression $e$ and a type $t$ and returns the best type environment
$\Gamma'$ such that $\Gamma \evdash e t \Gamma'$ holds. By the best
environment we mean the one in which the occurrences of $e$ are
associated to the largest possible types (type environments are
hypotheses so they are contravariant: the larger the type the better
the hypothesis).  Recall that in Section~\ref{sec:challenges} we said
that we want our analysis to be able to capture all the information
available from nested checks. If we gave up such a kind of precision
728
then the definition of $\Refinef$ would be pretty easy: it must map
729
730
731
732
733
734
735
736
737
738
739
740
741
742
each subexpression of $e$ to the intersection of the types deduced by
$\vdashp$ (\emph{ie}, by $\env{}{}$) for each of its occurrences. That
is, for each expression $e'$ occurring in $e$, $\Refine {e,t}\Gamma$
is a type environment that maps $e'$ into $\bigwedge_{\{\varpi \alt
  \occ e \varpi \equiv e'\}} \env {\Gamma,e,t} (\varpi)$. As we
explained in Section~\ref{sec:challenges} the intersection is needed
to apply occurrence typing to expression such as
$\tcase{(x,x)}{\pair{t_1}{t_2}}{e_1}{e_2}$ where some
expressions---here $x$---occur multiple times.

In order to capture most of the type information from nested queries
the rule \Rule{Path} allows the deduction of the type of some
occurrence $\varpi$ to use a type environment $\Gamma'$ that may
contain information about some suboccurrences of $\varpi$. On the
743
744
algorithm this would correspond to apply the $\Refinef$ defined
above to a result of $\Refinef$, and so on. Therefore, ideally our
745
algorithm should compute the type environment as a fixpoint of the
746
function $X\mapsto\Refine{e,t}{X}$. Unfortunately, an iteration of $\Refinef$ may
747
not converge. As an example consider the (dumb) expression $\tcase
Giuseppe Castagna's avatar
Giuseppe Castagna committed
748
749
{x_1x_2}{\Any}{e_1}{e_2}$: if $x_1:\Any\to\Any$, then every iteration of
$\Refinef$ yields for $x_1$ a type strictly more precise than the type deduced in the
750
751
752
previous iteration.

The solution we adopt here is to bound the  number of iterations to some number $n_o$. 
753
754
755
756
757
From a formal point of view, this means to give up the completeness of the algorithm: $\Refinef$ will be complete (\emph{ie}, it will find all solutions) for the deductions of $\Gamma \evdash e t \Gamma'$ of depth at most $n_o$. This is obtained by the following definition of $\Refinef$
\[
\begin{array}{rcl}
  \Refinef_{e,t} \eqdef (\RefineStep{e,t})^{n_o}\\
\text{where }\RefineStep {e,t}(\Gamma)(e') &=&  \left\{\begin{array}{ll}
758
759
760
        %\tyof {e'} \Gamma \tsand
        \bigwedge_{\{\varpi \alt \occ e \varpi \equiv e'\}}
        \env {\Gamma,e,t} (\varpi) & \text{if } \exists \varpi.\ \occ e \varpi \equiv e' \\
Mickael Laurent's avatar
Mickael Laurent committed
761
762
        \Gamma(e') & \text{otherwise, if } e'\in\dom\Gamma\\
        \text{undefined} & \text{otherwise}
763
764
765
      \end{array}\right.
\end{array}
\]
Giuseppe Castagna's avatar
Giuseppe Castagna committed
766
767
Note in particular that $\Refine{e,t}\Gamma$  extends  $\Gamma$ with hypotheses on the expressions occurring in $e$, since
$\dom{\Refine{e,t}\Gamma} = \dom{\RefineStep {e,t}(\Gamma)} = \dom{\Gamma} \cup \{e' \alt \exists \varpi.\ \occ e \varpi \equiv e'\}$.
768
769
770
771
772
773

In other terms, we try to find a fixpoint of $\RefineStep{e,t}$ but we
bound our search to $n_o$ iterations. Since $\RefineStep {e,t}$ is
monotone\footnote{\beppe{explain here the order on $\Gamma$.}}, then
  every iteration yields a better solution. \beppe{Does it make
    sense?}
774
775
776
777
778

While this is unsatisfactory from a formal point of view, in practice
the problem is a very mild one. Divergence may happen only when
refining the type of a function in an application: not only such a
refinement is meaningful only when the function is typed by a union
779
780
781
782
783
784
type (which is quite rare in practice)\footnote{The only impact of
  adding a negated arrow type to the type of a function is when we
  test whether the function has a given arrow type: in practice this
  never happens since programming languages test whether a value
  \emph{is} a function, rather than the type of a given function.},
but also we had to build the expression that causes the divergence in
Giuseppe Castagna's avatar
Giuseppe Castagna committed
785
quite an \emph{ad hoc} way which makes divergence even more unlikely: setting
786
an $n_o$ twice the depth of the syntax tree of the outermost type case
Giuseppe Castagna's avatar
Giuseppe Castagna committed
787
788
should be enough to capture all realistic cases \beppe{can we give an estimate
  based on benchmarking the prototype?}
789

Giuseppe Castagna's avatar
bla bla    
Giuseppe Castagna committed
790
791
792



Giuseppe Castagna's avatar
Giuseppe Castagna committed
793
\subsubsection{Algorithmic typing rules}\label{sec:algorules}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
794
We now have all  notions needed for our typing algorithm, which is defined by the following rules.
Giuseppe Castagna's avatar
Giuseppe Castagna committed
795
\begin{mathpar}
796
  \Infer[Efq\Aa]
Giuseppe Castagna's avatar
Giuseppe Castagna committed
797
798
799
  { }
  { \Gamma, (e:\Empty) \vdashA e': \Empty }
  { \begin{array}{c}\text{\tiny with priority over}\\[-1.8mm]\text{\tiny all the other rules}\end{array}}
Mickael Laurent's avatar
Mickael Laurent committed
800
801
802
803
804
  \qquad
  \Infer[Var\Aa]
      { }
      { \Gamma \vdashA x: \Gamma(x) }
      { x\in\dom\Gamma}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
805
  \\
806
  \Infer[Env\Aa]
Giuseppe Castagna's avatar
Giuseppe Castagna committed
807
808
      { \Gamma\setminus\{e\} \vdashA e : \ts }
      { \Gamma \vdashA e: \Gamma(e) \tsand \ts }
809
      { \begin{array}{c}e\in\dom\Gamma \text{ and }\\[-1mm] e \text{ not a variable}\end{array}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
810
  \qquad
811
  \Infer[Const\Aa]
Giuseppe Castagna's avatar
Giuseppe Castagna committed
812
813
814
815
      { }
      {\Gamma\vdashA c:\basic{c}}
      {c\not\in\dom\Gamma}
   \\
816
  \Infer[Abs\Aa]
Giuseppe Castagna's avatar
Giuseppe Castagna committed
817
818
819
820
821
822
      {\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}
      \\
823
  \Infer[App\Aa]
Giuseppe Castagna's avatar
Giuseppe Castagna committed
824
825
826
827
828
829
830
831
832
      {
        \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}
      \\
833
  \Infer[Case\Aa]
Giuseppe Castagna's avatar
Giuseppe Castagna committed
834
835
836
837
838
839
840
841
842
843
844
845
846
        {\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}$}
847
848
        \Refine {e,t} \Gamma \vdashA e_1 : \ts_1\\
        \Refine {e,\neg t} \Gamma \vdashA e_2 : \ts_2}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
849
        {\Gamma\vdashA \tcase {e} t {e_1}{e_2}: \ts_1\tsor \ts_2}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
850
        %{\ite {e} t {e_1}{e_2}\not\in\dom\Gamma}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
851
        { \tcase {e} {t\!} {\!e_1\!}{\!e_2}\not\in\dom\Gamma}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
852
  \\
853
  \Infer[Proj\Aa]
Giuseppe Castagna's avatar
Giuseppe Castagna committed
854
855
856
857
  {\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}

858
  \Infer[Pair\Aa]
Giuseppe Castagna's avatar
Giuseppe Castagna committed
859
860
861
862
  {\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}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
863
864
865
The side conditions of the rules ensure that the system is syntax
directed, that is, that at most one rule applies when typing a term:
priority is given to \Rule{Eqf\Aa} over all the other rules and to
866
\Rule{Env\Aa} over all remaining logical rules. Type schemes are
Giuseppe Castagna's avatar
Giuseppe Castagna committed
867
868
869
870
871
used to account the type multiplicity stemming from
$\lambda$-abstractions as shown in particular by rule \Rule{Abs\Aa}
(in what follows we use the word ``type'' also for type schemes). The
subsumption rule is no longer in the system. It is replaced by: $(i)$
using a union type in \Rule{Case\Aa}, $(ii)$ checking in \Rule{Abs\Aa}
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
that the body of the function is typed by a subtype of the type
declared in the annotation, and $(iii)$ using type operators and
checking subtyping in the elimination rules \Rule{App\Aa,Proj\Aa}. In
particular, for \Rule{App\Aa} notice that it checks that the type of
the function is a functional type, that the type of the argument is a
subtype of the domain of the function, and then returns the result
type of the application of the two types. The intersection rule is
replaced by the use of type schemes in \Rule{Abs\Aa} and by the rule
\Rule{Env\Aa}. The latter intersects the type deduced for an
expression $e$ by occurrence typing and stored in $\Gamma$ with the
type deduced for $e$ by the logical rules: this is simply obtained by
removing any hypothesis about $e$ from $\Gamma$, so that the deduction
of the type $\ts$ for $e$ cannot but end by a logical rule. Of course
this does not apply when the expression $e$ is a variable, since
an hypothesis in $\Gamma$ is the only way to deduce the type of a
variable, which is a why the algorithm reintroduces the classic rules
for variables.
Giuseppe Castagna's avatar
Giuseppe Castagna committed
889
890
891

The system above satisfies the following properties:\beppe{State here
  soundness and partial completeness}
892