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

typos

parent 86083962
......@@ -19,21 +19,21 @@ instance, the example at the beginning can be
typed by using gradual typing:
\begin{alltt}\color{darkblue}
function foo(x\textcolor{darkred}{ : \dyn}) \{
(typeof(x) === "number")? x++ : x.length
(typeof(x) === "number")? x++ : x.trim()
\}
\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
(typeof(x) === "number")? (\Cast{number}{x})++ : (\Cast{string}{x}).trim()
\}
\end{alltt}
where {\Cast{$t$}{$e$}} is a type-cast.\footnote{Intuitively, \code{\Cast{$t$}{$e$}} is
syntactic sugar for \code{(typeof($e$)==="$t$")? $e$ : (throw "Type
error")}. Not exactly though, since to implement compilation \emph{à la} sound gradual typing we need cast on function types.}
error")}. Not exactly though, since to implement compilation \emph{à la} sound gradual typing we need casts on function types.}
%
We have already seen in the introduction that by using occurrence
typing combined with a union type instead of the gradual type \dyn
typing combined with a union type instead of the gradual type \dyn{}
for parameter annotation, we can avoid the insertion of any cast, at the cost
of some additional type annotations.
But occurrence typing can be used also on the gradually typed code. If we use
......@@ -147,3 +147,7 @@ is $\code{number}$, and it is clear that, if $x$ is given type \code{number},
the function type-checks, thanks to occurrence typing. Thus, after some
simplifications, we can actually deduce the desired type
$(\code{number} \to \code{number}) \land ((\dyn \textbackslash \code{number}) \to \code{number})$.
\beppe{Problem: how to compile functions with intersection types, since their body is typed several distinct types. I see two possible solutions: either merge the casts of the various typings (as we did in the compilation of polymorphic functions for semantic subtyping) or allow just one gradual type in the intersection when a function is explicitly typed (reasonable since, why would you use more gradual types in an intersection?)}
......@@ -58,20 +58,18 @@ judgement can be deduced by the following deduction system
that collects type information on the variable lambda abstracted
(i.e., those in the domain of $\Gamma$, since lambdas are our only
binders):
\begin{mathpar}
\Infer[Var]
{
}
{ \Gamma \vdash x \triangleright\{x \mapsto \{ \Gamma(x) \} \} }
{}
\hfill
\Infer[NonVarIf]
\Infer[Const]
{
}
{ \Gamma \vdash e \triangleright \varnothing }
{e \in \textit{NVI}}
{ \Gamma \vdash c \triangleright \varnothing }
{}
\hfill
\Infer[Abs]
{\Gamma,x:s\vdash e\triangleright\psi}
......@@ -105,17 +103,7 @@ binders):
{\Gamma\vdash \ifty{e}{t}{e_1}{e_2}\triangleright\psi_\circ\cup\psi_1\cup\psi_2}
{}
\end{mathpar}
Where
\begin{enumerate}
\item \textit{NVI} is the set of expressions that are neither
variables nor contains a type case, namely those produced by
the following grammar : $e ::= c ~|~ e~e ~|~ \lambda x:t.e ~|~
(e, e) ~|~ \pi_1 e ~|~ \pi_2 e$
\item $\psi\setminus\{x\}$ is the function defined as $\psi$ but undefined on $x$.
\item $\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, that is :
\begin{displaymath}
(\psi_1\cup \psi_2)(x) = \left\{\begin{array}{ll}
\psi_1 (x) & \text{if~} x\notin
......@@ -125,9 +113,7 @@ Where
\psi_1(x)\cup\psi_2(x) & \text{otherwise}
\end{array}\right.
\end{displaymath}
\end{enumerate}
\noindent And now all we need to do is replace the rule [{\sc Abs}+] with the
\noindent All that remains to do is replace the rule [{\sc Abs}+] with the
following rule
\begin{mathpar}
\Infer[AbsInf+]
......@@ -244,7 +230,3 @@ information).
\beppe{Problem: how to compile functions with intersection types, since their body is typed several distinct types. I see two possible solutions: either merge the casts of the various typings (as we did in the compilation of polymorphic functions for semantic subtyping) or allow just one gradual type in the intersection when a function is explicitly typed (reasonable since, why would you use more gradual types in an intersection?)}
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