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

made some rewording

parent d023dcea
...@@ -52,7 +52,7 @@ let or_ = fun (x : Any) -> fun (y: Any) -> ...@@ -52,7 +52,7 @@ let or_ = fun (x : Any) -> fun (y: Any) ->
if x is True then true if x is True then true
else if y is True then true else false else if y is True then true else false
\end{lstlisting} \end{lstlisting}
&\smallskip\vfill &\vfill
$(\True\to\textsf{Any}\to\True)\land(\textsf{Any}\to\True\to\True)\;\land$\newline $(\True\to\textsf{Any}\to\True)\land(\textsf{Any}\to\True\to\True)\;\land$\newline
$(\lnot\True\to\lnot\True\to\False)$ $(\lnot\True\to\lnot\True\to\False)$
\\\hline \\\hline
......
We have implemented the algorithmic system $\vdashA$. Our We have implemented the algorithmic system $\vdashA$ we presented in Section~\ref{sec:algorules}. Our
implementation is written in OCaml and uses CDuce as a library to implementation is written in OCaml and uses CDuce as a library to
provide the semantic subtyping machinery. Besides the type-checking provide the semantic subtyping machinery. Besides the type-checking
algorithm defined on the base language, our implementation supports algorithm defined on the base language, our implementation supports
record types of Section \ref{ssec:struct} and the refinement of the record types and expressions of Section \ref{ssec:struct} and the refinement of
function types function types
\iflongversion%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \iflongversion%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
described in Section \ref{sec:refining}. Furthermore, our implementation uses for the inference of arrow types described in Section \ref{sec:refining}. Furthermore, our implementation uses for the inference of arrow types
...@@ -17,16 +17,17 @@ The implementation is rather crude and consists of 2000 lines of OCaml code, ...@@ -17,16 +17,17 @@ 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 including parsing, type-checking of programs, and pretty printing of types. We
demonstrate the output of our type-checking implementation in demonstrate the output of our type-checking implementation in
Table~\ref{tab:implem} and Table~\ref{tab:implem2}. Table~\ref{tab:implem} lists 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 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 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} 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 and, even more, the \code{and\_} and \code{xor\_} functions given
in \eqref{and+} and \eqref{xor+} later in this
section are out of reach of current systems, even when using the right explicit 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 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 \cite{THF10} be giving the type inferred for the fourteen examples given in that
work. work.
It should be noted that for all the examples we discuss, the the It should be noted that for all the examples we present, the
time for the type inference process is less than 5ms, hence we do not report 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 precise timings in the table. These and other examples can be tested in the
\ifsubmission \ifsubmission
...@@ -38,16 +39,22 @@ online toplevel available at ...@@ -38,16 +39,22 @@ online toplevel available at
\input{code_table} \input{code_table}
In both tables, 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 column the type deduced by our implementation as is (we
straightforward function similar to our introductory example \code{foo} in (\ref{foo},\ref{foo2}). Here the pretty printed it but we did not alter the output). Code~1 is a
straightforward function similar to our introductory
example \code{foo} in (\ref{foo}) and (\ref{foo2}) where \code{incr}
is the successor function and \code{lneg} the logical negation for
Booleans. Here the
programmer annotates the parameter of the function with a coarse type programmer annotates the parameter of the function with a coarse type
$\Int\vee\Bool$. Our implementation first type-checks the body of the $\Int\vee\Bool$. Our implementation first type-checks the body of the
function under this assumption, but doing so it collects that the type of function under this assumption, but doing so it collects that the type of
$\texttt{x}$ is specialized to \Int{} in the ``then'' case and to \Bool{} $\texttt{x}$ is specialized to \Int{} in the ``then'' case and to \Bool{}
in the ``else'' case. The function is thus type-checked twice more in the ``else'' case. The function is thus type-checked twice more
under each hypothesis for \texttt{x}, yielding the precise type under each hypothesis for \texttt{x}, yielding the precise type
$(\Int\to\Int)\land(\Bool\to\Bool)$. Note that w.r.t.\ rule \Rule{AbsInf+} of Section~\ref{sec:refining}, our implementation improved the output of the computed $(\Int\to\Int)\land(\Bool\to\Bool)$. Note that w.r.t.\
type. Indeed, using rule~[{\sc AbsInf}+] we would obtain the rule \Rule{AbsInf+} of Section~\ref{sec:refining}, the
rule \Rule{AbsInf++} we use int the implementation improved the output of the computed
type. Indeed, using rule~[{\sc AbsInf}+] we would have obtained the
type type
$(\Int\to\Int)\land(\Bool\to\Bool)\land(\Bool\vee\Int\to\Bool\vee\Int)$ $(\Int\to\Int)\land(\Bool\to\Bool)\land(\Bool\vee\Int\to\Bool\vee\Int)$
with a redundant arrow. Here we can see that, since we deduced with a redundant arrow. Here we can see that, since we deduced
...@@ -75,12 +82,14 @@ the singleton type \True{} (the type whose only value is ...@@ -75,12 +82,14 @@ the singleton type \True{} (the type whose only value is
any other value (recall that $\neg\True$ is equivalent to any other value (recall that $\neg\True$ is equivalent to
$\texttt{Any\textbackslash}\True$). It works on values of any type, $\texttt{Any\textbackslash}\True$). It works on values of any type,
but we could restrict it to Boolean values by simply annotating the but we could restrict it to Boolean values by simply annotating the
parameter by \Bool{} (which in CDuce is syntactic sugar for parameter by \Bool{} (which, in the CDuce types that our system uses, is syntactic sugar for
\True$\vee$\False) yielding the type \True$\vee$\False) yielding the type
$(\True{\to}\False)\wedge(\False{\to}\True)$. $(\True{\to}\False)\wedge(\False{\to}\True)$.
The \texttt{or\_} connective (Code~5) is straightforward as far as the The \texttt{or\_} connective (Code~5) is straightforward as far as the
code goes, but we see that the overloaded type precisely captures all code goes, but we see that the overloaded type precisely captures all
possible cases. Again we use a generalized version of the possible cases: the function returns \code{false} if and only if both
arguments are of type $\neg\True$, that is, they are any value
different from \code{true}. Again we use a generalized version of the
\texttt{or\_} connective that accepts and treats any value that is not \texttt{or\_} connective that accepts and treats any value that is not
\texttt{true} as \texttt{false} and again, we could easily restrict the \texttt{true} as \texttt{false} and again, we could easily restrict the
domain to \Bool{} if desired.\\ domain to \Bool{} if desired.\\
...@@ -109,7 +118,8 @@ function returns \texttt{3}. Our system correctly deduces a (complex) ...@@ -109,7 +118,8 @@ function returns \texttt{3}. Our system correctly deduces a (complex)
intersection type that covers all cases (plus several redundant arrow intersection type that covers all cases (plus several redundant arrow
types). That this type is as precise as possible can be shown by the fact that types). That this type is as precise as possible can be shown by the fact that
when applying when applying
\texttt{f} to arguments of the expected type, the \emph{type} deduced for the \texttt{f} to arguments of the expected type, the \emph{type}
statically deduced for the
whole expression is the singleton type \texttt{1}, or \texttt{2}, whole expression is the singleton type \texttt{1}, or \texttt{2},
or \texttt{3}, depending on the type of the arguments. or \texttt{3}, depending on the type of the arguments.
...@@ -154,9 +164,9 @@ $(\True\to\Any\to\True)\land(\Any\to\True\to\True)\land ...@@ -154,9 +164,9 @@ $(\True\to\Any\to\True)\land(\Any\to\True\to\True)\land
%}\\[.7mm] %}\\[.7mm]
then the rule \Rule{OverApp} applies and \True, \Any, and $\lnot\True$ become candidate types for then the rule \Rule{OverApp} applies and \True, \Any, and $\lnot\True$ become candidate types for
\texttt{x}, which allows us to deduce the precise type given in the table. Finally, thanks to rule \Rule{OverApp} it is not necessary to use a type case to force refinement. As a consequence, we can define the functions \texttt{and\_} and \texttt{xor\_} more naturally as: \texttt{x}, which allows us to deduce the precise type given in the table. Finally, thanks to rule \Rule{OverApp} it is not necessary to use a type case to force refinement. As a consequence, we can define the functions \texttt{and\_} and \texttt{xor\_} more naturally as:
\begin{alltt}\color{darkblue}\morecompact \begin{alltt}\color{darkblue}
let and_ = fun (x : Any) -> fun (y : Any) -> not_ (or_ (not_ x) (not_ y)) 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)) 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} \end{alltt}
for which the very same types as in Table~\ref{tab:implem} are deduced. for which the very same types as in Table~\ref{tab:implem} are deduced.
...@@ -167,7 +177,7 @@ explained, a single pass analysis would deduce ...@@ -167,7 +177,7 @@ explained, a single pass analysis would deduce
for {\tt x} for {\tt x}
a type \Int{} from the {\tt f\;x} application and \Any{} from the {\tt g\;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 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 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 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 type $(\Int{\to}\Int)\land(\Any{\to}\Bool)$ is to diverge when the
argument is of type \Int: since this intersection type states that argument is of type \Int: since this intersection type states that
...@@ -175,7 +185,7 @@ whenever the input is \Int, {\em both\/} branches can be selected, ...@@ -175,7 +185,7 @@ 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. 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. 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 Indeed our {\tt example10} function can be applied to an integer, but
at runtime the application of {\tt f ~x} will diverge. at runtime the application of {\tt f\,x} will diverge.
Code~11 simulates the behaviour of Javascript property resolution, by looking 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 for a property \texttt{l} either in the object \texttt{o} itself or in the
...@@ -208,7 +218,7 @@ previously defined). Note that for all examples for which there was no explicit ...@@ -208,7 +218,7 @@ 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. 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, 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 the function is ill-typed (which our typechecker detects accurately). The
original Example~14 could be written in our syntax with : original Example~14 could be written in our syntax as:
\begin{verbatim} \begin{verbatim}
let example14_alt = fun (input : Int | String) -> let example14_alt = fun (input : Int | String) ->
...@@ -221,13 +231,13 @@ original Example~14 could be written in our syntax with : ...@@ -221,13 +231,13 @@ original Example~14 could be written in our syntax with :
\end{verbatim} \end{verbatim}
Notice, in the version above the absence of an occurrence of \texttt{input} in 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 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 because \texttt{is\_int (fst extra)} is not \texttt{True} (i.e., if
\texttt{fst extra} is not an integer) or because \texttt{input} is not an \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 integer. Therefore, in our setting, the type information propagated to the
second test is : $\texttt{(input, is\_int (fst extra))} \in \lnot (\Int, 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)$, that is $\texttt{(input, is\_int (fst extra))} \in (\lnot\Int,
\True)\lor(\Int, \False)$ Therefore, the type of \texttt{input} in the second \True)\lor(\Int, \False)$. Therefore, the type deduced for \texttt{input} in the second
branch is of type $(\String\lor\Int) \land (\lnot\Int \lor \int) = branch is $(\String\lor\Int) \land (\lnot\Int \lor \Int) =
\String\lor\Int$ which is not precise enough. By adding an occurrence of \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 \texttt{input} in our \texttt{example14\_alt}, we can further restrict its type
typecheck the function. Lifting this limitation through a control-flow analysis typecheck the function. Lifting this limitation through a control-flow analysis
...@@ -235,7 +245,7 @@ Notice, in the version above the absence of an occurrence of \texttt{input} in ...@@ -235,7 +245,7 @@ Notice, in the version above the absence of an occurrence of \texttt{input} in
Although these experiments are still preliminary, they show how the Although these experiments are still preliminary, they show how the
combination occurrence typing and set-theoretic types, together combination of occurrence typing and set-theoretic types, together
with the type inference for overloaded function types presented in with the type inference for overloaded function types presented in
Section~\ref{sec:refining} goes beyond what languages like Section~\ref{sec:refining} goes beyond what languages like
TypeScript and Flow do, since they can only infer single arrow types. TypeScript and Flow do, since they can only infer single arrow types.
......
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