@@ -5,14 +5,14 @@ system of Section~\ref{sec:static}. In particular, as we

...

@@ -5,14 +5,14 @@ system of Section~\ref{sec:static}. In particular, as we

explained in Section~\ref{ssec:algorithm}, in the absence of type

explained in Section~\ref{ssec:algorithm}, in the absence of type

schemes it is not always possible to prove that $\forall v, \forall t,

schemes it is not always possible to prove that $\forall v, \forall t,

v \in t \text{~or~} v \not\in\lnot t$. Since this property cease

v \in t \text{~or~} v \not\in\lnot t$. Since this property cease

to hold only for $\lambda$-expressions, then not using type schemes

to hold only for $\lambda$-abstractions, then not using type schemes

yields less precise typing only for tests $\ifty{e}t{e_1}{e_2}$ where $e$

yields less precise typing only for tests $\ifty{e}t{e_1}{e_2}$ where $e$

has a functional type, that is the value tested will be a $\lambda$

has a functional type, that is, the value tested will be a $\lambda$-abstraction.

abstraction This seems like a reasonable compromise between the

This seems like a reasonable compromise between the

complexity of an implementation involving type scheme and the programs

complexity of an implementation involving type scheme and the programs

we want to type-check in practice. Indeed if we restrict the language

we want to type-check in practice. Indeed, if we restrict the language

so that the only functional type $t$ allowed in $\ifty{e}t{e_1}{e_2}$

so that the only functional type $t$ allowed in a test $\ifty{e}t{e_1}{e_2}$

is $\Empty\to\Any$---i.e., we allow to check whether a value is a

is $\Empty{\to}\Any$---i.e., if we allow to check whether a value is a

function but not whether it has a specific function type (\emph{cf.}, Footnote~\ref{foo:typecase})---, then our

function but not whether it has a specific function type (\emph{cf.}, Footnote~\ref{foo:typecase})---, then our

implementation becomes complete.

implementation becomes complete.

...

@@ -21,11 +21,11 @@ provide the semantic sub-typing machinery. Besides a type-checking

...

@@ -21,11 +21,11 @@ provide the semantic sub-typing machinery. Besides a type-checking

algorithm defined on the base language, our implementation supports

algorithm defined on the base language, our implementation supports

record types (Section \ref{ssec:struct}) and the refinement of function types

record types (Section \ref{ssec:struct}) and the refinement of function types

(Section \ref{sec:refining}). The implementation is rather crude and

(Section \ref{sec:refining}). The implementation is rather crude and

consits of 2000 lines of OCaml code, including parsing, type-checking

consist of 2000 lines of OCaml code, including parsing, type-checking

of programs and pretty printing of types. We demonstrate the output of

of programs and pretty printing of types. We demonstrate the output of

our type-checking implementation in Table~\ref{tab:implem}.

our type-checking implementation in Table~\ref{tab:implem}.

\input{code_table}

\input{code_table}

In this table, the second column gives a code fragment and third

In this table, the second column gives a code fragment and the third

column the type deduced by our implementation. Code~1 is a

column the type deduced by our implementation. Code~1 is a

straightforward function similar to our introductory example \code{foo} in (\ref{foo},\ref{foo2}). Here the

straightforward function similar to our introductory example \code{foo} in (\ref{foo},\ref{foo2}). Here the

programmer annotates the parameter of the function with a coarse type

programmer annotates the parameter of the function with a coarse type

...

@@ -51,14 +51,14 @@ nor in \Bool).

...

@@ -51,14 +51,14 @@ nor in \Bool).

The following examples paint a more interesting picture. First

The following examples paint a more interesting picture. First

(Code~3) it is

(Code~3) it is

easy in our formalism to provide type predicates such as those

easy in our formalism to program type predicates such as those

hard-coded in the $\lambda_{\textit{TR}}$ language of \citet{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

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

a particular type, are just plain functions with an intersection

a particular type, are just plain functions with an intersection

type. We then 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{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 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 \texttt{or\_} connective (Code~5) is defined as a

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

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

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

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

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

...

@@ -67,7 +67,7 @@ discriminates on its argument (which is the second argument of the

...

@@ -67,7 +67,7 @@ discriminates on its argument (which is the second argument of the

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

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

accordingly. Again we use a generalized version of the

accordingly. 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 initial

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

domain to \Bool{} if we want.

domain to \Bool{} if we want.

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

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

...

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

...

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

Laws instead of

Laws instead of

using a direct definition. Here the application of the outermost \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

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

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

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

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

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

and \texttt{y} to have type \True. The whole function is typed with

and \texttt{y} to have type \True. The whole function is typed with

the most precise type (we present the type as printed by our

the most precise type (we present the type as printed by our

implementation, but the first arrow of the resulting type is

implementation, but the first arrow of the resulting type is

...

@@ -122,7 +122,7 @@ further improve the precision of the inferred type.

...

@@ -122,7 +122,7 @@ 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

$\Any\to\Any\to\Bool$. Let us follow the behaviour of the

$\Any\to\Any\to\Bool$. Let us follow the behavior of the

``$\worra{}{}$'' operator. Here the whole \texttt{and\_} is requested

``$\worra{}{}$'' operator. Here the whole \texttt{and\_} is requested

to have type \True, which implies that \texttt{or\_ x y} must have

to have type \True, which implies that \texttt{or\_ x y} must have

type \True. This can always happen, whether \texttt{x} is \True{} or

type \True. This can always happen, whether \texttt{x} is \True{} or