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

typos

parent a8a74a09
......@@ -29,7 +29,7 @@ typed by using gradual typing:\vspace{-.4mm}
\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
syntactic sugar for \code{(typeof($e$)==="$t$")\,?\,$e$\,:\,(throw "Type
error")}. Not exactly though, since to implement compilation \emph{à la} sound gradual typing is is necessary to use casts on function types that need special handling.}
error")}. Not exactly though, since to implement compilation \emph{à la} sound gradual typing it is necessary to use casts on function types that need special handling.}
%
We already saw that thanks to occurrence typing we can annotate the parameter \code{x} by \code{number|string} instead of \dyn{} and avoid the insertion of any cast.
But occurrence typing can be used also on the gradually typed code in order to statically detect the insertion of useless casts. Using
......@@ -38,7 +38,7 @@ occurrence typing to type the gradually-typed version of \code{foo} in~\eqref{fo
occurrence of \code{x} at issue is given type \code{number} (the
second cast is still necessary however). But removing only this cast is far
from being satisfactory, since when this function is applied to an integer
there are some casts that still need to be inserted outside of the function.
there are some casts that still need to be inserted outside the function.
The reason is that the compiled version of the function
has type \code{\dyn$\to$number}, that is, it expects an argument of type
\dyn, and thus we have to apply a cast (either to the argument or
......
......@@ -3,7 +3,8 @@ QUESTIONS&ANSWERS
_**ReviewerA:** Are there idioms that are not typeable with Typescript or Flow today that become typeable with the presented system?_
Short answer: no example in Table 1 can be typed by Typescript/Flow/TypedRacket insofar as we "reconstruct" intersections of arrows and, as far as we know, no other type system does it. The cases typeable in the cited languages require the programmer to explicitly annotate the code with the precise intersection type, while our system can type the unannotated code (annotated with $Any$, which is equivalent). As a consequence, even if Flow and Typescript accept `foo` as defined in the very first page of our work, they both fail to type `(foo "Hello").trim()` for which our system correctly infers the type `string`. More importantly, typing the code 6, 7, and 9 in Table 1 is out of reach of the cited systems, even when using the right explicit annotations.
Short answer: no example in Table 1 can be typed by Typescript/Flow/TypedRacket insofar as we "reconstruct" intersections of arrows and, as far as we know, no other type system does it. The cases typeable in the cited languages require the programmer to explicitly annotate the code with the precise intersection type, while our system can type the unannotated code (annotated with $Any$, which is equivalent). As a consequence, even if Flow and Typescript accept `foo` as defined in the very first page of our work, they both fail to type `(foo "Hello").trim()` for which our system correctly infers the type `string`.
More importantly, typing the code 6, 7, and 9 in Table 1 is out of reach of the cited systems, even when using the right explicit annotations.
_**ReviewerB:** why does $gx \in Bool$ under these assumptions leads to $x:Empty$? Since $Int$ is a subtype of $Any$, it should be fine for $x$ to be an $Int$ if $gx \in Bool$. Or is the type of $f$ and $g$ equivalent to $(Int \to Int) \wedge (\neg Int \to Bool)$?_
......
......@@ -30,7 +30,7 @@ type
When $\tau$ is \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 typing the function under the
\code{$\neg\Real$}). Notice that typing the function under the
hypothesis that $\tau$ is \Any,
allows us to capture user-defined discrimination as defined
by~\citet{THF10} since, for instance
......
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