Section~\ref{sec:practical} where we give several paradigmatic examples of code typed by our prototype implementation. Section~\ref{sec:related} presents

related work. A discussion of future work concludes this

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 union of their domain exactly covers the domain the third arrow,

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

of the function is left unannotated (that is, annotated by the top

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

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

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

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

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 \Int

nor \Bool).

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

nor in \Bool).

The following examples paint a more interesting picture. First

(Code~3) it is

easy in our formalism to provide type predicates such as those

hard-coded in the $\lambda_{TR}$ language of \cite{THF10}. Such type

hard-coded in the $\lambda_{\textit{TR}}$ language of \citet{THF10}. Such type

predicates, which return \texttt{true} if and only if their input has

a particular type, are just plain functions with an intersection

type. We then define Boolean combinators as overloaded

functions. The \texttt{not\_} combinator just tests whether its

type. We then define Boolean connectives as overloaded

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

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

the singleton type \True.

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

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

on the type it may return either a constant function that returns

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

the singleton type \True{} (the type whose only value is \texttt{true}) returning \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 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 \texttt{or\_} connective (Code~5) is defined as a

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

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

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

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

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

accordingly. Notice that we use here a generalized version of the

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

\texttt{true} as \texttt{false}. Again, we could restrict the initial

domain to \Bool if we wanted.

accordingly. Again we use a generalized version of the

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

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

domain to \Bool{} if we want.

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

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

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

type operation, we define \texttt{and\_} (Code~6) using De Morgan's

type operator, we define \texttt{and\_} (Code~6) using De Morgan's

Laws instead of

using a direct definition. Here the application of the outer

most \texttt{not\_} operator is checked against type \True. This

using a direct definition. Here the application of the outermost \texttt{not\_} operator is checked against type \True. This

allows the system to deduce that the whole \texttt{or\_} application

has type \False, which in turn leads to \texttt{not\_ x} and

\texttt{not\_ y} to have type $\lnot\True$ and therefore \texttt{x}

...

...

@@ -83,33 +84,32 @@ implementation, but the first arrow of the resulting type is

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

\texttt{x} which, in turn allows us to deduce a precise type.

\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:

\begin{alltt}\color{darkblue}

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))

\end{alltt}

for which the very same types as in Table~\ref{tab:implem} are deduced.