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

Rework example, move fixpoint explanation to the main part and use singleton string for typeof.

parent 51117419
......@@ -143,7 +143,29 @@ let example10 = fun (x : Any) ->
$(\Int\to\textsf{Empty})\land(\neg\Int\to{}2)$\newline
\texttt{Warning: line 4, 39-40: unreachable expression}
\\\hline
11 & \begin{lstlisting}
11 & \begin{lstlisting}
let typeof = fun (x:Any) ->
if x is Int then "number"
else if x is Char then "string"
else if x is Bool then "boolean" else "object"
let test = fun (x:Any) ->
if typeof x is "number" then incr x
else if typeof x is "string" then charcode x
else if typeof x is "boolean" then int_of_bool x
else 0\end{lstlisting} &\vfill\smallskip
$(\Int\to\textsf{"number"}) \wedge$\newline
$(\Char\to\textsf{"string"})\wedge$\newline
$(\Bool\to\textsf{"boolean"})\wedge$\newline
$(\lnot(\Bool{\vee}\Int{\vee}\Char)\to\textsf{"object"})\wedge \ldots$\newline
(two other redundant cases omitted)
\newline~\newline
$(\Int \to \Int) \wedge (\Char \to \Int) \wedge
(\Bool \to \Int) \wedge $\newline
$(\lnot(\Bool{\vee} \Int {\vee} \Char) \to 0)\wedge \ldots$\newline
(two other redundant cases omitted)
\\\hline
12 & \begin{lstlisting}
atom null
type Object = Null | { prototype = Object ..}
type ObjectWithPropertyL = { l = Any ..}
......@@ -170,39 +192,6 @@ $((\Keyw{Nil}\,|\,\orecord{\texttt{l}\,=\,?\Keyw{Empty},\, \texttt{prototype}\,=
~\newline
$\Keyw{Object}\to\Keyw{Any}$
\\\hline
12 & \begin{lstlisting}
(* number, character,... are atoms that represent
the strings "number", "string",... from JS. *)
let typeof = fun (x:Any) -> if x is Int then number
else if x is Char then character
else if x is Bool then boolean else object
let test = fun (x:Any) ->
if typeof x is Number then incr x
else if typeof x is Character then charcode x
else if typeof x is Boolean then int_of_bool x
else 0\end{lstlisting} &\vfill\smallskip
$(\Int\to\textsf{Number}) \wedge$\newline
$(\Char\to\textsf{Character})\wedge$\newline
$(\Bool\to\textsf{Boolean})\wedge$\newline
$(\lnot(\Bool{\vee}\Int{\vee}\Char)\to\textsf{Undefined})\wedge \ldots$\newline
(two other redundant cases omitted)
\newline~\newline
$(\Int \to \Int) \wedge (\Char \to \Int) \wedge
(\Bool \to \Int) \wedge $\newline
$(\lnot(\Bool{\vee} \Int {\vee} \Char) \to 0)\wedge \ldots$\newline
(two other redundant cases omitted)
\\\hline
13 & \begin{lstlisting}
type X = X -> Empty -> Any
let z = fun (((Empty -> Any) -> Empty -> Any ) ->
(Empty -> Any)) f ->
let delta = fun ( X -> (Empty -> Any) ) x ->
f ( fun (Empty -> Any) v -> ( x x v ))
in delta delta
\end{lstlisting} &\vfill
$((\Empty\to\Any)\to\Empty\to\Any)\to\Empty\to\Any$
\\\hline
\end{tabular}
}
......
......@@ -259,11 +259,11 @@ The authors thank Paul-André Melliès for his help on type ranking.
\label{sec:proofs-algo}
\input{proofs-algo}
\newpage
%%\newpage
\section{Fix-point combinator}
\label{sec:fixpoint}
\input{fixpoint}
%% \section{Fix-point combinator}
%% \label{sec:fixpoint}
%% \input{fixpoint}
\iflongversion%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......
......@@ -187,7 +187,22 @@ 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 behavior of JavaScript property resolution, by looking
Code~11 implements the typical type-switching pattern used in JavaScript. While
languages such as Scheme and Racket provides specific type predicates for each
type---predicates that in our system must not be provided since they can be
directly defined (cf. Code~3)---, JavaScript includes a \code{typeof} function
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
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}
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
\texttt{test}, we can deduce for the latter a precise type (the given in
Table~\ref{tab:implem} is equivalent to
$(\textsf{Any}\to\Int)\wedge(\lnot(\Bool{\vee} \Int {\vee} \Char) \to 0)$).
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
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
......@@ -206,33 +221,31 @@ 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). As an aside notice that even if our language does
not explicitly include recursive expression, it is quite easy to
define a well-typed fix-point combinator (for the reader convinience
we show its definition both in \Appendix\ref{sec:fixpoint} and in our
on-line prototype).
Code~12 implements the typical type-switching pattern used in
JavaScript. While languages such as Scheme and Racket provides specific
type predicates for each type---predicates that in our system must not
be provided since they can be
directly defined (cf. Code~3)---, JavaScript includes a \code{typeof}
function that takes an expression and
returns a string indicating the type of the expression. Code~12 shows
that also \code{typeof} can be encoded and precisely typed in our
system. Since our prototype has no type for strings, then we
defined the return type of our encoding of \code{typeof} as
a union of some fixed atoms (for concision) but it would work the same way with real strings. In
JavaScript \code{typeof} is then used as in the \code{test} function and our
systems precisely types its usage (the type of \code{test} in
Table~\ref{tab:implem} is
equivalent to $(\textsf{Any}\to\Int)\wedge(\lnot(\Bool{\vee} \Int {\vee} \Char) \to 0)$).
is absent for sure).
Notice that in our language, a fixpoint combinator can be defined as follows
\begin{alltt}\color{darkblue}
type X = X -> \textit{S} -> \textit{T}
let z = fun (((\textit{S} -> \textit{T}) -> \textit{S} -> \textit{T} ) -> (\textit{S} -> \textit{T})) f ->
let delta = fun ( X -> (\textit{S} -> \textit{T}) ) x ->
f ( fun (\textit{S} -> \textit{T}) v -> ( x x v ))
in delta delta
\end{alltt}
which applied to any function \code{f:(\textit{S}$\to$\textit{T})$\to$\textit{S}$\to$\textit{T}}
returns a function \code{(z\,f):\textit{S}$\to$\textit{T}} such that
for every non
diverging expression \code{$e$} of type \code{\textit{S}}, the
expression \code{(z\,f)$e$} (which is of type \code{\textit{T}}) reduces to \code{f((z\,f)$e$)}.
It is then clear that definition of \code{get\_property\_l} in Code 12, is nothing but syntactic sugar for
\begin{alltt}\color{darkblue}
let get_property_l =
let aux = fun (self:Object->Any) -> fun (o:Object)->
if has_own_property_l o is True then o.l
else if o is Null then null
else self (o.prototype)
in z aux
\end{alltt}
where \code{\textit{S}} is \code{Object} and \code{\textit{T}} is \code{Any}.
Finally, Code~13 shows that, thanks to recursive function types, one can easily
define and typecheck a fixpoint combinator. We demonstrate it by first defining a
recursive function type $X=(X\to \Empty\to\Any)$ and then using it to annotate
the functions occuring in the definition of $Z$ (the eta-expanded version of
Curry's $Y$ combinator).
\input{code_table2}
......
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