Commit 4bdf9ce9 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

rewritten example14

parent acf31761
......@@ -208,62 +208,6 @@ 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 reproduce in our syntax the 14
archetypal examples of
\citet{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 as:
\begin{alltt}\color{darkblue}
let and_ = fun (x : Any) -> fun (y : Any) -> not_ (or_ (not_ x) (not_ y)) \refstepcounter{equation} \mbox{\color{black}\rm(\theequation)}\label{and+}
let xor_ = fun (x : Any) -> fun (y : Any) -> and_ (or_ x y) (not_ (and_ x y)) \refstepcounter{equation} \mbox{\color{black}\rm(\theequation)}\label{xor+}
\end{alltt}
for which the very same types as in Table~\ref{tab:implem} are deduced.
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}
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
that {\tt x} has type $\Empty$ (i.e., $\textsf{Empty}$), that is, that the first branch can never
be selected (and our implementation warns the user accordingly). In hindsight, the only way for a well-typed overloaded function to have
type $(\Int{\to}\Int)\land(\Any{\to}\Bool)$ is to diverge when the
argument is of type \Int: since this intersection type states that
whenever the input is \Int, {\em both\/} branches can be selected,
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.
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 reproduce in our syntax the 14
......@@ -279,7 +223,14 @@ function whereas in~\cite{THF10} the same examples are always in a
context where the type of identifiers is known or the input type of
function is fully annotated. 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
(which our typechecker detects accurately).
{\definecolor{lightgray}{gray}{.8}
\color{lightgray}OLD VERSION
The original Example~14
could be written in our syntax as:
\begin{alltt}\color{darkblue}
let example14_orig = fun (input : Int | String) ->
......@@ -303,7 +254,67 @@ Notice, in the version above the absence of an occurrence of \texttt{input} in
\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.
}
The original Example~14
could be written in our syntax as:
\begin{alltt}\color{darkblue}
let example14 = fun (input : Int|String) ->
fun (extra : (Any, Any)) ->
if and2_(is_int input , is_int(fst extra)) is True then
add input (fst extra)
else if is_int(fst extra) is True then
add (strlen input) (fst extra)
else 0
\end{alltt}
where \code{and2\_} is the uncurried version of the \code{and\_}
function in \eqref{and+}.
Our system rejects this expression while the system in~\cite{THF10}
correctly infers the the function always return an integer. The reason
why our system rejects it is because the type it deduces for the
occurrence of \code{input} in the 6th line of the code
is \code{Int|String} rather than \code{String} as required by the
application of \code{strlen}. The general reason for this failure is
that, contrary to~\cite{THF10}, our system does not implement an
analysis of the flow of type information. In particular, since the
variable \code{input} does not occur in the condition of the
second \code{if}, then its type is not refined (as it could be).
Indeed, if the first test fails, it is either
because \code{fst\,extra} is not an integer
(i.e., \code{is\_int(fst\,extra)} is not \True) or
because \code{input} is not an integer. Therefore, in
our setting, the type information propagated to the second test for
the pair of the arguments in the first test is :
$\code{(is\_int input , is\_int(fst\,extra))} \in \lnot (\True, \True)$, that
is $\code{(input, is\_int(fst\,extra))} \in
(\lnot\Int, \True)\lor(\Int, \False)$. Since the second test checks
whether \code{is\_int(fst\,extra)} holds or not, then we could deduce
that the following occurrence of \code{input} is of type
$\lnot\Int$. But since \code{input} does not occur in the test, this
is not done. Instead, the type deduced
for \code{input} in the second branch is $(\String\lor\Int) \land
(\lnot\Int \lor \Int) = \String\lor\Int$ which is not precise
enough to type the application \code{strlen\;input}. Although
unsatisfactory, it not difficult
to patch this example in our system: it suffices to test
dummily in the second \code{if} the whole argument of \code{and2\_},
without really checking its first component:
\begin{alltt}\color{darkblue}
let example14_alt = fun (input : Int|String) ->
fun (extra : (Any, Any)) ->
if and2_(is_int input , is_int(fst extra)) is True then
add input (fst extra)
else if (is_int input , is_int(fst extra)) is (Any,True) then
add (strlen input) (fst extra)
else 0
\end{alltt}
Even if the type of \code{is\_int\,input} is not really tested (any
result will have the same effect) its presence in the test triggers the
refinement of the type of the last occurrence of \code{input}, which
type checks with the (quite precise) type shown in the entry 14 of
Table~\ref{tab:implem2}.
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 of occurrence typing and set-theoretic types, together
......
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