Commit 90bd343a authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

typos

parent 92917429
......@@ -99,22 +99,22 @@ $(\lnot (\String\lor\Int)\to 0)$
let example10 = fun (p : (Any,Any)) ->
if is_int (fst p) is True then add1 (fst p) else 7
\end{lstlisting} & \vfill
$((\Int,\Any) \to \Int) \land ((\lnot (\Int,\Any) \to 7)$
$((\Int,\textsf{Any}) \to \Int) \land ((\lnot (\Int,\textsf{Any}) \to 7)$
\\\hline
11 & \begin{lstlisting}
let example11 = fun (p : (Any, Any)) ->
if and_ (is_int (fst p)) (is_int (snd p)) is True
then g p else no
\end{lstlisting} & \vfill\medskip\smallskip
\end{lstlisting} & \vfill\smallskip
$((\Int, \Int) \to \Int) \land
(((\Any, \lnot \Int)\lor(\lnot Int, \Any))\to\Keyw{no})$
(((\textsf{Any}, \lnot \Int)\lor(\lnot\Int, \textsf{Any}))\to\Keyw{no})$
\\\hline
12 & \begin{lstlisting}
let example12 =
fun (p : (Any, Any)) ->
if is_int (fst p) is True then true else false
\end{lstlisting} & \vfill
$((\Int,\Any) -> \True) \land ((\lnot \Int,\Any) -> \False) )$
$((\Int,\textsf{Any}) -> \True) \land ((\lnot \Int,\textsf{Any}) -> \False) )$
\\\hline
13 & \begin{lstlisting}
let example13 = fun (x : Any) -> fun (y : Any) ->
......@@ -123,21 +123,21 @@ let example13 = fun (x : Any) -> fun (y : Any) ->
else 3
\end{lstlisting} & \vfill
$(\Int \to \String \to 1) \land (\Int \to \lnot\String \to 2)) \land$\newline
$(\lnot \Int \to Any \to 3)$
$(\lnot \Int \to \textsf{Any} \to 3)$
\\\hline
14 & \begin{lstlisting}
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 (input, is_int (fst extra)) is (Any,True)
then add (strlen input) (fst extra)
else if (input, is_int (fst extra)) is (Any,True) then
add (strlen input) (fst extra)
else 0 \end{lstlisting}
& \vfill
$(\Int \to (\Int,\Any) \to \Int) ~\land~
(\Int \to (\lnot \Int, \Any) \to 0) ~\land~$\newline
$(\String \to (\Int,\Any) \to \Int) ~\land~
(\String \to (\lnot \Int, \Any) \to 0)$
$(\Int \to (\Int,\textsf{Any}) \to \Int) ~\land~
(\Int \to (\lnot \Int, \textsf{Any}) \to 0) ~\land~$\newline
$(\String \to (\Int,\textsf{Any}) \to \Int) ~\land~
(\String \to (\lnot \Int, \textsf{Any}) \to 0)$
\\\hline
\end{tabular}
}
......
......@@ -221,15 +221,71 @@ 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{verbatim}
\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
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 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}
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{alltt}
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} (i.e., if
......
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