with a redundant arrow. Here we can see that since we deduced

with a redundant arrow. Here we can see that since we deduced

the first two arrows $(\Int\to\Int)\land(\Bool\to\Bool)$, and since

the first two arrows $(\Int\to\Int)\land(\Bool\to\Bool)$, and since

the union of their domain exactly covers the domain the third arrow,

the union of their domain exactly covers the domain of the third arrow,

the latter is not needed. Code~2 shows what happens when the argument

the latter is not needed. Code~2 shows what happens when the argument

of the function is left unannotated (i.e., it is annotated by the top

of the function is left unannotated (i.e., it is annotated by the top

type \Any, written \texttt{Any} in our implementation). Here

type \Any, written \texttt{Any} in our implementation). Here

type-checking and refinement also work as expected, but the function

type-checking and refinement also work as expected, but the function

only type checks if all cases for \texttt{x} are covered (which means

only type checks if all cases for \texttt{x} are covered (which means

that the function must handle the case of inputs that are neither in \Int{}

that the function must handle the case of inputs that are neither in \Int{}

...

@@ -58,17 +58,20 @@ a particular type, are just plain functions with an intersection

...

@@ -58,17 +58,20 @@ a particular type, are just plain functions with an intersection

type inferred by the system of Section~\ref{sec:refining}. We next define Boolean connectives as overloaded

type inferred by the system of Section~\ref{sec:refining}. We next define Boolean connectives as overloaded

functions. The \texttt{not\_} connective (Code~4) just tests whether its

functions. The \texttt{not\_} connective (Code~4) just tests whether its

argument is the Boolean \texttt{true} by testing that it belongs to

argument is the Boolean \texttt{true} by testing that it belongs to

the singleton type \True{} (the type whose only value is \texttt{true}) returning \texttt{false} for it and \texttt{true} for any other value (recall that $\neg\True$ is equivalent to $\texttt{Any\textbackslash}\True$). It works on values of any type, but we could restrict it to Boolean values by simply annotating the parameter by \Bool{} (which in CDuce is syntactic sugar for \True$\vee$\False) yielding the type $(\True{\to}\False)\wedge(\False{\to}\True)$.

the singleton type \True{} (the type whose only value is

The \texttt{or\_} connective (Code~5) is defined as a

\texttt{true}) returning \texttt{false} for it and \texttt{true} for

curried function, that first type cases on its argument. Depending

any other value (recall that $\neg\True$ is equivalent to

on this first type it may return either a constant function that returns

$\texttt{Any\textbackslash}\True$). It works on values of any type,

\texttt{true} for every input, or, a function that

but we could restrict it to Boolean values by simply annotating the

discriminates on its argument (which is the second argument of the

parameter by \Bool{} (which in CDuce is syntactic sugar for

\texttt{or\_}) and returns \texttt{true} or \texttt{false}

\True$\vee$\False) yielding the type

accordingly. Again we use a generalized version of the

$(\True{\to}\False)\wedge(\False{\to}\True)$.

The \texttt{or\_} connective (Code~5) is straightforward as far as the

code goes, but we see that the overloaded type precisely capture all

the possible cases. Again we use a generalized version of the

\texttt{or\_} connective that accepts and treats any value that is not

\texttt{or\_} connective that accepts and treats any value that is not

\texttt{true} as \texttt{false} and again, we could restrict the

\texttt{true} as \texttt{false} and again, we could easily restrict the

domain to \Bool{} if we want.

domain to \Bool{} if desired.

To showcase the power of our type system, and in particular of

To showcase the power of our type system, and in particular of

the ``$\worra{}{}$''

the ``$\worra{}{}$''

...

@@ -117,8 +120,8 @@ nodes. This splits, at the type level, the case for the \Keyw{Element}

...

@@ -117,8 +120,8 @@ nodes. This splits, at the type level, the case for the \Keyw{Element}

type depending on whether the content of the \texttt{childNodes} field

type depending on whether the content of the \texttt{childNodes} field

is the empty list or not.

is the empty list or not.

Our implementation features one last improvement that allows us

Our implementation features one last enhancement that allows us

further improve the precision of the inferred type.

to further improve the precision of the inferred type.

Consider the definition of the \texttt{xor\_} operator (Code~9).

Consider the definition of the \texttt{xor\_} operator (Code~9).

Here the rule~[{\sc AbsInf}+] is not sufficient to precisely type the

Here the rule~[{\sc AbsInf}+] is not sufficient to precisely type the

function, and using only this rule would yield a type

function, and using only this rule would yield a type

...

@@ -156,7 +159,7 @@ since, \texttt{or\_} has type\\

...

@@ -156,7 +159,7 @@ since, \texttt{or\_} has type\\

We consider \True, \Any and $\lnot\True$ as candidate types for

We consider \True, \Any and $\lnot\True$ as candidate types for

\texttt{x} which, in turn allows us to deduce a precise type given in the table. Finally, thanks to this rule it is no longer necessary to force refinement by using a type case. As a consequence we can define the functions \texttt{and\_} and \texttt{or\_} more naturally as:

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

\begin{alltt}\color{darkblue}\morecompact

\begin{alltt}\color{darkblue}\morecompact

let and_ = fun (x : Any) -> fun (y : Any) -> not_ (or_ (not_ x) (not_ y))

let and_ = fun (x : Any) -> fun (y : Any) -> not_ (or_ (not_ x) (not_ y))

let xor_ = fun (x : Any) -> fun (y : Any) -> and_ (or_ x y) (not_ (and_ x y))

let xor_ = fun (x : Any) -> fun (y : Any) -> and_ (or_ x y) (not_ (and_ x y))

Occurrence typing is for variables in TypeScript, also paths in Flow. STRESS THE USE OF INTERSECTIONS AND UNIONS. ACTUALLY SPEAK OF UNION AND NEGATION (UNION FOR ALTERNATIVES, NEGATION FOR TYPING THE ELSE BRANCH AND THEREFORE WE GET INTERSECTION FOR FREE)

\kim{

\citet{THF10} extend to selectors, logical connectives, paths, and user

I don't really know about these:\\

Occurrence typing is for variables in TypeScript, also paths in Flow. STRESS THE USE OF INTERSECTIONS AND UNIONS. ACTUALLY SPEAK OF UNION AND NEGATION (UNION FOR ALTERNATIVES, NEGATION FOR TYPING THE ELSE BRANCH AND THEREFORE WE GET INTERSECTION FOR FREE)

extend to selectors, logical connectives, paths, and user

defined predicates.

defined predicates.

[IMPORTANT: check the differences with what we do here]

[IMPORTANT: check the differences with what we do here]

State what we capture already, for instance lists since we have product and recursive types.

State what we capture already, for instance lists since we have product and recursive types.

}

Occurrence typing was introduced by \citet{THF08} and further advanced

in \cite{THF10} in the context of the Typed Racket language. This

latter work in particular is close to ours, with some key differences.

The work of \cite{THF10} defines $\lambda_{TR}$, a core calculus for

typed racket. In this language types are annotated by logical

propositions that records the type of the input depending on the

(Boolean) value of the output. For instance, the type of the

{\tt number?} function states that when the output is {\tt true}, then

the argument has type {\tt Number}, and when the output is false, the

argument does not. Such information is used selectively

in the ``then'' and ``else'' branches of a test. One area where this

work goes further than ours is that the type informations also flows

outside of the tests to the surrounding context. In contrast, our type

system only refine the type of variables strictly in the branches of a

test. However using semantic-subtyping as a foundation we believe our

approach has several merrits over theirs. First, in our case, type

predicates are not built-in. A user may define any type predicate she

wishes by using an overloaded function, as we have shown in

Section~\ref{sec:practical}. Second, in our setting, {\em types\/} play

the role of formulæ. Using set-theoretic types, we can express the

complex types of variables without resorting to a meta-logic. This

allows us to type all but one of their key examples (with the notable

exception of their Example~8 which uses the propgation of type

information outside of the branches of a test). Also, while they

extend their core calculus with pairs, they only provide a simple {\tt

cons?} predicate that allows them to test whether some value is a

pair. It is therefore unclear whether their systems allows one to

write predicates over list types ({\em .e.g\/} test whether the input

is a list of integers), which we can easily do thanks to our support