new_system3.tex 11 KB
 Mickael Laurent committed Nov 11, 2020 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}$ \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} 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  Mickael Laurent committed Nov 11, 2020 84  \Infer[EFQ]  Mickael Laurent committed Nov 11, 2020 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}  Mickael Laurent committed Nov 12, 2020 109 110 111 TODO: Inter rule needed?\\ TODO: Theorems and proof: no need for rule Inter, etc.  Mickael Laurent committed Nov 11, 2020 112 113 114 \newpage \subsection{Algorithmic type system}  Mickael Laurent committed Nov 11, 2020 115   Mickael Laurent committed Nov 14, 2020 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}  Mickael Laurent committed Nov 11, 2020 128 \begin{mathpar}  Mickael Laurent committed Nov 11, 2020 129 130 \Infer[EFQ] {\exists x\in\dom\Gamma.\ \Gamma(x)=\Empty}  Mickael Laurent committed Nov 14, 2020 131 {\Gamma \avdash\Gammap\ct e : \{(\Empty,\Gamma)\}}  Mickael Laurent committed Nov 11, 2020 132 133 { } \qquad  Mickael Laurent committed Nov 11, 2020 134 135  \Infer[Const] { }  Mickael Laurent committed Nov 14, 2020 136  {\Gamma\avdash\Gammap\ct c: \{(\basic{c},\Gamma)\}}  Mickael Laurent committed Nov 11, 2020 137 138 139 140  { } \quad \Infer[Var] { }  Mickael Laurent committed Nov 14, 2020 141 { \Gamma \avdash\Gammap\ct x: \{(\Gamma(x),\Gamma)\} }  Mickael Laurent committed Nov 11, 2020 142 143 144 145 { x\in\dom\Gamma } \\ \Infer[Proj] {\Gamma(x)\equiv\pair{t_1}{t_2}}  Mickael Laurent committed Nov 14, 2020 146 {\Gamma \avdash\Gammap\ct \pi_i x: \{(t_i,\Gamma)\}}  Mickael Laurent committed Nov 11, 2020 147 148 149 150 { } \\ \Infer[Proj*] {\Gamma(x)\equiv\textstyle\bigvee_{i\in I}\pair{t_i}{s_i}\\  Mickael Laurent committed Nov 14, 2020 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}  Mickael Laurent committed Nov 11, 2020 152 }  Mickael Laurent committed Nov 14, 2020 153 {\Gamma \avdash\Gammap\ct \pi_i x: \{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\}}  Mickael Laurent committed Nov 11, 2020 154 155 156 157 { } \\ \Infer[ProjDom] {\Gamma(x) = t\\  Mickael Laurent committed Nov 12, 2020 158 159 t\land(\pair{\Any}{\Any})\neq\Empty\\ t\land\neg(\pair{\Any}{\Any})\neq\Empty\\  Mickael Laurent committed Nov 14, 2020 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}  Mickael Laurent committed Nov 11, 2020 162 }  Mickael Laurent committed Nov 14, 2020 163 {\Gamma \avdash\Gammap\ct \pi_i x: \{(u_i,\Gamma_i)\}_{i\in I}\cup\{(u_j,\Gamma_j)\}_{j\in J}}  Mickael Laurent committed Nov 11, 2020 164 165 166 167 { } \\ \Infer[Pair] { }  Mickael Laurent committed Nov 14, 2020 168 {\Gamma \avdash\Gammap\ct (x_1,x_2):\{(\pair {\Gamma(x_1)} {\Gamma(x_2)},\Gamma)\}}  Mickael Laurent committed Nov 11, 2020 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 committed Nov 14, 2020 177 { \Gamma \avdash\Gammap\ct {x_1}{x_2}: \{((\textstyle\bigwedge_{i\in I}\arrow {s_i}{t_i}) \circ s,\Gamma)\} }  Mickael Laurent committed Nov 11, 2020 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 committed Nov 14, 2020 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}  Mickael Laurent committed Nov 11, 2020 186 }  Mickael Laurent committed Nov 14, 2020 187 { \Gamma \avdash\Gammap\ct {x_1}{x_2}: \{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\} }  Mickael Laurent committed Nov 11, 2020 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\\  Mickael Laurent committed Nov 12, 2020 194  \Gamma(x_2)=s\\s\land s_\circ\neq\Empty\\s\land \neg s_\circ\neq\Empty\\  Mickael Laurent committed Nov 14, 2020 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}  Mickael Laurent committed Nov 11, 2020 197 }  Mickael Laurent committed Nov 14, 2020 198 { \Gamma \avdash\Gammap\ct {x_1}{x_2}: \{(u_i,\Gamma_i)\}_{i\in I}\cup\{(u_j,\Gamma_j)\}_{j\in J} }  Mickael Laurent committed Nov 11, 2020 199 200 201 { } \\ \Infer[AppL*]  Mickael Laurent committed Nov 12, 2020 202 {\Gamma(x_1)\equiv\textstyle\bigvee_{i\in I}t_i\leq\arrow{\Empty}{\Any}\\  Mickael Laurent committed Nov 14, 2020 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}  Mickael Laurent committed Nov 11, 2020 204 }  Mickael Laurent committed Nov 14, 2020 205 {\Gamma \avdash\Gammap\ct {x_1}{x_2}: \{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\}}  Mickael Laurent committed Nov 11, 2020 206 207 208 { } \\ \Infer[AppLDom]  Mickael Laurent committed Nov 12, 2020 209 {\Gamma(x_1) = t\\t\land (\arrow{\Empty}{\Any})\neq\Empty\\t\land \neg (\arrow{\Empty}{\Any})\neq\Empty\\  Mickael Laurent committed Nov 14, 2020 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}  Mickael Laurent committed Nov 11, 2020 212 }  Mickael Laurent committed Nov 14, 2020 213 {\Gamma \avdash\Gammap\ct {x_1}{x_2}: \{(u_i,\Gamma_i)\}_{i\in I}\cup\{(u_j,\Gamma_j)\}_{j\in J}}  Mickael Laurent committed Nov 11, 2020 214 { }  Mickael Laurent committed Nov 12, 2020 215 216 217 \end{mathpar} \begin{mathpar}  Mickael Laurent committed Nov 11, 2020 218 219 220 \Infer[CaseThen] { \Gamma(x)=t_\circ\\t_\circ\leq t\\  Mickael Laurent committed Nov 14, 2020 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}}  Mickael Laurent committed Nov 11, 2020 223 224 225 226 227 { } \\ \Infer[CaseElse] { \Gamma(x)=t_\circ\\t_\circ\leq \neg t\\  Mickael Laurent committed Nov 14, 2020 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}}  Mickael Laurent committed Nov 11, 2020 230 231 232 233 { } \\ \Infer[Case*] {\Gamma(x) = t_\circ\\  Mickael Laurent committed Nov 14, 2020 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}  Mickael Laurent committed Nov 11, 2020 236 }  Mickael Laurent committed Nov 14, 2020 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}}  Mickael Laurent committed Nov 11, 2020 238 { }  Mickael Laurent committed Nov 12, 2020 239 240 \end{mathpar}  Mickael Laurent committed Nov 13, 2020 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.  Mickael Laurent committed Nov 12, 2020 244 \begin{mathpar}  Mickael Laurent committed Nov 11, 2020 245 246 247 248 % \Infer[Abs] % {\Gamma,(x:s)\vdash e:t} % {\Gamma\vdash\lambda x:s.e: t} % { }  Mickael Laurent committed Nov 12, 2020 249 % \\  Mickael Laurent committed Nov 16, 2020 250 \Infer[LetFirst]  Mickael Laurent committed Nov 13, 2020 251  {  Mickael Laurent committed Nov 14, 2020 252  \Gamma\avdash\Gammap\ct a:\{(t_i,\Gamma_i)\}_{i\in I}\\  Mickael Laurent committed Nov 16, 2020 253 254  \forall i\in I.\ \Gamma_i,(x:t_i)\avdash\Gammap\ct\letexp x a e : S_i }  Mickael Laurent committed Nov 14, 2020 255  {  Mickael Laurent committed Nov 16, 2020 256  \Gamma\avdash\Gammap\ct\letexp x a e : \textstyle\bigcup_{i\in I}S_i  Mickael Laurent committed Nov 13, 2020 257  }  Mickael Laurent committed Nov 16, 2020 258 259 260 261 262 263 264 265 266 267 268 269 270 271  { 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] { \Gamma\land\Gammap\bvdash{a}{\Gamma(x)\land\Gammap(x)}\{(t_i,\Gamma_i)\}_{i\in I}\\  Mickael Laurent committed Nov 16, 2020 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 committed Nov 16, 2020 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) }  Mickael Laurent committed Nov 11, 2020 277 \end{mathpar}  Mickael Laurent committed Nov 12, 2020 278   Mickael Laurent committed Nov 16, 2020 279 TODO: Check let rule  Mickael Laurent committed Nov 13, 2020 280 281  TODO: Abs rules  Mickael Laurent committed Nov 16, 2020 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 committed Nov 16, 2020 370 371 TODO: Is the Inter rule even needed?? (now that result of backtyping must be intersected with the original env)  Mickael Laurent committed Nov 16, 2020 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?