then the rule \Rule{OverApp} applies and \True, \Any, and $\lnot\True$ become candidate types for

then the rule \Rule{OverApp} applies and \True, \Any, and $\lnot\True$ become candidate types for

\texttt{x}, which allows us to deduce the precise type given in the table. Finally, thanks to rule \Rule{OverApp} it is not necessary to use a type case to force refinement. As a consequence, we can define the functions \texttt{and\_} and \texttt{xor\_} more naturally as:

\code{x}, which allows us to deduce the precise type given in the table. Finally, thanks to rule \Rule{OverApp} it is not necessary to use a type case to force refinement. As a consequence, we can define the functions \code{and\_} and \code{xor\_} more naturally as:

\begin{alltt}\color{darkblue}

\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 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+}

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+}

...

@@ -189,40 +189,41 @@ at runtime the application of {\tt f\,x} will diverge.

...

@@ -189,40 +189,41 @@ at runtime the application of {\tt f\,x} will diverge.

Code~11 implements the typical type-switching pattern used in JavaScript. While

Code~11 implements the typical type-switching pattern used in JavaScript. While

languages such as Scheme and Racket provides specific type predicates for each

languages such as Scheme and Racket hard-code specific type predicates for each

type---predicates that in our system must not be provided since they can be

type---predicates that our system does not need to hard-code since they can be

directly defined (cf. Code~3)---, JavaScript includes a \code{typeof} function

directly defined (cf. Code~3)---, JavaScript hard-codes a \code{typeof} function

that takes an expression and returns a string indicating the type of the

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

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

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}

characters (themselves encoded as pairs as usual, with special atom \code{nil}

representing the empty list). Thanks to our precise tracking of singleton types

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

both in the result type of \code{typeof} and in the type case of

\texttt{test}, we can deduce for the latter a precise type (the given in

\code{test}, we can deduce for the latter a precise type (the given in