Commit 0af273e2 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

Merge branch 'master' of gitlab.math.univ-paris-diderot.fr:beppe/occurrence-typing

parents ccd746b4 3518a8fc
\lstset{language=[Objective]Caml,columns=fixed,basicstyle=\linespread{0.43}\ttfamily\scriptsize,aboveskip=-0.5em,belowskip=-1em,xleftmargin=-0.5em} \lstset{language=[Objective]Caml,columns=fixed,basicstyle=\linespread{0.43}\ttfamily\scriptsize,aboveskip=-0.5em,belowskip=-1em,xleftmargin=-0.5em}
\begin{table} \begin{table}
{\scriptsize {\scriptsize
\begin{tabular}{|@{\,}c@{\,}|p{0.54\textwidth}@{}|@{\,}p{0.41\textwidth}@{\,}|} \begin{tabular}{|@{\,}c@{\,}|p{0.53\textwidth}@{}|@{\,}p{0.42\textwidth}@{\,}|}
\hline \hline
& Code & Inferred type\\ & Code & Inferred type\\
% \hline % \hline
...@@ -124,9 +124,8 @@ $(\Keyw{Document}\to\False)~\land$\newline ...@@ -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{Nil} }\to\True) ~\land$\newline
$(\orecord{ \texttt{nodeType}\,{=}\,1, $(\orecord{ \texttt{nodeType}\,{=}\,1,
\texttt{childNodes}\,{=}\,(\Keyw{Node},\Keyw{NodeList}) \texttt{childNodes}\,{=}\,(\Keyw{Node},\Keyw{NodeList})
}$\newline }\to\False) ~\land$\newline
\hspace*{4.5cm}$\to\False) ~\land$\newline $(\Keyw{Text}\to\Bool)~\land\ldots$ (omitted redundant arrows)
$(\Keyw{Text}\to\Bool)~\land$\newline (omitted redundant arrows)
\\\hline \\\hline
9 & \begin{lstlisting} 9 & \begin{lstlisting}
let xor_ = fun (x : Any) -> fun (y : Any) -> let xor_ = fun (x : Any) -> fun (y : Any) ->
...@@ -172,7 +171,35 @@ $((\Keyw{Nil}\,|\,\orecord{\texttt{l}\,=\,?\Keyw{Empty},\, \texttt{prototype}\,= ...@@ -172,7 +171,35 @@ $((\Keyw{Nil}\,|\,\orecord{\texttt{l}\,=\,?\Keyw{Empty},\, \texttt{prototype}\,=
~\newline ~\newline
$\Keyw{Object}\to\Keyw{Any}$ $\Keyw{Object}\to\Keyw{Any}$
\\\hline \\\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} \caption{Types inferred by the implementation}
\ifsubmission% \ifsubmission%
......
...@@ -24,7 +24,7 @@ and, even more, the \code{and\_} and \code{xor\_} functions given ...@@ -24,7 +24,7 @@ and, even more, the \code{and\_} and \code{xor\_} functions given
in \eqref{and+} and \eqref{xor+} later in this 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} by giving the type inferred for the fourteen examples given in that
work. work.
It should be noted that for all the examples we present, the It should be noted that for all the examples we present, the
...@@ -208,6 +208,21 @@ whether \texttt{l} is present at some point in the list or not (recall that ...@@ -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} in a record type such as $\orecord{ l=?\Empty }$, indicate that field \texttt{l}
is absent for sure). 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} \input{code_table2}
In Table~\ref{tab:implem2}, we reproduce in our syntax the 14 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: ...@@ -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\_} where \code{and2\_} is the uncurried version of the \code{and\_}
function we defined in \eqref{and+} and \code{is\_int} is the fuction function we defined in \eqref{and+} and \code{is\_int} is the fuction
defined in the third row of Table~\ref{tab:implem}. 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 correctly infers the the function always return an integer. The reason
why our system rejects it is because the type it deduces for the why our system rejects it is because the type it deduces for the
occurrence of \code{input} in the 6th line of the code 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