Commit cd2ab74d by Giuseppe Castagna

### small rewording of the intro

parent bae1da77
 ... @@ -56,7 +56,7 @@ function \code{foo} has type ... @@ -56,7 +56,7 @@ function \code{foo} has type one that states that \code{foo} returns a number when it is applied to one that states that \code{foo} returns a number when it is applied to a number and it returns a string when it is applied to a string, so that the type deduced for, say \code{foo(42)} would be \code{number} rather than \code{number|string}. This is a number and it returns a string when it is applied to a string, so that the type deduced for, say \code{foo(42)} would be \code{number} rather than \code{number|string}. This is exactly what the intersection type \code{(number$\to$number) \& exactly what the intersection type \code{(number$\to$number) \& (string$\to$string)} states (intuitively, an expression has an intersection of types if and only if it has all the types of the intersection) and corresponds in Flow to declaring \code{foo} as follows: (string$\to$string)} states (intuitively, an expression has an intersection of type, noted \code{\&}, if and only if it has all the types of the intersection) and corresponds in Flow to declaring \code{foo} as follows: \begin{alltt}\color{darkblue} \begin{alltt}\color{darkblue} var foo : \textcolor{darkred}{(number => number) & (string => string)} = x => \{ var foo : \textcolor{darkred}{(number => number) & (string => string)} = x => \{ (typeof(x) === "number")? x++ : x.trim() \refstepcounter{equation} \mbox{\color{black}\rm(\theequation)}\label{foo2} (typeof(x) === "number")? x++ : x.trim() \refstepcounter{equation} \mbox{\color{black}\rm(\theequation)}\label{foo2} ... @@ -71,8 +71,8 @@ fails. We already saw them at work when we informally typed the else'' ... @@ -71,8 +71,8 @@ fails. We already saw them at work when we informally typed the else'' branch in \code{foo}, for which we assumed that $x$ did \emph{not} have branch in \code{foo}, for which we assumed that $x$ did \emph{not} have type \code{number}---i.e., it had the (negation) type \code{$\neg$number}---and type \code{number}---i.e., it had the (negation) type \code{$\neg$number}---and deduced from it that $x$ then had type \code{string}---i.e., deduced from it that $x$ then had type \code{string}---i.e., \code{(number|string)\&$\neg$number}, that is, \code{(number|string)\&$\neg$number} which is equivalent to the set-theoretic difference \code{(number|string)\textbackslash\,number} which is equivalent to \code{string}. \code{(number|string)\textbackslash\,number} and, thus, to \code{string}. The approaches described above essentially focus on refining the type The approaches described above essentially focus on refining the type of variables that occur in an expression whose type is being tested. They of variables that occur in an expression whose type is being tested. They ... @@ -106,7 +106,7 @@ We focus our study on conditionals that test types and consider the following s ... @@ -106,7 +106,7 @@ We focus our study on conditionals that test types and consider the following s $$\( \ifty{x}{\Int}{x+1}{(\textsf{trim } x)} \ifty{x}{\Int}{x+1}{(\textsf{trim } x)}$$). \)). In particular, in this introduction section we concentrate on applications, since they constitute the most difficult case and many other cases can be reduced to it. A typical example is the expression In particular, in this introduction section we concentrate on applications, since they constitute the most difficult case and many other cases can be reduced to them. A typical example is the expression \label{typical} \label{typical} \ifty{x_1x_2}{t}{e_1}{e_2} \ifty{x_1x_2}{t}{e_1}{e_2} ... @@ -114,7 +114,7 @@ where $x_i$'s denote variables, $t$ is some type, and $e_i$'s are generic expres ... @@ -114,7 +114,7 @@ where $x_i$'s denote variables, $t$ is some type, and $e_i$'s are generic expres Depending the actual $t$ and the static types of $x_1$ and $x_2$ we Depending the actual $t$ and the static types of $x_1$ and $x_2$ we can make type assumptions for $x_1$, for $x_2$ \emph{and} for the application $x_1x_2$ can make type assumptions for $x_1$, for $x_2$ \emph{and} for the application $x_1x_2$ when typing $e_1$ that are different from those we can make when typing when typing $e_1$ that are different from those we can make when typing $e_2$. For instance, suppose $x_1$ is bound to the function \code{foo} defined in \eqref{foo2}. Thus $x_1$ has type, in the syntax of our formalism, $(\Int\to\Int)\wedge(\String\to\String)$. $e_2$. For instance, suppose $x_1$ is bound to the function \code{foo} defined in \eqref{foo2}. Thus $x_1$ has type, $(\Int\to\Int)\wedge(\String\to\String)$ (we used the syntax of the types of Section~\ref{sec:language} where unions and intersections are denoted by $\vee$ and $\wedge$). Then it is not hard to see that the expression\footnote{Most of the following expressions are given just for the sake of example. Determining the type of expressions other than variables is interesting for constructor expressions but less so for destructors such as applications, projections, and selections: any reasonable programmer would not repeat the same application twice, it would store its result in a variable. This becomes meaningful when we introduce constructor such as pairs, as we do for instance in the expression in~\eqref{pair}.} Then it is not hard to see that the expression\footnote{Most of the following expressions are given just for the sake of example. Determining the type of expressions other than variables is interesting for constructor expressions but less so for destructors such as applications, projections, and selections: any reasonable programmer would not repeat the same application twice, it would store its result in a variable. This becomes meaningful when we introduce constructor such as pairs, as we do for instance in the expression in~\eqref{pair}.} % % \label{mezzo} \label{mezzo} ... @@ -210,18 +210,18 @@ well-typed lambda-abstractions, the values of functional type) whose domain, den ... @@ -210,18 +210,18 @@ well-typed lambda-abstractions, the values of functional type) whose domain, den $t_1$; second that $t_2$ must be a subtype of the domain of $t_1$; $t_1$; second that $t_2$ must be a subtype of the domain of $t_1$; third, we also know the type of the application, that is the type third, we also know the type of the application, that is the type that denotes all the values that may result from the application of a that denotes all the values that may result from the application of a function in $t_1$ to an argument in $t_2$ and that we denote by function in $t_1$ to an argument in $t_2$, type that we denote by $t_1\circ t_2$. For instance, if $t_1=\Int\to\Bool$ and $t_2=\Int$, $t_1\circ t_2$. For instance, if $t_1=\Int\to\Bool$ and $t_2=\Int$, then $\dom{t_1}=\Int$ and $t_1\circ t_2 = \Bool$. Notice that, introducing operations such as $\dom{}$ and $\circ$ is redundant when working with simple types, but becomes necessary in the presence of set-theoretic types. If for instance $$t_1=(\Int \to \Int)$$ $$\wedge$$ $$(\Bool \to \Bool)$$---which then $\dom{t_1}=\Int$ and $t_1\circ t_2 = \Bool$. Notice that, introducing operations such as $\dom{}$ and $\circ$ is redundant when working with simple types, but becomes necessary in the presence of set-theoretic types. If for instance $t_1$ is the type of \eqref{foo2}, that is, $$t_1=(\Int{\to}\Int)$$ $$\wedge$$ $$(\String{\to}\String)$$---which denotes functions that will return an integer if applied to an integer and a Boolean if applied to a Boolean---, then we have denotes functions that return an integer if applied to an integer and a string if applied to a string---, then $$\dom{t} = \Int \vee \Bool$$, $$\dom{t} = \Int \vee \String$$, that is the union of all the possible that is the union of all the possible input types. Now the precise return type of such a input types, while the precise return type of such a function depends on what the type of the argument of such a function is: function depends on the type of the argument the function is applied to: either an integer, or a Boolean, or both (i.e., the argument has union type either an integer, or a Boolean, or both (i.e., the argument has union type $$\Int\vee\Bool$$). So we have $$t \circ \Int = \Int$$, $$\Int\vee\String$$). So we have $$t_1 \circ \Int = \Int$$, $$t_1 \circ \Bool = \Bool$$, and $$t_1 \circ \String = \String$$, and $$t_1 \circ (\Int\vee\Bool) = \Int \vee \Bool$$ (see Section~\ref{sec:typeops} for the formal definition of $\circ$). $$t_1 \circ (\Int\vee\String) = \Int \vee \String$$ (see Section~\ref{sec:typeops} for the formal definition of $\circ$). What we want to do What we want to do is to refine the types of $e_1$ and $e_2$ (i.e., $t_1$ and $t_2$) for the cases where the test is to refine the types of $e_1$ and $e_2$ (i.e., $t_1$ and $t_2$) for the cases where the test ... @@ -239,7 +239,7 @@ $t_2$ all the values in $s$ or, equivalently, keep in $t_2$ all the ... @@ -239,7 +239,7 @@ $t_2$ all the values in $s$ or, equivalently, keep in $t_2$ all the values of $\dom{t_1}$ that are not in $s$. Let us implement the second values of $\dom{t_1}$ that are not in $s$. Let us implement the second viewpoint: the set of all elements of $\dom{t_1}$ for which an viewpoint: the set of all elements of $\dom{t_1}$ for which an application \emph{does not} surely give a result in $\neg t$ is application \emph{does not} surely give a result in $\neg t$ is denoted $\worra{t_1}t$ and defined as $\min\{u\leq \dom{t_1}\alt denoted$\worra{t_1}t$(read, worra'') and defined as$\min\{u\leq \dom{t_1}\alt t_1\circ(\dom{t_1}\setminus u)\leq\neg t\}$: it is easy to see that t_1\circ(\dom{t_1}\setminus u)\leq\neg t\}$: it is easy to see that according to this definition $\dom{t_1}\setminus(\worra{t_1} t)$ is according to this definition $\dom{t_1}\setminus(\worra{t_1} t)$ is the largest subset of $\dom{t_1}$ satisfying \eqref{eq1}. Then we can the largest subset of $\dom{t_1}$ satisfying \eqref{eq1}. Then we can ... @@ -292,7 +292,7 @@ obtain ... @@ -292,7 +292,7 @@ obtain and since and since $(\Bool{\vee}\String\to\Bool)\wedge\neg(\String\to\neg\Int)$ is empty $(\Bool{\vee}\String\to\Bool)\wedge\neg(\String\to\neg\Int)$ is empty (because $\String\to\neg\Int$ contains $\Bool{\vee}\String\to\Bool$), (because $\String\to\neg\Int$ contains $\Bool{\vee}\String\to\Bool$), then what we obtain is a strict subtype of $\Int{\vee}\String\to\Int$, namely the functions of type $\Int{\vee}\String\to\Int$ minus those then what we obtain is the left summand, a strict subtype of $\Int{\vee}\String\to\Int$, namely the functions of type $\Int{\vee}\String\to\Int$ minus those that diverge on all \String{} arguments. that diverge on all \String{} arguments. ... @@ -407,5 +407,5 @@ retyping the expression without that assumption (see rule ... @@ -407,5 +407,5 @@ retyping the expression without that assumption (see rule \subsubsection*{Outline} Our presentation proceeds as follows \subsubsection*{Outline} Our presentation proceeds as follows For space reasons several technical definitions and all the proofs are omitted from this presentation and can be found in the Appendix available online. For space reasons several technical definitions and all the proofs are omitted from this presentation and can be found in the appendix available online.
 ... @@ -426,8 +426,7 @@ $\pair{t'}\Any$ (respectively, $\pair\Any{t'}$). ... @@ -426,8 +426,7 @@ $\pair{t'}\Any$ (respectively, $\pair\Any{t'}$). This concludes the presentation of our type system, which satisfies This concludes the presentation of our type system, which satisfies the property of soundness, deduced, as customary, from the properties the property of soundness, deduced, as customary, from the properties of progress and subject reduction, whose proof is given in the of progress and subject reduction, whose proofs are given in Appendix~\ref{app:soundness}. appendix. \begin{theorem}[soundness] \begin{theorem}[soundness] For every expression $e$ such that $\varnothing\vdash e:t$ either $e$ For every expression $e$ such that $\varnothing\vdash e:t$ either $e$ diverges or there diverges or there ... @@ -624,7 +623,7 @@ $i$ in $I$. For such a $t$ and any type $s$ then we have: ... @@ -624,7 +623,7 @@ $i$ in $I$. For such a $t$ and any type $s$ then we have: \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) \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) \beppe{Explain the formula?} \beppe{Explain the formula?} The proof that this type satisfies \eqref{worra} is given in the Appendix~\ref{}. The proof that this type satisfies \eqref{worra} is given in the Appendix~\ref{app:worra}. ... ...
 ... @@ -202,7 +202,7 @@ ... @@ -202,7 +202,7 @@ \\ \\ \end{mathpar} \end{mathpar} \subsection{Proofs for the descriptive type system} \subsection{Proofs for the declarative type system}\label{app:soundness} In this section, the substitutions on expressions that we introduce are up to alpha-renaming and perform only one pass. In this section, the substitutions on expressions that we introduce are up to alpha-renaming and perform only one pass. For instance, if our substitution is $\rho=\subst {(\lambda^t x. x) y} {y}$, we have $((\lambda^t x. x)((\lambda^t z. z) y))\rho = (\lambda^t x. x) y$. For instance, if our substitution is $\rho=\subst {(\lambda^t x. x) y} {y}$, we have $((\lambda^t x. x)((\lambda^t z. z) y))\rho = (\lambda^t x. x) y$. ... @@ -728,7 +728,7 @@ ... @@ -728,7 +728,7 @@ \qed \qed \subsection{Operator $\worra {} {}$} \subsection{Operator $\worra {} {}$}\label{app:worra} In this section, we will use the algorithmic definition of $\worra {} {}$ and show that it is equivalent to its In this section, we will use the algorithmic definition of $\worra {} {}$ and show that it is equivalent to its descriptive definition. descriptive definition. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!