language2.tex 25.9 KB
Newer Older
Giuseppe Castagna's avatar
Giuseppe Castagna committed
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 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
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
\[
\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}
\item (regularity) the term has a finite number of different sub-terms;
\item (contractivity) every infinite branch of a type contains an infinite number of occurrences of the
arrow type constructor.
\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
t_i$, $\neg t \vartriangleright t$ is Noetherian. 
This gives an induction principle on $\types$ that we
will use without any further explicit reference to the relation.
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
49
50
51
52
53
54
55
56
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
type $s$, if the computation terminates, then they return a result of
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
Giuseppe Castagna's avatar
Giuseppe Castagna committed
83
84
t_i$ for all $i\in I$. Every value is associated to a type: we 
described above the types of constants and abstractions 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 cbv reduction for a $\lambda$-calculus with pairs enriched with a specific rule for type-cases. We have the following  notions of reduction:
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
\[
\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
definition to Section~\ref{sec:type-schemes}. Context reductions are
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
115
116
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
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
178
179
180
181
182
\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}
183
The \Rule{Env} rule is coupled with the classic intersection introduction rule
184
185
186
187
188
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
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 their type 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}
197
As explained in Section~\ref{sec:challenges}, we need to be able to
198
199
200
201
202
203
204
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
205
206
of deduction was already present in the system by~\citet{Frisch2008}
though it that system this deduction was motivated by the semantics of types rather than
207
208
209
210
211
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
212
instance, consider this simple example of a function that applied to an
213
integer returns its successor and applied to anything else returns
214
\textsf{true}:
215
\[
216
\lambda^{(\Int\to\Int)\wedge(\neg\Int\to\Bool)} x\,.\,\tcase{x}{\Int}{x+1}{\textsf{true}}
217
\]
218
Clearly, the expression above is well typed, but the rule \Rule{Abs+} alone
219
is not enough to type it. In particular, according to \Rule{Abs+} we
220
have to prove that under the hypothesis that $x$ is of type $\Int$ the expression
221
$(\tcase{x}{\Int}{x+1}{\textsf{true}})$ is of type $\Int$, too.  That is, that under the
222
hypothesis that x has type $\Int\wedge\Int$ (we apply occurrence
223
typing) the expression $x+1$ is of type \Int{} (which holds) and that under the
224
hypothesis that $x$ has type $\Int\setminus\Int$, that is $\Empty$
225
226
(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
Giuseppe Castagna's avatar
Giuseppe Castagna committed
227
second case of a type-case even if we know that there is no chance that, when $x$ is bound to an $\Int$,
228
229
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
230
avoid this problem (and type the term above) we add the rule
231
232
233
\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:
234
235
236
237
238
239
\begin{mathpar}
  \Infer[Efq]
  { }
  { \Gamma, (e:\Empty) \vdash e': t }
  { }
\end{mathpar}
240
241
242
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
243
need the rule \Rule{Efq}, which is more general, to ensure the
244
property of subject reduction.\beppe{Example?}
245

246
247
248
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}}
249
250
251
252
253

\begin{mathpar}
    \Infer[Case]
        {\Gamma\vdash e:t_0\\
        %t_0\not\leq \neg t \Rightarrow
254
        \Gamma \evdash + e t \Gamma_1 \\ \Gamma_1 \vdash e_1:t'\\
255
        %t_0\not\leq t \Rightarrow
256
        \Gamma \evdash - e t \Gamma_2 \\ \Gamma_2 \vdash e_2:t'}
257
258
        {\Gamma\vdash \tcase {e} t {e_1}{e_2}: t'}
        { }
259
\end{mathpar}
260
The rule \Rule{Case} checks whether the expression $e$, whose type is being tested, is
261
262
well-typed and then performs the occurrence typing analysis that produces
the environments $\Gamma_i$'s under whose hypothesis the expressions
263
$e_i$'s are typed. The production of these environments is represented by the judgment
264
265
$\Gamma \evdash p e t \Gamma_i$ (with $p$ either $+$ or $-$). The
intuition is that when $\Gamma \evdash p e t \Gamma_i$ is provable
Giuseppe Castagna's avatar
Giuseppe Castagna committed
266
267
then $\Gamma_i$ is a version of $\Gamma$ extended with type hypotheses for all
expressions occurring in $e$, type hypotheses that can be deduced
268
269
270
assuming that the test $e\in t$ succeeds (for $p=+$) or fails (for
$p=-$).

271
272
All it remains to do is to show how to deduce judgments of the form
$\Gamma \evdash p e t \Gamma'$. For that we first have to define how
Giuseppe Castagna's avatar
Giuseppe Castagna committed
273
274
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
275
276
277
278
279
280
281
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
282
283
284
285
286
287
288
289
290
291
292
\[
\begin{array}{r@{\downarrow}l@{\quad=\quad}l}
e&\epsilon & e\\
e_0e_1& i.\varpi & \occ{e_i}\varpi\qquad i=0,1\\
(e_0,e_1)& l.\varpi & \occ{e_0}\varpi\\
(e_0,e_1)& r.\varpi & \occ{e_1}\varpi\\
\pi_1 e& f.\varpi & \occ{e}\varpi\\
\pi_2 e& s.\varpi & \occ{e}\varpi\\
\end{array}
\]
undefined otherwise
293

294
295
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
296
application, $l$ and $r$ for the $l$eft and $r$ight expressions forming a pair
Giuseppe Castagna's avatar
Giuseppe Castagna committed
297
and $f$ and $s$ for the argument of a $f$irst or of a $s$econd projection. The judgments  $\Gamma \evdash p e t \Gamma'$ are then deduced by the following two rules: 
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
\begin{mathpar}
%        \Infer[Base]
%            { \Gamma \vdash e':t' }
%            { \Gamma \cvdash p e t e':t' }
%            { }
%            \qquad
%        \Infer[Path]
%            { \pvdash \Gamma p e t \varpi:t_1 \\ \Gamma,(\occ e \varpi:t_1) \cvdash p e t e':t_2 }
%            { \Gamma \cvdash p e t e':t_2 }
%            { }
    \Infer[Base]
      { }
      { \Gamma \evdash p e t \Gamma }
      { }
    \qquad
    \Infer[Path]
      { \pvdash {\Gamma'} p e t \varpi:t' \\ \Gamma \evdash p e t \Gamma' }
      { \Gamma \evdash p e t \Gamma',(\occ e \varpi:t') }
      { }
317
\end{mathpar}
318
319
320
321
322
323
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
324
\Rule{Path} uses a (last) auxiliary judgement $\pvdash {\Gamma} p e t
Giuseppe Castagna's avatar
Giuseppe Castagna committed
325
\varpi:t'$ to deduce the type $t'$ of the occurrence $\occ e \varpi$ when
326
327
328
329
330
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
331
judgements of the form $\pvdash {\Gamma} p e t \varpi:t'$ where
332
$\varpi$ is a path to an expression occurring in $e$. This is given by the following set
333
334
335
336
337
338
339
of rules.

\begin{mathpar}
    \Infer[PSubs]
        { \pvdash \Gamma p e t \varpi:t_1 \\ t_1\leq t_2 }
        { \pvdash \Gamma p e t \varpi:t_2 }
        { }
340
341
342
343
344
        \qquad
    \Infer[PIntersect]
        { \pvdash \Gamma p e t \varpi:t_1 \\ \pvdash \Gamma p e t \varpi:t_2 }
        { \pvdash \Gamma p e t \varpi:t_1\land t_2 }
        { }
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
        \\
    \Infer[PTypeof]
        { \Gamma \vdash \occ e \varpi:t' }
        { \pvdash \Gamma p e t \varpi:t' }
        { }
        \qquad
    \Infer[PEps+]
        { }
        { \pvdash \Gamma + e t \epsilon:t }
        { }
        \qquad
    \Infer[PEps-]
        { }
        { \pvdash \Gamma - e t \epsilon:\neg t }
        { }
        \\
    \Infer[PAppR]
362
        { \pvdash \Gamma p e t \varpi.0:\arrow{t_1}{t_2} \\ \pvdash \Gamma p e t \varpi:t_2'}
363
        { \pvdash \Gamma p e t \varpi.1:\neg t_1 }
364
        { t_2\land t_2' \simeq \Empty  }
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
        \\
    \Infer[PAppL]
        { \pvdash \Gamma p e t \varpi.1:t_1 \\ \pvdash \Gamma p e t \varpi:t_2 }
        { \pvdash \Gamma p e t \varpi.0:\neg (\arrow {t_1} {\neg t_2}) }
        { }
        \qquad
    \Infer[PPairL]
        { \pvdash \Gamma p e t \varpi:\pair{t_1}{t_2} }
        { \pvdash \Gamma p e t \varpi.l:t_1 }
        { }
        \\
    \Infer[PPairR]
        { \pvdash \Gamma p e t \varpi:\pair{t_1}{t_2} }
        { \pvdash \Gamma p e t \varpi.r:t_2 }
        { }
        \qquad
    \Infer[PFst]
        { \pvdash \Gamma p e t \varpi:t' }
        { \pvdash \Gamma p e t \varpi.f:\pair {t'} \Any }
        { }
        \qquad
    \Infer[PSnd]
        { \pvdash \Gamma p e t \varpi:t' }
        { \pvdash \Gamma p e t \varpi.s:\pair \Any {t'} }
        { }
        \qquad
\end{mathpar}
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
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
the deduction $\vdashp$. The rule \Rule{PIntersect} combined with
\Rule{PTypeof} allows the system to deduce for an occurrence $\varpi$
the intersection of the static type of $\occ e \varpi$ (deduced by
\Rule{PTypeof}) and the type deduced for $\varpi$ by the other $\vdashp$ rules. The
rules \Rule{PEps\,$p$} are the starting points of the analysis: when
checking whether $e$ has type $t$ we can assume that $e$ (\emph{ie},
$\occ e\epsilon$) has type $t$ in the positive branch (rule
\Rule{PEps+}) and type $\neg t$ in the negative branch (rule
\Rule{PEps-}). The rule \Rule{PApprR} implements occurrence typing for
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\_}
are straightforward since they state that $i$-th projection of a pair
of type $\pair{t_1}{t_2}$ must be of type $t_i$. So are the last two
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
of progress and subject reduction, whose proof is given in the
appendix.
\begin{theorem}[soundness]
For every expression $e$ such that $\varnothing\vdash e:t$ either there
exists a value $v$ of type $t$ such that $e\reduces^* v$ or $e$
diverges.
\end{theorem}
427
428
429
430
431





432
433
434

\subsection{Algorithmic system}

Giuseppe Castagna's avatar
Giuseppe Castagna committed
435
436
437
438
439
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$
440
441
442
443
444
445
446
447
448
449
450
451
is probable. For that we need to solve essentially three problems:
$(i)$ how to handle the fact that it is possible to deduce several
types for the same well-typed expression $(ii)$ how to compute the
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
extend the technique of \emph{type schemes} defined
Giuseppe Castagna's avatar
Giuseppe Castagna committed
452
by~\citet{Frisch2004}. Type schemes are canonical representations of
453
the infinite set of types of $\lambda$-abstractions and they are
Giuseppe Castagna's avatar
Giuseppe Castagna committed
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
presented in Section~\ref{sec:type-schemes}. The second origin is due
to the presence of structural rules\footnote{In logic, logical rules
  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
  contraction) do not.} such as \Rule{Subs} and \Rule{Intersect}. We
handle it in the classic way: we define an algorithmic system that
tracks the miminum type (actually, minimum type scheme) of an
expression which is obtained from the original system by eliminating
the two structural rules and distrubuting checks of the subtyping
relation in the remaining rules. To do that in the presence of
set-theoretic types we need to define some operators on types, given
in section~\ref{sec:typeops}.

For what concerns the use of the auxiliary derivation for the $ $
judgments, we present in Section~\ref{sec:typenv} an algorithm that we
prove sound \beppe{and complete?}. All these notions are used in the
algorithmic typing system given in Section~\ref{sec:algorules}.
472

473
474
475
476
477
\beppe{\begin{enumerate}
 \item type of functions -> type schemes
  \item elimination rules (app, proj,if) ->operations on types and how to compute them
  \item not syntax directed: rules Subs, Intersect, Env.
  \item Compute the environments for occurrence typing. Algorithm to compute $\Gamma\vdash\Gamma$
478
\end{enumerate}
479
}
480
481


482
\subsubsection{Type schemes}\label{sec:type-schemes}
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
We introduce the new syntactic category of \emph{types schemes} which are the terms $\ts$ produced by the following grammar.
\[
\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}
\]
type schemes denote sets of type, as formally stated by the following definition:
\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
(straightforward induction) and that $\tsempty$, which denotes the
empty set of types is different from $\empty$ whose interpretation is
the set of all types.

\begin{lemma}
  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$.

\beppe{Do we need the next definition and lemma here or they can go in the appendix?

\begin{definition}[Representative]
  We define a function $\tsrep {\_}$ that maps every non-empty type scheme into a type, \textit{representative} of the set of types denoted by the scheme.

  \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$.
\begin{lemma}
  Let $\ts$ be a type scheme and $t$ a type. We can compute a type scheme, written $t \tsand \ts$, such that:
  \[\tsint {t \tsand \ts} = \{s \alt \exists t' \in \tsint \ts.\ t \land t' \leq s \}\]
\end{lemma}
}
548
549
550



Giuseppe Castagna's avatar
Giuseppe Castagna committed
551
\subsubsection{Operators on types}\label{sec:typeops}
552
553
554
555
556
557

\paragraph{Declarative version}

\paragraph{Algorithmic version}


558
\subsubsection{Type environments for occurrence typing}\label{sec:typenv}
559
560
561



Giuseppe Castagna's avatar
Giuseppe Castagna committed
562
\subsection{Algorithmic typing rules}\label{sec:algorules}
563