new_system3.tex 11 KB
Newer Older
1
2
3
4
5
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
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
\subsection{Syntax}

\[
\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}
\]

\begin{equation}\label{expressions2}
  \begin{array}{lrclr}
    \textbf{Atomic expr} &a &::=& c\alt x\alt\lambda x:t.e\alt (x,x)
    \alt x x\alt \tcase{x}{t}{e}{e}\alt \pi_i x\\[.3mm]
    \textbf{Expressions} &e &::=& \letexp{x}{a}{e}\alt a \\[.3mm]
    \textbf{Values} &v &::=& c\alt\lambda x:t.e\alt (v,v)\\
  \end{array}
\end{equation}

TODO: Which restrictions on types? (cannot test a precise arrow type, etc)

\subsection{Declarative type system}

\begin{mathpar}
    \Infer[Const]
    { }
    {\Gamma\vdash c:\basic{c}}
    { }
    \quad
    \Infer[Var]
  { }
  { \Gamma \vdash x: \Gamma(x) }
  { x\in\dom\Gamma }
  % \qquad
  % \Infer[Inter]
  % { \Gamma \vdash e:t_1\\\Gamma \vdash e:t_2 }
  % { \Gamma \vdash e: t_1 \wedge t_2 }
  % { }
  \\
  \Infer[Proj]
  {\Gamma \vdash x:\pair{t_1}{t_2}}
  {\Gamma \vdash \pi_i x:t_i}
  { }
  \qquad
  \Infer[Pair]
  {\Gamma \vdash x_1:t_1 \and \Gamma \vdash x_2:t_2}
  {\Gamma \vdash (x_1,x_2):\pair {t_1} {t_2}}
  { }
  \\
  \Infer[App]
  {
    \Gamma \vdash x_1: \arrow {t_1}{t_2}\quad
    \Gamma \vdash x_2: t_1
  }
  { \Gamma \vdash {x_1}{x_2}: t_2 }
  { }
  \\
  \Infer[Case]
  {
  \Gamma\vdash x:t_\circ\\  
  \Gamma\subst{x}{t_\circ\land t} \vdash e_1:t'\\
  \Gamma\subst{x}{t_\circ\land \neg t} \vdash e_2:t'}
  {\Gamma\vdash \tcase {x} t {e_1}{e_2}: t'}
  { }
  \\
  \Infer[Abs]
    {\Gamma,(x:s)\vdash e:t}
    {\Gamma\vdash\lambda x:s.e: t}
    { }
  \qquad
  \Infer[Let]
    {\Gamma\vdash a:t_\circ\\
    \Gamma,(x:t_\circ)\vdash e:t}
    {
    \Gamma\vdash\letexp x a e : t
    }
    { }
  \end{mathpar}

\begin{mathpar}
    \Infer[Subs]
    { \Gamma \vdash e:t\\t\leq t' }
    { \Gamma \vdash e: t' }
    { }
    \qquad
84
    \Infer[EFQ]
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
    { \exists x\in\dom{\Gamma}.\ \Gamma(x)=\Empty }
    { \Gamma \vdash e: t }
    { }
\\
  \Infer[Split]
  {
    \Gamma, (x:t_1)\vdash e: t\\
    \Gamma, (x:t_2)\vdash e: t\\
  }
  {
    \Gamma, (x:t_1\vee t_2)\vdash e: t
  }
  { }
  \Infer[AbsSplit]
  {
    \Gamma\vdash \lambda x:s_1.\ e: t_1\\
    \Gamma\vdash \lambda x:s_2.\ e: t_2\\
  }
  {
    \Gamma\vdash \lambda x:s_1\vee s_2.\ e: t_1\wedge t_2
  }
  { }
\end{mathpar}

109
110
111
TODO: Inter rule needed?\\
TODO: Theorems and proof: no need for rule Inter, etc.

112
113
114
\newpage

\subsection{Algorithmic type system}
115

Mickael Laurent's avatar
Mickael Laurent committed
116
117
118
119
120
121
122
123
124
125
126
127
The elements of $\Gamma\avdash\Gammap\ct e:t$ mean:
\begin{itemize}
  \item $\Gamma$ is the environment: it associates to some variables their associated type,
  and can also associate types to variables that will be declared later in $e$ (in this case,
  it can be seen as an assumption that we can make about the type of a future variable)
  \item $\ct$ is the context in which $e$ is located
  (it is used when backtyping: the whole context is retyped)
  \item $\Gammap$ is an additional environment that maps some "future" variables
  to a type. It can be seen as an assumption we make about the type of a future variable,
  but that hasn't been propagated yet.
\end{itemize}

128
\begin{mathpar}
129
130
\Infer[EFQ]
{\exists x\in\dom\Gamma.\ \Gamma(x)=\Empty}
Mickael Laurent's avatar
Mickael Laurent committed
131
{\Gamma \avdash\Gammap\ct e : \{(\Empty,\Gamma)\}}
132
133
{ }
\qquad
134
135
  \Infer[Const]
  { }
Mickael Laurent's avatar
Mickael Laurent committed
136
  {\Gamma\avdash\Gammap\ct c: \{(\basic{c},\Gamma)\}}
137
138
139
140
  { }
  \quad
  \Infer[Var]
{ }
Mickael Laurent's avatar
Mickael Laurent committed
141
{ \Gamma \avdash\Gammap\ct x: \{(\Gamma(x),\Gamma)\} }
142
143
144
145
{ x\in\dom\Gamma }
\\
\Infer[Proj]
{\Gamma(x)\equiv\pair{t_1}{t_2}}
Mickael Laurent's avatar
Mickael Laurent committed
146
{\Gamma \avdash\Gammap\ct \pi_i x: \{(t_i,\Gamma)\}}
147
148
149
150
{ }
\\
\Infer[Proj*]
{\Gamma(x)\equiv\textstyle\bigvee_{i\in I}\pair{t_i}{s_i}\\
Mickael Laurent's avatar
Mickael Laurent committed
151
\forall i\in I.\ \Gamma\avdash{\Gammap\subst{x}{\pair{t_i}{s_i}}}{[]} \ct[\pi_i x]: \{(u_j,\Gamma_j)\}_{j\in J_i}
152
}
Mickael Laurent's avatar
Mickael Laurent committed
153
{\Gamma \avdash\Gammap\ct \pi_i x: \{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\}}
154
155
156
157
{ }
\\
\Infer[ProjDom]
{\Gamma(x) = t\\
158
159
t\land(\pair{\Any}{\Any})\neq\Empty\\
t\land\neg(\pair{\Any}{\Any})\neq\Empty\\
Mickael Laurent's avatar
Mickael Laurent committed
160
161
\Gamma\avdash{\Gammap\subst{x}{t\land(\pair{\Any}{\Any})}}{[]} \ct[\pi_i x]: \{(u_i,\Gamma_i)\}_{i\in I}\\
\Gamma\avdash{\Gammap\subst{x}{t\land\neg(\pair{\Any}{\Any})}}{[]} \ct[\pi_i x]: \{(u_j,\Gamma_j)\}_{j\in J}
162
}
Mickael Laurent's avatar
Mickael Laurent committed
163
{\Gamma \avdash\Gammap\ct \pi_i x: \{(u_i,\Gamma_i)\}_{i\in I}\cup\{(u_j,\Gamma_j)\}_{j\in J}}
164
165
166
167
{ }
\\
\Infer[Pair]
{ }
Mickael Laurent's avatar
Mickael Laurent committed
168
{\Gamma \avdash\Gammap\ct (x_1,x_2):\{(\pair {\Gamma(x_1)} {\Gamma(x_2)},\Gamma)\}}
169
170
171
172
173
174
175
176
{ }
\\
\Infer[App]
{
  \Gamma(x_1)\equiv \textstyle\bigwedge_{i\in I}\arrow {s_i}{t_i}\\
  \Gamma(x_2)=s\\
  \exists i\in I.\ s\leq s_i
}
Mickael Laurent's avatar
Mickael Laurent committed
177
{ \Gamma \avdash\Gammap\ct {x_1}{x_2}: \{((\textstyle\bigwedge_{i\in I}\arrow {s_i}{t_i}) \circ s,\Gamma)\} }
178
179
180
181
182
183
184
{ }
\\
\Infer[AppR*]
{
  \Gamma(x_1)\equiv \textstyle\bigwedge_{i\in I}\arrow {s_i}{t_i}\\
  \Gamma(x_2)=s\\
  s\leq \textstyle\bigvee_{i\in I}s_i\\
Mickael Laurent's avatar
Mickael Laurent committed
185
  \forall i\in I.\ \Gamma\avdash{\Gammap\subst{x_2}{s\land s_i}}{[]} \ct[{x_1}{x_2}]: \{(u_j,\Gamma_j)\}_{j\in J_i}
186
}
Mickael Laurent's avatar
Mickael Laurent committed
187
{ \Gamma \avdash\Gammap\ct {x_1}{x_2}: \{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\} }
188
189
190
191
192
193
{ }
\\
\Infer[AppRDom]
{
  \Gamma(x_1)\equiv \textstyle\bigwedge_{i\in I}\arrow {s_i}{t_i}\\
  s_\circ=\textstyle\bigvee_{i\in I}s_i\\
194
  \Gamma(x_2)=s\\s\land s_\circ\neq\Empty\\s\land \neg s_\circ\neq\Empty\\
Mickael Laurent's avatar
Mickael Laurent committed
195
196
  \Gamma\avdash{\Gammap\subst{x_2}{s\land s_\circ}}{[]} \ct[{x_1}{x_2}]: \{(u_i,\Gamma_i)\}_{i\in I}\\
  \Gamma\avdash{\Gammap\subst{x_2}{s\land \neg s_\circ}}{[]} \ct[{x_1}{x_2}]: \{(u_j,\Gamma_j)\}_{j\in J}
197
}
Mickael Laurent's avatar
Mickael Laurent committed
198
{ \Gamma \avdash\Gammap\ct {x_1}{x_2}: \{(u_i,\Gamma_i)\}_{i\in I}\cup\{(u_j,\Gamma_j)\}_{j\in J} }
199
200
201
{ }
\\
\Infer[AppL*]
202
{\Gamma(x_1)\equiv\textstyle\bigvee_{i\in I}t_i\leq\arrow{\Empty}{\Any}\\
Mickael Laurent's avatar
Mickael Laurent committed
203
\forall i\in I.\ \Gamma\avdash{\Gammap\subst{x_1}{t_i}}{[]} \ct[{x_1}{x_2}]: \{(u_j,\Gamma_j)\}_{j\in J_i}
204
}
Mickael Laurent's avatar
Mickael Laurent committed
205
{\Gamma \avdash\Gammap\ct {x_1}{x_2}: \{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\}}
206
207
208
{ }
\\
\Infer[AppLDom]
209
{\Gamma(x_1) = t\\t\land (\arrow{\Empty}{\Any})\neq\Empty\\t\land \neg (\arrow{\Empty}{\Any})\neq\Empty\\
Mickael Laurent's avatar
Mickael Laurent committed
210
211
\Gamma\avdash{\Gammap\subst{x_1}{t\land(\arrow{\Empty}{\Any})}}{[]} \ct[{x_1}{x_2}]: \{(u_i,\Gamma_i)\}_{i\in I}\\
\Gamma\avdash{\Gammap\subst{x_1}{t\land\neg(\arrow{\Empty}{\Any})}}{[]} \ct[{x_1}{x_2}]: \{(u_j,\Gamma_j)\}_{j\in J}
212
}
Mickael Laurent's avatar
Mickael Laurent committed
213
{\Gamma \avdash\Gammap\ct {x_1}{x_2}: \{(u_i,\Gamma_i)\}_{i\in I}\cup\{(u_j,\Gamma_j)\}_{j\in J}}
214
{ }
215
216
217
\end{mathpar}

\begin{mathpar}
218
219
220
\Infer[CaseThen]
{
\Gamma(x)=t_\circ\\t_\circ\leq t\\
Mickael Laurent's avatar
Mickael Laurent committed
221
222
\Gamma \avdash\Gammap\ct e_1:\{(u_i,\Gamma_i)\}_{i\in I}}
{\Gamma\avdash\Gammap\ct \tcase {x} t {e_1}{e_2}: \{(u_i,\Gamma_i)\}_{i\in I}}
223
224
225
226
227
{ }
\\
\Infer[CaseElse]
{
\Gamma(x)=t_\circ\\t_\circ\leq \neg t\\
Mickael Laurent's avatar
Mickael Laurent committed
228
229
\Gamma \avdash\Gammap\ct e_2:\{(u_i,\Gamma_i)\}_{i\in I}}
{\Gamma\avdash\Gammap\ct \tcase {x} t {e_1}{e_2}: \{(u_i,\Gamma_i)\}_{i\in I}}
230
231
232
233
{ }
\\
\Infer[Case*]
{\Gamma(x) = t_\circ\\
Mickael Laurent's avatar
Mickael Laurent committed
234
235
\Gamma\avdash{\Gammap\subst{x}{t_\circ\land t}}{[]} \ct[\tcase {x} t {e_1}{e_2}]: \{(u_i,\Gamma_i)\}_{i\in I}\\
\Gamma\avdash{\Gammap\subst{x}{t_\circ\land\neg t}}{[]} \ct[\tcase {x} t {e_1}{e_2}]: \{(u_j,\Gamma_j)\}_{j\in J}
236
}
Mickael Laurent's avatar
Mickael Laurent committed
237
{\Gamma\avdash\Gammap\ct \tcase {x} t {e_1}{e_2}: \{(u_i,\Gamma_i)\}_{i\in I}\cup\{(u_j,\Gamma_j)\}_{j\in J}}
238
{ }
239
240
\end{mathpar}

241
242
243
NOTE: No need to add the case statement to the context in the premises of the \Rule{CaseThen} and \Rule{CaseElse}
rules, because one branch is already unreachable and retyping only occurs with stronger environments.

244
\begin{mathpar}
245
246
247
248
% \Infer[Abs]
%   {\Gamma,(x:s)\vdash e:t}
%   {\Gamma\vdash\lambda x:s.e: t}
%   { }
249
% \\
Mickael Laurent's avatar
Mickael Laurent committed
250
\Infer[LetFirst]
251
  {
Mickael Laurent's avatar
Mickael Laurent committed
252
  \Gamma\avdash\Gammap\ct a:\{(t_i,\Gamma_i)\}_{i\in I}\\
253
  \forall i\in I.\ \Gamma_i,(x:t_i)\avdash\Gammap{\ct[\letexp x a {[]}]} e : S_i
Mickael Laurent's avatar
Mickael Laurent committed
254
  }
Mickael Laurent's avatar
Mickael Laurent committed
255
  {
Mickael Laurent's avatar
Mickael Laurent committed
256
  \Gamma\avdash\Gammap\ct\letexp x a e : \textstyle\bigcup_{i\in I}S_i
257
  }
Mickael Laurent's avatar
Mickael Laurent committed
258
259
260
261
262
263
264
265
266
267
268
269
270
  { x\not\in\dom\Gamma }
\\
\Infer[LetNoRefine]
  {
  \Gamma\avdash{\Gammap\setminus\{x\}}{\ct[\letexp x a {[]}]} e : S
  }
  {
  \Gamma\avdash\Gammap\ct\letexp x a e : S
  }
  { x\in\dom\Gamma \text{ and } (x\not\in\dom\Gammap \text{ or } \Gamma(x)\leq\Gammap(x)) }
\\
\Infer[LetRefine]
  {
271
  \Gamma\bvdash{a}{\Gamma(x)\land\Gammap(x)}\{(t_i,\Gamma_i)\}_{i\in I}\\
Mickael Laurent's avatar
Mickael Laurent committed
272
  \forall i\in I.\ \Gamma\subst{x}{t_i}\avdash{(\Gammap\land\Gamma_i)\setminus\{x\}}{[]} \ct[\letexp x a e] : S_i}
Mickael Laurent's avatar
Mickael Laurent committed
273
274
275
276
  {
  \Gamma\avdash\Gammap\ct\letexp x a e : \textstyle\bigcup_{i\in I} S_i
  }
  { x\in\dom\Gamma \text{ and } x\in\dom\Gammap \text{ and } \Gamma(x) \not\leq \Gammap(x) }
277
\end{mathpar}
278

Mickael Laurent's avatar
Mickael Laurent committed
279
TODO: Check let rule
280
281

TODO: Abs rules
Mickael Laurent's avatar
Mickael Laurent committed
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369

\subsection{Backward typing rules}

\begin{mathpar}
  \Infer[Var]
  { }
  {\Gamma\bvdash x t \{(t, \subst{x}{t})\}}
  { }
\qquad
\Infer[Const]
{ }
{\Gamma\bvdash c t \{(t, \{\})\}}
{ }
\\
  \Infer[Inter]
  {\Gamma\vdash e:t' \\ \Gamma\bvdash e {t\wedge t'} \{(t_i, \Gamma_i)\}_{i\in I}}
  {\Gamma\bvdash e t \{(t_i, \Gamma_i)\}_{i\in I}}
  { }
\qquad
  \Infer[EFQ]
   {\Gamma\bvdash e t \{(t_i,\Gamma_i)\}_{i\in I}\cup\{(\Empty, \Gamma')\}}
   {\Gamma\bvdash e t \{(t_i,\Gamma_i)\}_{i\in I}}
   { }
\\
  \Infer[Pair]
  {
   \forall i\in I.\ \Gamma_1^i = \subst{x_1}{t_i}\\
   \forall i\in I.\ \Gamma_2^i = \subst{x_2}{s_i}
  }
  {\Gamma\bvdash {(x_1,x_2)} {\bigcup_{i\in I}(t_i,s_i)} \bigcup_{i\in I}\{(\pair{t_i}{s_i}, \Gamma_1^i\land\Gamma_2^i)\}}
  { }
  \\
  \Infer[Proj]
  {
    i = 1 \Rightarrow t' = \pair{t}{\Any}\\
    i = 2 \Rightarrow t' = \pair{\Any}{t}
  }
  {\Gamma\bvdash {\pi_i x}{t} \{(t,\subst{x}{\Gamma(x)\land t'})\}}
  { }
\\
  \Infer[App]
  {\Gamma(x_1)\equiv\bigvee_{i\in I}u_i \\ \Gamma(x_2)=t'\\ 
  \forall i\in I.\ u_i\leq \arrow{\neg t_i}{s_i} \text{ with } s_i\land t = \varnothing \\
  \forall i\in I.\ \Gamma_1^i = \subst{x_1}{u_i}\\
  \forall i\in I.\ \Gamma_2^i = \subst{x_2}{t_i\land t'}\\
  \forall i\in I.\ u_i\leq\arrow{(t_i\land t')}{s_i}}
  {
    \Gamma\bvdash {(x_1\ x_2)} {t} \bigcup_{i\in I}\{(s_i, \Gamma_{1}^i\land\Gamma_{2}^i)\}
  }
  { }
\\
  \Infer[Case]
  {
   \Gamma\subst{x}{t_x\land\Gamma(x)} \bvdash {e_1} {t} \{(t_i,\Gamma_1^i)\}_{i\in I}\\
   \Gamma\subst{x}{\neg t_x\land\Gamma(x)} \bvdash {e_2} {t} \{(s_j,\Gamma_2^j)\}_{j\in J}}
  {\Gamma\bvdash {\tcase {x} {t_x} {e_1}{e_2}}{t} \{(t_i,\Gamma_1^i\subst{x}{t_x\land\Gamma_1^i(x)})\}_{i\in I}
  \cup \{(s_j,\Gamma_2^j\subst{x}{\neg t_x\land\Gamma_2^j(x)})\}_{j\in J}}
  { }
  \\
  \Infer[Abs]
  { }
  {\Gamma\bvdash {\lambda x:s.\ e}{t} \{(t,\{\})\}}
  { }
  \qquad
  \Infer[Abs-]
  {t\leq \arrow{t_1}{t_2}\\ t_1\not\leq s}
  {\Gamma\bvdash {\lambda x:s.\ e}{t} \{\}}
  { }
  \\
  \Infer[Let]
  {
    \Gamma\bvdash{e}{t} \{(t_i,\Gamma_i)\}_{i\in I}\\
    \forall i\in I.\ \Gamma\land\Gamma_i\bvdash{a}{\Gamma\land\Gamma_i)(x)} \{(t_i^j,\Gamma_i^j)\}_{j\in J_i}
  }
  {
    \Gamma\bvdash{\letexp{x}{a}{e}}{t} \{(t_i,\Gamma_i\land\Gamma_i^j)\ \alt\ i\in I,\ j\in J_i\}
  }
  { }
\end{mathpar}

NOTE: For the Let rule: as the expression $a$ has been typed before backtyping,
the environment is supposed to already contain a type for $x$.

TODO: Simplify Case rule: as the expression has been typed before backtyping,
$x$ is supposed to be included into $t_x$ or $\neg t_x$.

TODO: Improve Abs rule

Mickael Laurent's avatar
Mickael Laurent committed
370
371
TODO: Is the Inter rule even needed?? (now that result of backtyping must be intersected with the original env)

Mickael Laurent's avatar
Mickael Laurent committed
372
373
374
375
TODO: Algorithmic App, Inter and EFQ rule

TODO: Is the Comp rule needed in this new setting where every application is alone in a let,
and where union-arrow app are backtyped by splitting possibilities?