Commit 6660e137 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Add Fixpoint example and fix some errors in table one.

parent d48a9533
......@@ -53,7 +53,7 @@ let or_ = fun (x : Any) -> fun (y: Any) ->
else if y is True then true else false
\end{lstlisting}
&\vfill
$(\True\to\textsf{Any}\to\True)\land(\textsf{Any}\to\True\to\True)\;\land$\newline
$(\True\to\textsf{Any}\to\True)\land(\lnot\Keyw{True}\to\True\to\True)\;\land$\newline
$(\lnot\True\to\lnot\True\to\False)$
\\\hline
6 &
......@@ -137,10 +137,9 @@ $(\lnot\True\to((\True\to\True) \land (\lnot\True\to\False))$
\\\hline
10 & \begin{lstlisting}
(* f, g have type: (Int->Int) & (Any->Bool) *)
let example10 = fun (x : Any) ->
if (f x, g x) is (Int, Bool) then 1 else 2
\end{lstlisting} &\vfill\medskip\smallskip
\end{lstlisting} &\vfill
$(\Int\to\textsf{Empty})\land(\neg\Int\to{}2)$\newline
\texttt{Warning: line 4, 39-40: unreachable expression}
\\\hline
......@@ -172,22 +171,17 @@ $((\Keyw{Nil}\,|\,\orecord{\texttt{l}\,=\,?\Keyw{Empty},\, \texttt{prototype}\,=
$\Keyw{Object}\to\Keyw{Any}$
\\\hline
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
(* 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 undefined
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\bigskip\medskip\smallskip
else 0\end{lstlisting} &\vfill\smallskip
$(\Int\to\textsf{Number}) \wedge$\newline
$(\Char\to\textsf{Character})\wedge$\newline
$(\Bool\to\textsf{Boolean})\wedge$\newline
......@@ -199,6 +193,17 @@ $(\Int \to \Int) \wedge (\Char \to \Int) \wedge
$(\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$
\\\hline
\end{tabular}
}
\caption{Types inferred by the implementation}
......
......@@ -212,7 +212,7 @@ 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).
Finally, Code~12 implements the typical type-switching pattern used in
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
......@@ -228,6 +228,13 @@ system. Since our prototype has no type for strings, then we
Table~\ref{tab:implem} is
equivalent to $(\textsf{Any}\to\Int)\wedge(\lnot(\Bool{\vee} \Int {\vee} \Char) \to 0)$).
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}
In Table~\ref{tab:implem2}, we reproduce in our syntax the 14
archetypal examples of
......
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