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

More commentaries on the examples.

parent a7afc2f3
......@@ -33,7 +33,7 @@ let is_bool = fun (x : Any) ->
let is_char = fun (x : Any) ->
if x is Char then true else false
\end{lstlisting}
&\smallskip
&\smallskip
$(\Int\to\Keyw{True})\land(\lnot\Int\to\Keyw{False})$\newline
~\newline\smallskip
$(\Bool\to\Keyw{True})\land(\lnot\Bool\to\Keyw{False})$\newline
......@@ -146,8 +146,8 @@ $(\Int\to\textsf{Empty})\land(\neg\Int\to{}2)$\newline
\texttt{Warning: line 4, 39-40: unreachable expression}
\\\hline
11 & \begin{lstlisting}
atom nil
type Object = Nil | { prototype = Object ..}
atom null
type Object = Null | { prototype = Object ..}
type ObjectWithPropertyL = { l = Any ..}
| { prototype = ObjectWithPropertyL ..}
......
......@@ -79,7 +79,8 @@ $(\lnot \Int \to \String \to 0) \land (\lnot \String \to 0)$
\\\hline
8 & \begin{lstlisting}
let example8 = fun (x : Any) ->
if or_ (is_int x) (is_string x) is True then true else false
if or_ (is_int x) (is_string x) is True then true
else false
\end{lstlisting} &
$(\Int \to \True)\land(\String \to \True)~\land$\newline
$(\lnot(\String\lor\Int)\to \False)$
......
......@@ -2,7 +2,7 @@ We have implemented the algorithmic system $\vdashA$. Our
implementation is written in OCaml and uses CDuce as a library to
provide the semantic subtyping machinery. Besides the type-checking
algorithm defined on the base language, our implementation supports
record types of Section \ref{ssec:struct}) and the refinement of
record types of Section \ref{ssec:struct} and the refinement of
function types
\iflongversion%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
described in Section \ref{sec:refining}. Furthermore, our implementation uses for the inference of arrow types
......@@ -13,19 +13,22 @@ of Section \ref{sec:refining} with the rule of
Appendix~\ref{app:optimize}.
\fi%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
The implementation is rather crude and
consists of 2000 lines of OCaml code, including parsing, type-checking
of programs, and pretty printing of types. We demonstrate the output
of our type-checking implementation in Table~\ref{tab:implem} by
listing some examples none of which can be typed by current
systems (even though some systems such as Flow and TypeScript
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). It should be noted that for all the examples we discuss,
the the time for the type inference process is less than 5ms, hence we do not
report precise timings in the table.
These and other examples can be tested in the
The implementation is rather crude and consists of 2000 lines of OCaml code,
including parsing, type-checking of programs, and pretty printing of types. We
demonstrate the output of our type-checking implementation in
Table~\ref{tab:implem} and Table~\ref{tab:implem2}. Table~\ref{tab:implem} lists
some examples, none of which can be typed by current systems (even though some
systems such as Flow and TypeScript 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). Table~\ref{tab:implem2} allows for a direct comparison of with
\cite{THF10} be giving the type inferred for the fourteen examples given in that
work.
It should be noted that for all the examples we discuss, the the
time for the type inference process is less than 5ms, hence we do not report
precise timings in the table. These and other examples can be tested in the
\ifsubmission
anonymized
\else
......@@ -34,9 +37,7 @@ online toplevel available at
\url{https://occtyping.github.io/}%
\input{code_table}
\input{code_table2}
In Table~\ref{tab:implem}, the second column gives a code fragment and the third
In both tables, the second column gives a code fragment and the third
column the type deduced by our implementation. Code~1 is a
straightforward function similar to our introductory example \code{foo} in (\ref{foo},\ref{foo2}). Here the
programmer annotates the parameter of the function with a coarse type
......@@ -159,8 +160,8 @@ then the rule \Rule{OverApp} applies and \True, \Any, and $\lnot\True$ become ca
\end{alltt}
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
As for Code~10 (corresponding to our introductory
example~\eqref{nest1}), it illustrates the need for iterative refinement of
type environments, as defined in Section~\ref{sec:typenv}. As
explained, a single pass analysis would deduce
for {\tt x}
......@@ -176,6 +177,63 @@ 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.
Code~11 simulates the behaviour of Javascript property resolution, by looking
for a property \texttt{l} either in the object \texttt{o} itself or in the
chained list of its \texttt{prototype} objects. In that example, we first model
prototype chaining by defining a type \texttt{Object} that can be either the
atom \texttt{Null} or any record with a \texttt{prototype} field which contains
(recursively) an \texttt{Object}. To ease the reading, we defined a recursive
type \texttt{ObjectWithPropertyL} which is either a record with a field
\texttt{l} or a record with a prototype of type \texttt{ObjectWithPropertyL}. We
can then define two predicate function \texttt{has\_property\_l} and
\texttt{has\_own\_property\_l} that tests whether an object has a property
through its prototype or directly. Lastly we can define a function
\texttt{get\_property\_l} which directly access the field if it is present, or
recursively search for it through the prototype chain (in our syntax, the
paremeter \texttt{self} allows one to refer to the function itself). Of
particular interest is the type deduced for the two predicate functions. Indeed,
we can see that \texttt{has\_own\_property\_l} is given an overloaded type whose
first argument is in each case a recursive record type that describe precisely
whether \texttt{l} is present at some point in the list or not (recall that
in a record type such as $\orecord{ l=?\Empty }$, indicate that field \texttt{l}
is absent for sure).
\input{code_table2}
In Table~\ref{tab:implem2}, we convert in our syntax the 14 examples of
\cite{THF10} (we tried to complete such examples with neutral code when they
were incomplete in the original paper). Of these 14 examples, Example~1 to 13
depict combinations of type predicates (such as \texttt{is\_int}) used either
directly or through Boolean predicates (such as the \texttt{or\_} function
previously defined). Note that for all examples for which there was no explicit
indication in the original version, we \emph{infer} the type of the function.
Notice also that for Example~6, the goal of the example is to show that indeed,
the function is ill-typed (which our typechecker detects accurately). The
original Example~14 could be written in our syntax with :
\begin{verbatim}
let example14_alt = fun (input : Int | String) ->
fun (extra : (Any, Any)) ->
if (input, is_int (fst extra)) is (Int, True) then
add input (fst extra)
else if is_int (fst extra) is True
then add (strlen input) (fst extra)
else 0
\end{verbatim}
Notice, in the version above the absence of an occurrence of \texttt{input} in
the second \texttt{if} statement. Indeed, if the first test fails, it is either
because \texttt{is\_int (fst extra)} is not \texttt{True} (that is, if
\texttt{fst extra} is not an integer) or because \texttt{input} is not an
integer. Therefore, in our setting, the type information propagated to the
second test is : $\texttt{(input, is\_int (fst extra))} \in \lnot (\Int,
\True)$, that is $\texttt{(input, is\_int (fst extra))} \in (\lnot\Int,
\True)\lor(\Int, \False)$ Therefore, the type of \texttt{input} in the second
branch is of type $(\String\lor\Int) \land (\lnot\Int \lor \int) =
\String\lor\Int$ which is not precise enough. By adding an occurrence of
\texttt{input} in our \texttt{example14\_alt}, we can further restrict its type
typecheck the function. Lifting this limitation through a control-flow analysis
is part of our future work.
Although these experiments are still preliminary, they show how the
combination occurrence typing and set-theoretic types, together
with the type inference for overloaded function types presented in
......
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