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

added example 12

parent 5d6c115a
\lstset{language=[Objective]Caml,columns=fixed,basicstyle=\linespread{0.43}\ttfamily\scriptsize,aboveskip=-0.5em,belowskip=-1em,xleftmargin=-0.5em}
\begin{table}
{\scriptsize
\begin{tabular}{|@{\,}c@{\,}|p{0.54\textwidth}@{}|@{\,}p{0.41\textwidth}@{\,}|}
\begin{tabular}{|@{\,}c@{\,}|p{0.53\textwidth}@{}|@{\,}p{0.42\textwidth}@{\,}|}
\hline
& Code & Inferred type\\
% \hline
......@@ -124,9 +124,8 @@ $(\Keyw{Document}\to\False)~\land$\newline
$(\orecord{ \texttt{nodeType}\,{=}\,1, \texttt{childNodes}\,{=}\,\Keyw{Nil} }\to\True) ~\land$\newline
$(\orecord{ \texttt{nodeType}\,{=}\,1,
\texttt{childNodes}\,{=}\,(\Keyw{Node},\Keyw{NodeList})
}$\newline
\hspace*{4.5cm}$\to\False) ~\land$\newline
$(\Keyw{Text}\to\Bool)~\land$\newline (omitted redundant arrows)
}\to\False) ~\land$\newline
$(\Keyw{Text}\to\Bool)~\land\ldots$ (omitted redundant arrows)
\\\hline
9 & \begin{lstlisting}
let xor_ = fun (x : Any) -> fun (y : Any) ->
......@@ -172,7 +171,35 @@ $((\Keyw{Nil}\,|\,\orecord{\texttt{l}\,=\,?\Keyw{Empty},\, \texttt{prototype}\,=
~\newline
$\Keyw{Object}\to\Keyw{Any}$
\\\hline
\end{tabular}
12 & \begin{lstlisting}
atom character
atom boolean
atom undefined
type String = Number | Character | Boolean | Undefined
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 undefined
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\bigskip\medskip\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
\end{tabular}
}
\caption{Types inferred by the implementation}
\ifsubmission%
......
......@@ -208,6 +208,21 @@ 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).
Finally, 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)$).
\input{code_table2}
In Table~\ref{tab:implem2}, we reproduce in our syntax the 14
......@@ -269,7 +284,7 @@ The original Example~14 of~\citet{THF10} can be written in our syntax as:
where \code{and2\_} is the uncurried version of the \code{and\_}
function we defined in \eqref{and+} and \code{is\_int} is the fuction
defined in the third row of Table~\ref{tab:implem}.
Our system rejects the expression above, while the system in~\cite{THF10}
Our system rejects the expression above, while the system by~\citet{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
......
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