Commit 6b6e6629 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

space savings

parent 3ed41ac9
......@@ -101,15 +101,15 @@ and add the following rules for the new paths:
{ \pvdash \Gamma e t \varpi.u_\ell^2: \proj \ell t'}
{ }
\end{mathpar}
Deriving the algorithm from these rules is then straightforward:
\[
\begin{array}{lcl}
\constr{\varpi.a_\ell}{\Gamma,e,t} & = & \orecord {\ell: \env {\Gamma,e,t} (\varpi)}\\
\constr{\varpi.r_\ell}{\Gamma,e,t} & = & \recdel {(\env {\Gamma,e,t} (\varpi))} \ell + \crecord{\ell \eqq \Any}\\
\constr{\varpi.u_\ell^1}{\Gamma,e,t} & = & \recdel {(\env {\Gamma,e,t} (\varpi))} \ell + \crecord{\ell \eqq \Any}\\
\constr{\varpi.u_\ell^2}{\Gamma,e,t} & = & \proj \ell {(\env {\Gamma,e,t} (\varpi))}
Deriving the algorithm from these rules is then straightforward:\\[1.8mm]
\hspace*{-2mm}\(
\begin{array}{llll}
\constr{\varpi.a_\ell}{\Gamma,e,t} = \orecord {\ell: \env {\Gamma,e,t} (\varpi)}\hspace*{-1mm}&
\constr{\varpi.r_\ell}{\Gamma,e,t} = \recdel {(\env {\Gamma,e,t} (\varpi))} \ell + \crecord{\ell \eqq \Any}\\
\constr{\varpi.u_\ell^2}{\Gamma,e,t} = \proj \ell {(\env {\Gamma,e,t} (\varpi))} &
\constr{\varpi.u_\ell^1}{\Gamma,e,t} = \recdel {(\env {\Gamma,e,t} (\varpi))} \ell + \crecord{\ell \eqq \Any}\\[1.8mm]
\end{array}
\]
\)
%% \beppe{Je ne suis absolument pas convaincu par Ext1. Pour moi il devrait donner le field avec le type de $u_\ell^2$ autrement dit pour moi les regles correctes sont:
%% \begin{mathpar}
%% \Infer[PExt1]
......
......@@ -254,7 +254,6 @@ $\worra{t_1} t$, the set of arguments that when applied to a function
of type $t_1$ \emph{may} return a result in $t$; then we can refine the
type of $e_2$ as $t_2^+ \eqdeftiny t_2\wedge(\worra{t_1} t)$ in the ``then'' branch (we call it the \emph{positive} branch)
and as $t_2^- \eqdeftiny t_2\setminus(\worra{t_1} t)$ in the ``else'' branch (we call it the \emph{negative} branch).
\iflongversion
As a side remark note\marginpar{\tiny\beppe{Remove if space is needed}}
that the set $\worra{t_1} t$ is different from the set of elements that return a
result in $t$ (though it is a supertype of it). To see that, consider
......@@ -264,7 +263,7 @@ Boolean and when applied to an integer return either an integer or a
string; then we have that $\dom{t_1}=\Int\vee\Bool$ and $\worra{t_1}\String=\Int$,
but there is no (non-empty) type that ensures that an application of a
function in $t_1$ will surely yield a $\String$ result.
\fi
Once we have determined $t_2^+$, it is then not very difficult to refine the
type $t_1$ for the positive branch, too. If the test succeeded, then we know two facts: first,
......
......@@ -13,7 +13,7 @@
%\withcommentsfalse
\newif\iflongversion
\longversiontrue
%\longversionfalse
\longversionfalse
\usepackage{setup}
\fancypagestyle{emptyfooter}{
......
As we explained in the introduction, both TypeScript and Flow deduce the type
\code{(number$\vee$string) $\to$ (number$\vee$string)} for the first definition of the function \code{foo} in~\eqref{foo}, and the more precise type
\code{(number$\vee$string) $\to$ (number$\vee$string)} for the first definition of the function \code{foo} in~\eqref{foo}, and the more precise type\vspace{-3pt}
\begin{equation}\label{tyinter}
\code{(number$\to$number)$\,\wedge\,$(string$\to$string)}
\code{(number$\to$number)$\,\wedge\,$(string$\to$string)}\vspace{-3pt}
\end{equation}
can be deduced by these languages only if they are instructed to do so: the
programmer has to explicitly annotate \code{foo} with the
......@@ -15,7 +15,7 @@ even in the absence the annotation given in \eqref{foo2}.
In this section we show how to do it by using the theory of occurrence
typing we developed in the first part of the paper. In particular we
collect the different types the parameter of a function is assigned in
its body to determine a partition of the domain types againt which
its body to determine a partition of the domain types against which
the body of the function is checked. Consider a more involved example
\begin{alltt}\color{darkblue}
function (x \textcolor{darkred}{: \(\tau\)}) \{
......@@ -33,7 +33,7 @@ then the function must be rejected (since it tries to type
hypothesis that $\tau$ is \Any,
allows us to capture user-defined discrimination as defined
by~\citet{THF10} since, for instance
\begin{alltt}\color{darkblue}
\begin{alltt}\color{darkblue}\morecompact
let is_int x = (x\(\in\)Int)? true : false
in if is_int z then z+1 else 42
\end{alltt}
......@@ -57,7 +57,7 @@ the set that contains the types of all the occurrences of $x$ in $e$. This
judgement can be deduced by the following deduction system
that collects type information on the variables that are $\lambda$-abstracted
(i.e., those in the domain of $\Gamma$, since lambdas are our only
binders):
binders):\vspace{-2mm}
\begin{mathpar}
\Infer[Var]
{
......@@ -77,7 +77,7 @@ binders):
\Gamma\vdash\lambda x:s.e\triangleright\psi\setminus\{x\}
}
{}
\vspace{-2mm}\\
\Infer[App]
{
\Gamma \vdash e_1\triangleright\psi_1 \\
......@@ -95,7 +95,7 @@ binders):
{\Gamma \vdash e\triangleright\psi}
{\Gamma \vdash \pi_i e\triangleright\psi}
{}
\vspace{-2mm}\\
\Infer[Case]
{\Gamma\vdash e\triangleright\psi_\circ\\
\Gamma \evdash e t \Gamma_1\\ \Gamma_1\vdash e_1\triangleright\psi_1\\
......@@ -103,7 +103,9 @@ binders):
{\Gamma\vdash \ifty{e}{t}{e_1}{e_2}\triangleright\psi_\circ\cup\psi_1\cup\psi_2}
{}
\end{mathpar}
Where $\psi\setminus\{x\}$ is the function defined as $\psi$ but undefined on $x$ and $\psi_1\cup \psi_2$ denote component-wise union, that is :
Where $\psi\setminus\{x\}$ is the function defined as $\psi$ but undefined on $x$ and $\psi_1\cup \psi_2$ denote component-wise union%
\iflongversion%
, that is :
\begin{displaymath}
(\psi_1\cup \psi_2)(x) = \left\{\begin{array}{ll}
\psi_1 (x) & \text{if~} x\notin
......@@ -113,7 +115,9 @@ Where $\psi\setminus\{x\}$ is the function defined as $\psi$ but undefined on $x
\psi_1(x)\cup\psi_2(x) & \text{otherwise}
\end{array}\right.
\end{displaymath}
\noindent All that remains to do is replace the rule [{\sc Abs}+] with the
\noindent
\else.\fi
All that remains to do is replace the rule [{\sc Abs}+] with the
following rule
\begin{mathpar}
\Infer[AbsInf+]
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment