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

Add comment on type script inference.

parent 2e36cd4f
In this work we presented the core of our analysis of occurrence
typing, extended it to record types and proposed a couple of novel
applications of the theory, namely the reconstruction of
intersection types for unannotated or partially annotated functions and a static analysis to reduce the number of
intersection types for unannotated functions and a static analysis to reduce the number of
casts inserted when compiling gradually-typed programs.
One of the by-products of our work is the ability to define type
predicates such as those used in \cite{THF10} as plain functions and
......
......@@ -14,13 +14,12 @@ can type some of these examples by adding explicit type annotations, the code 6,
7, 9, and 10 in Table~\ref{tab:implem} and, even more, the \code{and\_} and \code{xor\_} functions at the end of this
section are out of reach of current systems, even when using the right
explicit annotations). These and other examples can be tested in the
online toplevel available at
\url{https://occtyping.github.io/}%
\ifsubmission
~(the repository is
anonymized).
\else.
anonymized
\else
\fi
online toplevel available at
\url{https://occtyping.github.io/}%
\input{code_table}
In Table~\ref{tab:implem}, the second column gives a code fragment and the third
column the type deduced by our implementation. Code~1 is a
......@@ -102,12 +101,12 @@ Code~8 allows us to demonstrate the use and typing of record paths. We
model, using open records, the type of DOM objects that represent XML
or HTML documents. Such objects possess a common field
\texttt{nodeType} containing an integer constant denoting the kind of
the node (e.g., \p{9} for the root element, \p{1} for an element node, \p{3} for a text node, \ldots). Depending on the kind, the object will have
the node (e.g., \p{1} for an element node, \p{3} for a text node, \ldots). Depending on the kind, the object will have
different fields and methods. It is common practice to perform a test
on the value of the \texttt{nodeType} field. In dynamic languages such
as JavaScript, the relevant field or method can directly be accessed
after having checked for the appropriate \texttt{nodeType}. In
mainstream statically typed languages, such as Java, a downward cast
as JavaScript, the relevant field can directly be accessed
after having checked for the appropriate \texttt{nodeType}, whereas
in statically typed languages such as Java, a downward cast
from the generic \texttt{Node} type to the expected precise type of
the object is needed. We can see that using the extension presented in
Section~\ref{ssec:struct} we can deduce the correct type for
......@@ -130,7 +129,7 @@ Let us follow the behavior of the
not (but then depends on the type of \texttt{y}). The ``$\worra{}{}$''
operator correctly computes that the type for \texttt{x} in the
``\texttt{then}'' branch is $\True\vee\lnot\True\lor\True\simeq\Any$,
and a similar reasoning holds for \texttt{y}.
and a similar reasoning holds for \texttt{y}.
\fi%%%%%%%%%%%%%%
However, since \texttt{or\_} has type
%\\[.7mm]\centerline{%
......@@ -148,7 +147,7 @@ for which the very same types as in Table~\ref{tab:implem} are deduced.
Last but not least Code~10 (corresponding to our introductory
example~\eqref{nest1}) illustrates the need for iterative refinement of
type environments, as defined in Section~\ref{sec:typenv}. As
explained, a single pass analysis would deduce
explained, a single pass analysis would deduce
for {\tt x}
a type \Int{} from the {\tt f\;x} application and \Any{} from the {\tt g\;x}
application. Here by iterating a second time, the algorithm deduces
......@@ -161,3 +160,14 @@ yielding a result that is at the same time an integer and a Boolean.
This is precisely reflected by the case $\Int\to\Empty$ in the result.
Indeed our {\tt example10} function can be applied to an integer, but
at runtime the application of {\tt f ~x} will diverge.
Although these experiments are still preliminary, they show how the
combination of occurrence typing and set-theoretic types, together
with the type inference for overloaded function types presented in
Section~\ref{sec:refining} allows us to go beyond what languages like
TypeScript and Flow which can only infer single arrow types.
Our refining of overloaded
function is also future proof. Since it ``retypes'' functions
using information gathered by the typing of occurrences in the body,
its precision will improve when we further improve the
our occurrence typing implementation.
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