Commit 129254cb authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

few typos

parent 8eade7d0
...@@ -48,9 +48,9 @@ Booleans. Here the ...@@ -48,9 +48,9 @@ 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{} $\code{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 \code{x}, yielding the precise type
$(\Int\to\Int)\land(\Bool\to\Bool)$. Note that w.r.t.\ $(\Int\to\Int)\land(\Bool\to\Bool)$. Note that w.r.t.\
rule \Rule{AbsInf+} of Section~\ref{sec:refining}, the rule \Rule{AbsInf+} of Section~\ref{sec:refining}, the
rule \Rule{AbsInf++} we use in the implementation improves the output of the computed rule \Rule{AbsInf++} we use in the implementation improves the output of the computed
...@@ -62,9 +62,9 @@ the first two arrows $(\Int\to\Int)\land(\Bool\to\Bool)$, and since ...@@ -62,9 +62,9 @@ the first two arrows $(\Int\to\Int)\land(\Bool\to\Bool)$, and since
the union of their domain exactly covers the domain of the third arrow, then the union of their domain exactly covers the domain of the third arrow, then
the latter is not needed. Code~2 shows what happens when the argument the latter is not needed. Code~2 shows what happens when the argument
of the function is left unannotated (i.e., it is annotated by the top of the function is left unannotated (i.e., it is annotated by the top
type \Any, written ``\texttt{Any}'' in our implementation). Here type \Any, written ``\code{Any}'' in our implementation). Here
type-checking and refinement also work as expected, but the function type-checking and refinement also work as expected, but the function
only type checks if all cases for \texttt{x} are covered (which means only type checks if all cases for \code{x} are covered (which means
that the function must handle the case of inputs that are neither in \Int{} that the function must handle the case of inputs that are neither in \Int{}
nor in \Bool). nor in \Bool).
...@@ -72,37 +72,37 @@ The following examples paint a more interesting picture. First ...@@ -72,37 +72,37 @@ The following examples paint a more interesting picture. First
(Code~3) it is (Code~3) it is
easy in our formalism to program type predicates such as those easy in our formalism to program type predicates such as those
hard-coded in the $\lambda_{\textit{TR}}$ language of \citet{THF10}. Such type hard-coded in the $\lambda_{\textit{TR}}$ language of \citet{THF10}. Such type
predicates, which return \texttt{true} if and only if their input has predicates, which return \code{true} if and only if their input has
a particular type, are just plain functions with an intersection a particular type, are just plain functions with an intersection
type inferred by the system of Section~\ref{sec:refining}. We next define Boolean connectives as overloaded type inferred by the system of Section~\ref{sec:refining}. We next define Boolean connectives as overloaded
functions. The \texttt{not\_} connective (Code~4) just tests whether its functions. The \code{not\_} connective (Code~4) just tests whether its
argument is the Boolean \texttt{true} by testing that it belongs to argument is the Boolean \code{true} by testing that it belongs to
the singleton type \True{} (the type whose only value is the singleton type \True{} (the type whose only value is
\texttt{true}) returning \texttt{false} for it and \texttt{true} for \code{true}) returning \code{false} for it and \code{true} for
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 the CDuce types that our system uses, is syntactic sugar for parameter by \Bool{} (which, in the CDuce's 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 \code{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: the function returns \code{false} if and only if both possible cases: the function returns \code{false} if and only if both
arguments are of type $\neg\True$, that is, they are any value arguments are of type $\neg\True$, that is, they are any value
different from \code{true}. Again we use a generalized version of the different from \code{true}. Again we use a generalized version of the
\texttt{or\_} connective that accepts and treats any value that is not \code{or\_} connective that accepts and treats any value that is not
\texttt{true} as \texttt{false} and again, we could easily restrict the \code{true} as \code{false} and again, we could easily restrict the
domain to \Bool{} if desired.\\ domain to \Bool{} if desired.\\
\indent \indent
To showcase the power of our type system, and in particular of To showcase the power of our type system, and in particular of
the ``$\worra{}{}$'' the ``$\worra{}{}$''
type operator, we define \texttt{and\_} (Code~6) using De Morgan's type operator, we define \code{and\_} (Code~6) using De Morgan's
Laws instead of Laws instead of
using a direct definition. Here the application of the outermost \texttt{not\_} operator is checked against type \True. This using a direct definition. Here the application of the outermost \code{not\_} operator is checked against type \True. This
allows the system to deduce that the whole \texttt{or\_} application allows the system to deduce that the whole \code{or\_} application
has type \False, which in turn leads to \texttt{not\_\;x} and has type \False, which in turn leads to \code{not\_\;x} and
\texttt{not\_\;y} to have type $\lnot \True$ and therefore both \texttt{x} \code{not\_\;y} to have type $\lnot \True$ and therefore both \code{x}
and \texttt{y} to have type \True. The whole function is typed with and \code{y} to have type \True. The whole function is typed with
the most precise type (we present the type as printed by our the most precise type (we present the type as printed by our
implementation, but the first arrow of the resulting type is implementation, but the first arrow of the resulting type is
equivalent to equivalent to
...@@ -110,60 +110,60 @@ $(\True\to\lnot\True\to\False)\land(\True\to\True\to\True)$). ...@@ -110,60 +110,60 @@ $(\True\to\lnot\True\to\False)\land(\True\to\True\to\True)$).
All these type predicates and Boolean connectives can be used together All these type predicates and Boolean connectives can be used together
to write complex type tests, as in Code~7. Here we define a function to write complex type tests, as in Code~7. Here we define a function
\texttt{f} that takes two arguments \texttt{x} and \texttt{y}. If \code{f} that takes two arguments \code{x} and \code{y}. If
\texttt{x} is an integer and \texttt{y} a Boolean, then it returns the \code{x} is an integer and \code{y} a Boolean, then it returns the
integer \texttt{1}; if \texttt{x} is a character or integer \code{1}; if \code{x} is a character or
\texttt{y} is an integer, then it returns \texttt{2}; otherwise the \code{y} is an integer, then it returns \code{2}; otherwise the
function returns \texttt{3}. Our system correctly deduces a (complex) function returns \code{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} \code{f} to arguments of the expected type, the \emph{type
statically deduced for the statically deduced} for the
whole expression is the singleton type \texttt{1}, or \texttt{2}, whole expression is the singleton type \code{1}, or \code{2},
or \texttt{3}, depending on the type of the arguments. or \code{3}, depending on the type of the arguments.
Code~8 allows us to demonstrate the use and typing of record paths. We 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 model, using open records, the type of DOM objects that represent XML
or HTML documents. Such objects possess a common field or HTML documents. Such objects possess a common field
\texttt{nodeType} containing an integer constant denoting the kind of \code{nodeType} containing an integer constant denoting the kind of
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 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 different fields and methods. It is common practice to perform a test
on the value of the \texttt{nodeType} field. In dynamic languages such on the value of the \code{nodeType} field. In dynamic languages such
as JavaScript, the relevant field can directly be accessed as JavaScript, the relevant field can directly be accessed
after having checked for the appropriate \texttt{nodeType}, whereas after having checked for the appropriate \code{nodeType}, whereas
in statically typed languages such as Java, a downward cast in statically typed languages such as Java, a downward cast
from the generic \texttt{Node} type to the expected precise type of from the generic \code{Node} type to the expected precise type of
the object is needed. We can see that using the extension presented in the object is needed. We can see that using the record expressions presented in
Section~\ref{ssec:struct} we can deduce the correct type for Section~\ref{ssec:struct} we can deduce the correct type for
\texttt{x} in all cases. Of particular interest is the last case, \code{x} in all cases. Of particular interest is the last case,
since we use a type case to check the emptiness of the list of child since we use a type case to check the emptiness of the list of child
nodes. This splits, at the type level, the case for the \Keyw{Element} nodes. This splits, at the type level, the case for the \Keyw{Element}
type depending on whether the content of the \texttt{childNodes} field type depending on whether the content of the \code{childNodes} field
is the empty list or not. is the empty list or not.
Code~9 shows the usefulness of the rule \Rule{OverApp}. Code~9 shows the usefulness of the rule \Rule{OverApp}.
Consider the definition of the \texttt{xor\_} operator. Consider the definition of the \code{xor\_} operator.
Here the rule~[{\sc AbsInf}+] is not sufficient to precisely type the Here the rule~[{\sc AbsInf}+] is not sufficient to precisely type the
function, and using only this rule would yield a type function, and using only this rule would yield a type
$\Any\to\Any\to\Bool$. $\Any\to\Any\to\Bool$.
\iflongversion \iflongversion
Let us follow the behavior of the Let us follow the behavior of the
``$\worra{}{}$'' operator. Here the whole \texttt{and\_} is requested ``$\worra{}{}$'' operator. Here the whole \code{and\_} is requested
to have type \True, which implies that \texttt{or\_ x y} must have to have type \True, which implies that \code{or\_ x y} must have
type \True. This can always happen, whether \texttt{x} is \True{} or type \True. This can always happen, whether \code{x} is \True{} or
not (but then depends on the type of \texttt{y}). The ``$\worra{}{}$'' not (but then depends on the type of \code{y}). The ``$\worra{}{}$''
operator correctly computes that the type for \texttt{x} in the operator correctly computes that the type for \code{x} in the
``\texttt{then}'' branch is $\True\vee\lnot\True\lor\True\simeq\Any$, ``\emph{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 \code{y}.
\fi%%%%%%%%%%%%%% \fi%%%%%%%%%%%%%%
However, since \texttt{or\_} has type However, since \code{or\_} has type
%\\[.7mm]\centerline{% %\\[.7mm]\centerline{%
$(\True\to\Any\to\True)\land(\Any\to\True\to\True)\land $(\True\to\Any\to\True)\land(\Any\to\True\to\True)\land
(\lnot\True\to\lnot\True\to\False)$ (\lnot\True\to\lnot\True\to\False)$
%}\\[.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: \code{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 \code{and\_} and \code{xor\_} more naturally as:
\begin{alltt}\color{darkblue} \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 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+} 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+}
...@@ -189,40 +189,41 @@ at runtime the application of {\tt f\,x} will diverge. ...@@ -189,40 +189,41 @@ at runtime the application of {\tt f\,x} will diverge.
Code~11 implements the typical type-switching pattern used in JavaScript. While Code~11 implements the typical type-switching pattern used in JavaScript. While
languages such as Scheme and Racket provides specific type predicates for each languages such as Scheme and Racket hard-code specific type predicates for each
type---predicates that in our system must not be provided since they can be type---predicates that our system does not need to hard-code since they can be
directly defined (cf. Code~3)---, JavaScript includes a \code{typeof} function directly defined (cf. Code~3)---, JavaScript hard-codes a \code{typeof} function
that takes an expression and returns a string indicating the type of the that takes an expression and returns a string indicating the type of the
expression. Code~11 shows that \code{typeof} can be encoded and precisely typed expression. Code~11 shows that \code{typeof} can be encoded and precisely typed
in our system. Indeed, constant strings are simply encoded as fixed list of in our system. Indeed, constant strings are simply encoded as fixed list of
characters (themselves encoded as pairs as usual, with special atom \textsf{nil} characters (themselves encoded as pairs as usual, with special atom \code{nil}
representing the empty list). Thanks to our precise tracking of singleton types representing the empty list). Thanks to our precise tracking of singleton types
both in the result type of \texttt{typeof} and in the type case of both in the result type of \code{typeof} and in the type case of
\texttt{test}, we can deduce for the latter a precise type (the given in \code{test}, we can deduce for the latter a precise type (the given in
Table~\ref{tab:implem} is equivalent to Table~\ref{tab:implem} is equivalent to
$(\textsf{Any}\to\Int)\wedge(\lnot(\Bool{\vee} \Int {\vee} \Char) \to 0)$). $(\textsf{Any}\to\Int)\wedge(\lnot(\Bool{\vee} \Int {\vee} \Char) \to 0)$).
Code~12 simulates the behavior of JavaScript property resolution, by looking Code~12 simulates the behavior of JavaScript property resolution, by looking
for a property \texttt{l} either in the object \texttt{o} itself or in the for a property \code{l} either in the object \code{o} itself or in the
chained list of its \texttt{prototype} objects. In that example, we first model chained list of its \code{prototype} objects. In this example, we first model
prototype-chaining by defining a type \texttt{Object} that can be either the prototype-chaining by defining a type \code{Object} that can be either the
atom \texttt{Null} or any record with a \texttt{prototype} field which contains atom \code{Null} or any record with a \code{prototype} field which contains
(recursively) an \texttt{Object}. To ease the reading, we defined a recursive (recursively) an \code{Object}. To ease the reading, we defined a recursive
type \texttt{ObjectWithPropertyL} which is either a record with a field type \code{ObjectWithPropertyL} which is either a record with a field
\texttt{l} or a record with a prototype of type \texttt{ObjectWithPropertyL}. We \code{l} or a record with a prototype of type \code{ObjectWithPropertyL}. We
can then define two predicate functions \texttt{has\_property\_l} and can then define two predicate functions \code{has\_property\_l} and
\texttt{has\_own\_property\_l} that test whether an object has a property \code{has\_own\_property\_l} that test whether an object has a property
through its prototype or directly. Lastly, we can define a function 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 \code{get\_property\_l} which directly accesses the field if it is present, or
recursively search for it through the prototype chain, where in our syntax, the recursively search for it through the prototype chain; the recursive
explicitly-typed parameter \texttt{self} allows one to refer to the function itself. Of search is implemented by calling the explicitly-typed
parameter \code{self} which, in our syntax, refers to the function itself. Of
particular interest is the type deduced for the two predicate functions. Indeed, 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 we can see that \code{has\_own\_property\_l} is given an overloaded type whose
first argument is in each case a recursive record type that describe precisely first argument is in each case a recursive record type that describes precisely
whether \texttt{l} is present at some point in the list or not (recall that whether \code{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} in a record type a field such as $\orecord{ \ell=?\textsf{Empty} }$, indicate that field \code{$\ell$}
is absent for sure). is surely absent).
Notice that in our language, a fixpoint combinator can be defined as follows Notice that in our language a fixpoint combinator can be defined as follows
\begin{alltt}\color{darkblue} \begin{alltt}\color{darkblue}
type X = X -> \textit{S} -> \textit{T} type X = X -> \textit{S} -> \textit{T}
let z = fun (((\textit{S} -> \textit{T}) -> \textit{S} -> \textit{T} ) -> (\textit{S} -> \textit{T})) f -> let z = fun (((\textit{S} -> \textit{T}) -> \textit{S} -> \textit{T} ) -> (\textit{S} -> \textit{T})) f ->
...@@ -254,8 +255,8 @@ archetypal examples of ...@@ -254,8 +255,8 @@ archetypal examples of
\citet{THF10} (we tried to complete such examples with neutral code when they \citet{THF10} (we tried to complete such examples with neutral code when they
were incomplete in the original paper). Of these 14 examples, were incomplete in the original paper). Of these 14 examples,
Example~1 to 13 depict combinations of type predicates (such Example~1 to 13 depict combinations of type predicates (such
as \texttt{is\_int}) used either directly or through Boolean as \code{is\_int}) used either directly or through Boolean
predicates (such as the \texttt{or\_} function previously predicates (such as the \code{or\_} function previously
defined). Note that for all examples for which there was no explicit defined). Note that for all examples for which there was no explicit
indication in the original version, we \emph{infer} the type of the indication in the original version, we \emph{infer} the type of the
function whereas in~\cite{THF10} the same examples are always in a function whereas in~\cite{THF10} the same examples are always in a
...@@ -280,22 +281,24 @@ of the example is to show that indeed, the function is ill-typed ...@@ -280,22 +281,24 @@ of the example is to show that indeed, the function is ill-typed
%% add (strlen input) (fst extra) %% add (strlen input) (fst extra)
%% else 0 %% else 0
%% \end{alltt} %% \end{alltt}
%% 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 \code{input} in
%% the second \texttt{if} statement. Indeed, if the first test fails, it is either %% the second \code{if} statement. Indeed, if the first test fails, it is either
%% because \texttt{is\_int (fst extra)} is not \texttt{True} (i.e., if %% because \code{is\_int (fst extra)} is not \code{True} (i.e., if
%% \texttt{fst extra} is not an integer) or because \texttt{input} is not an %% \code{fst extra} is not an integer) or because \code{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 : $\code{(input, is\_int (fst extra))} \in \lnot (\Int,
%% \True)$, that is $\texttt{(input, is\_int (fst extra))} \in (\lnot\Int, %% \True)$, that is $\code{(input, is\_int (fst extra))} \in (\lnot\Int,
%% \True)\lor(\Int, \False)$. Therefore, the type deduced for \texttt{input} in the second %% \True)\lor(\Int, \False)$. Therefore, the type deduced for \code{input} in the second
%% branch is $(\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 %% \code{input} in our \code{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
%% is part of our future work. %% is part of our future work.
%% } %% }
The original Example~14 of~\citet{THF10} can be written in our syntax as: The original Example~14 of~\citet{THF10} is the only case of their
work that our
system cannot directly capture. It can be written in our syntax as:
\begin{alltt}\color{darkblue} \begin{alltt}\color{darkblue}
let example14 = fun (input : Int|String) -> let example14 = fun (input : Int|String) ->
fun (extra : (Any, Any)) -> fun (extra : (Any, Any)) ->
......
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