Commit e2b65eba authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

added gradual typing

parent 19dbd263
......@@ -79,7 +79,6 @@ As an example one can consider
Finally, for what concerns the algorithmic part, the operators $\bpi_{\boldsymbol 1}$ and $\bpi_{\boldsymbol 2}$ are standard in the semantic subtyping framework and they can be computed as described by~\citet{???} (see also~\citep[\S4.4.1]{Cas15} for a detailed description)
\subsubsection{Lists} The work above on pairs is enough for having also the lists. It suffices to encode them as right associative nested pairs, as it is done in the language CDuce. The interesting part is that thanks to the presence of union and recursive types one can type heterogenous lists whose content is described by regular expressions on types as proposed by~\citet{hosoyapierce}.
......@@ -92,7 +91,134 @@ Compare with path expressions of hochstadt
\subsection{Adding gradual types}
\subsection{Integrating gradual typing}
Occurrence typing and gradual typing are two complementary disciplines which have a lot to gain to be integrated. In a sense occurrence typing is a discipline designed to push forward the frontiers after which graudal typing is needed. For instance, the example at the beginning can be typed by using graudal typing:
\begin{alltt}\color{darkblue}
function foo(x\textcolor{darkred}{ : ?}) \{
(typeof(x) === "number")? x++ : x.length
\}
\end{alltt}
Using ``standard'' gradual typing this is compiled into:
\begin{alltt}\color{darkblue}
function foo(x) \{
(typeof(x) === "number")? (\Cast{number}{x})++ : (\Cast{string}{x}).length
\}
\end{alltt}
where {\Cast{$t$}{$e$}} is a type-cast.\footnote{Intuitively, it is
syntactic sugar for \code{(typeof($e$)==="$t$")? $e$ : (throw "Type
error")}}.
%
Using occurrence typing we can avoid inserting the first cast since
thanks to occurrence typing (the second is still necessary). But this
is not completely satisfactory since when this function is applied to
an integer there are some casts that are applied at the application
since the compiled version of the function has type
\code{?$\to$Number}. In order to fully exploit the information of
occurrence typing we have to deduce for the compiled function the type
\code{(Number$\to$Number)$\wedge$((?\textbackslash Number)$\to$Number)} so that the
cast is not inserted when the function is applied to a number. To make
this deduction we need a separate deduction system to collect the type
information generated by the occurrence typing technique we developed
in the previous section (we define a separate deduction system only
for presentation pulposes: in reality this should be merged we the
type deduction system in order to avoid several passes on the parse
trees).
The case of study is the following function
\begin{alltt}\color{darkblue}
function (x \textcolor{darkred}{: \(\tau\)}) \{
(x \(\in\) Real) ?
? \{ (x \(\in\) Int) ? succ x : sqrt x \}
: \{ \(\neg\)x \}
\}
\end{alltt}
first we consider the case without gradual typing. In particular when $\tau$ is \code{Real|Bool} we want to deduce for this function the type
\code{$(\Int\to\Int)\wedge(\Real\backslash\Int\to\Complex)\wedge(\Bool\to\Bool)$}. No cast is inserted, of course.
Then we consider gradual typing and in particular when $\tau$ is \code{?}. Then we want to deduce for this function the type \code{$(\Int\to\Int)\wedge(\Real\backslash\Int\to\Complex)\wedge(?\backslash\Real\to\Bool)$}, and a cast is inserted on the last occurrence of \code x\ which is compiled as \code{\(\neg\)(\Cast{Bool}{x})}.
If we omit $\tau$ and imagine that this is syntactic sugar for \Any\ then the function must be rejected (since it tries to type \code{\(\neg\)x} under the assumption that \code x\ has type \code{$\neg\Real$}. Notice that this last syntactic sugar allows us to capture user-defined discrimintions as defined by ~\citet{THF10} since, for instance
\begin{alltt}\color{darkblue}
let is_int x = (x\(\in\)Int)? true : false
in if is_int z then z+1 else 42
\end{alltt}
the function \code{is\_int} is given type $(\Int\to\True)\wedge(\neg\Int\to\False)$
Here is how to do it first for non-graudal types.
\begin{mathpar}
\Infer[STL]
{
}
{ \Gamma \vdash e \triangleright\{\Gamma\} }
{ e\in STL}
\\
\Infer[Abs]
{\Gamma,x:s\vdash e\triangleright\psi}
{
\Gamma\vdash\lambda x:s.e\triangleright\psi\setminus\{x\}
}
{}
\\
\Infer[App]
{
\Gamma \vdash e_1\triangleright\psi_1 \\
\Gamma\vdash e_2\triangleright\psi_2
}
{ \Gamma \vdash {e_1}{e_2}\triangleright\psi_1\cup\psi_2 }
{}
\\
\Infer[If]
{\Gamma\vdash e\triangleright\psi_\circ\\
\Gamma, \Gamma^+_{\Gamma,e,t}\vdash e_1\triangleright\psi_1\\
\Gamma, \Gamma^-_{\Gamma,e,t}\vdash e_2\triangleright\psi_2}
{\Gamma\vdash \ite e t {e_1}{e_2}\triangleright\psi_\circ\cup\psi_1\cup\psi_2}
{}
\\\end{mathpar}
Where
\begin{enumerate}
\item STL is the set of expressions in simply-typed lambda calculus (no type-case occurring in them),
\item $\{\Gamma\}$ is the function that maps $\Gamma(e)$ into $\{\Gamma(e)\}$ if $e$ is a variable and undefined otherwise
\item $\psi$ ranges on functions that map variables into set of types, $\psi\setminus\{x\}$ is the function defined as $\psi$ but undefined on $x$.
\item \begin{equation}
(\psi_1\cup\psi_2)(x)=
\left\{\begin{array}{ll}
\psi_i(x) &\text{ if }\psi_i(x)\subseteq\psi_{[i+1]_2}(x)\\
\psi_1(x)\cup\psi_2(x) &\text{ otherwise}
\end{array}\right.
\end{equation}
and $\psi_1(x)\subseteq\psi_2(x)\iff \forall\tau\in\psi_1(x),\exists \tau'\in\psi_2(x),\tau\leq\tau'$
\end{enumerate}
And now all we need to do is to modify the typing rule for lambdas as follows
\begin{mathpar}
\Infer[Abs]
{\Gamma,x:t\vdash e\triangleright\psi\and \forall i\in I\quad \Gamma,x:s_i\vdash e:t_i }
{
\Gamma\vdash\lambda x:t.e:\textstyle\bigwedge_{i\in I}s_i\to t_i
}
{\psi(x)=\{s_i\alt i\in I\}}
\end{mathpar}
Note the invariant that the domain of $\psi$ is always equal to the domain of $\Gamma$ restricted to variables.
Finally to take into account gradual typing we need a little bit of extra work, but just in this last typing rule, all the rest remain unchanged.
Let $\tau$ be a gradual type. Define $\tau^*$ as the type obtained from $\tau$ by replacing all covariant occurrences of ? by \Any\ and all contravariant one by empty. Now modify the rule above as follows:
\begin{mathpar}
\Infer[Abs]
{\Gamma,x:\tau^*\vdash e\triangleright\psi\and \Gamma,x:\tau\setminus\textstyle\vee_{i\in I}s_i\vdash e:\tau_\circ\and \forall i\in I\quad \Gamma,x:s_i\vdash e:t_i }
{
\Gamma\vdash\lambda x:\tau.e:\textstyle\bigwedge_{i\in i}s_i\to t_i\wedge((\tau\setminus\vee_{i\in I}s_i)\to \tau_\circ)
}
{\psi(x)=\{s_i\alt i\in I\}}
\end{mathpar}
\subsection{Adding polymorphism}
......@@ -118,9 +244,4 @@ which is well typed for $y:\Int\vee\Bool$
\end{itemize}
Both things that system of~\citet{THF10} can do.
The current formalization relies on type annotations to determine user defined discriminations:
\begin{alltt}
let is_int x = (x\(\in\)Int)? true : false
in if is_int z then z+1 else 42
\end{alltt}
the current formalization rightly deduces the type for \texttt{z+1} only if the programmer has explicitly typed the function \verb|is_int| by the type $(\Int\to\True)\wedge(\neg\Int\to\False)$. The automatic inference of this type for the code above is future work.
......@@ -114,7 +114,7 @@ We define the following algorithmic system (we deduce at most one type for every
\Infer[Abs]
{\Gamma,x:s_i\vdash e:t_i}
{
\Gamma\vdash\lambda^{\wedge_{i\in I}s_i\to t_i}.e:\textstyle\bigwedge_{i\in I}s_i\to t_i
\Gamma\vdash\lambda^{\wedge_{i\in I}s_i\to t_i}x.e:\textstyle\bigwedge_{i\in I}s_i\to t_i
}
{\lambda^{\wedge_{i\in I}s_i\to t_i}.e\not\in\dom\Gamma}
\\
......
......@@ -74,7 +74,10 @@
\newcommand {\True} {\Keyw{True}}
\newcommand {\Int} {\Keyw{Int}}
\newcommand {\Bool} {\Keyw{Bool}}
\newcommand {\Real} {\Keyw{Real}}
\newcommand {\Complex} {\Keyw{Complex}}
\newcommand {\String} {\Keyw{String}}
\newcommand {\Cast}[2]{\tt #2\(\langle\)#1\(\rangle\)}
\newcommand {\ifty}[4]{\ensuremath{\texttt{(}#1\in#2\texttt{)?}#3\texttt{:}#4}}
\newcommand {\code}[1]{\texttt{\color{darkblue}#1}}
\newcommand {\eqdef} {\hbox{\;\;$=$\hspace*{-2.94mm}\raise5pt\hbox{\rm\scriptsize def}\hspace*{1mm}}}
......
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