Commit 73e043ca by Mickael Laurent

Merge branch 'master' of https://gitlab.math.univ-paris-diderot.fr/beppe/occurrence-typing

parents 307cd361 221ec667
 ... ... @@ -306,7 +306,7 @@ This is essentially what we formalize in Section~\ref{sec:language}, in the type In the previous section we outlined the main ideas of our approach to occurrence typing. However, devil is in the details. So the formalization we give in Section~\ref{sec:language} is not so smooth as we just outlined: we must introduce several auxiliary definitions to handle some corner cases. This section presents by tiny examples the main technical difficulties we had to overcome and the definitions we introduced to handle them. As such it provides a kind of road-map for the technicalities of Section~\ref{sec:language}. \paragraph{Typing occurrences} As it should be clear by now, not only variables but also generic expression are given different types in the then'' and else'' branches of type tests. For instance, in \eqref{two} the expression $x_1x_2$ has type \Int{} in the positive branch and type \Bool{} in the negative one. In this specific case it is possible to deduce these typings from the refined types of the variables (in particular, thanks to the fact that $x_2$ has type \Int{} the positive branch and \Bool{} in the negative one), but this is not possible in general. For instance, consider $x_1:\Int\to(\Int\vee\Bool)$, $x_2:\Int$, and the expression\vspace{-.9mm} \paragraph{Typing occurrences} As it should be clear by now, not only variables but also generic expressions are given different types in the then'' and else'' branches of type tests. For instance, in \eqref{two} the expression $x_1x_2$ has type \Int{} in the positive branch and type \Bool{} in the negative one. In this specific case it is possible to deduce these typings from the refined types of the variables (in particular, thanks to the fact that $x_2$ has type \Int{} the positive branch and \Bool{} in the negative one), but this is not possible in general. For instance, consider $x_1:\Int\to(\Int\vee\Bool)$, $x_2:\Int$, and the expression\vspace{-.9mm} \label{twobis} \ifty{x_1x_2}{\Int}{...x_1x_2...}{...x_1x_2...}\vspace{-.9mm} ... ...