Commit d77468ad authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Change ++ to +1.

parent 49b1c618
......@@ -18,13 +18,13 @@ instance, the JavaScript code of~\eqref{foo} and~\eqref{foo2} in the introductio
typed by using gradual typing:%\vspace{-.2mm}
\begin{alltt}\color{darkblue}\morecompact
function foo(x\textcolor{darkred}{ : \pmb{\dyn}}) \{
return (typeof(x) === "number")? x++ : x.trim(); \refstepcounter{equation} \mbox{\color{black}\rm(\theequation)}\label{foo3}
return (typeof(x) === "number")? x+1 : x.trim(); \refstepcounter{equation} \mbox{\color{black}\rm(\theequation)}\label{foo3}
\}\negspace
\end{alltt}
``Standard'' gradual typing inserts two dynamic checks since it compiles the code above into:
\begin{alltt}\color{darkblue}\morecompact
function foo(x) \{
return (typeof(x) === "number")? (\textcolor{darkred}{\Cast{number}{{\color{darkblue}x}}})++ : (\textcolor{darkred}{\Cast{string}{{\color{darkblue}x}}}).trim();
return (typeof(x) === "number")? (\textcolor{darkred}{\Cast{number}{{\color{darkblue}x}}})+1 : (\textcolor{darkred}{\Cast{string}{{\color{darkblue}x}}}).trim();
\}\negspace
\end{alltt}
where {\Cast{$t$}{$e$}} is a type-cast that dynamically checks whether the value returned by $e$ has type $t$.\footnote{Intuitively, \code{\Cast{$t$}{$e$}} is
......
Typescript and Flow are extensions of JavaScript that allow the programmer to specify in the code type annotations used to statically type-check the program. For instance, the following function definition is valid in both languages
\begin{alltt}\color{darkblue}
function foo(x\textcolor{darkred}{ : number | string}) \{
return (typeof(x) === "number")? x++ : x.trim(); \refstepcounter{equation} \mbox{\color{black}\rm(\theequation)}\label{foo}
return (typeof(x) === "number")? x+1 : x.trim(); \refstepcounter{equation} \mbox{\color{black}\rm(\theequation)}\label{foo}
\}
\end{alltt}
Apart from the type annotation (in red) of the function parameter, the above is
standard JavaScript code defining a function that checks whether
its argument is an integer; if it is so, then it returns the argument's successor
(\code{x++}), otherwise it calls the method \code{trim()} of the
(\code{x+1}), otherwise it calls the method \code{trim()} of the
argument. The annotation specifies that the parameter is either a
number or a string (the vertical bar denotes a union type). If this annotation is respected and the function
is applied to either an integer or a string, then the application
......@@ -44,7 +44,7 @@ shows: one flow for integer arguments and another for
strings. Intersection types appear (in limited forms) combined with
occurrence typing both in TypeScript and in Flow and serve to give, among other,
more precise types to functions such as \code{foo}. For instance,
since \code{++} returns an integer and \code{trim()} a string, then our
since \code{ +\,1} returns an integer and \code{trim()} a string, then our
function \code{foo} has type
\code{(number|string)$\to$(number|string)}.
% \footnote{\label{null}Actually,
......@@ -61,7 +61,7 @@ exactly what the \emph{intersection type}
states (intuitively, an expression has an intersection of types, 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}
var foo : \textcolor{darkred}{(number => number) & (string => string)} = x => \{
return (typeof(x) === "number")? x++ : x.trim(); \refstepcounter{equation} \mbox{\color{black}\rm(\theequation)}\label{foo2}
return (typeof(x) === "number")? x+1 : x.trim(); \refstepcounter{equation} \mbox{\color{black}\rm(\theequation)}\label{foo2}
\}
\end{alltt}
For what concerns negation types, they are pervasive in the occurrence
......
......@@ -145,9 +145,9 @@ carries over to this new rule.
This system is enough to type our case study \eqref{foorefine} for the case $\tau$
defined as \code{Real$\vee$Bool}. Indeed, the analysis of the body yields
$\psi(x)=\{\Int,\Real\setminus\Int\}$ for the branch \code{(x\,$\in$\,Int) ? succ\,x : sqrt\,x} and, since
$\psi(x)=\{\Int,\Real\setminus\Int\}$ for the branch \code{(x\,$\in$\,Int) ? x+1 : sqrt(x)} and, since
\code{$(\Bool\vee\Real)\setminus\Real = \Bool$}, yields
$\psi(x)=\{\Bool\}$ for the branch \code{$\neg$x}. So the function
$\psi(x)=\{\Bool\}$ for the branch \code{!x}. So the function
will be checked for the input types $\Int$, $\Real\setminus\Int$, and
\Bool, yielding the expected result.
......
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