@@ -5,8 +5,9 @@ In this section we formalize the ideas we outlined in the introduction. We start

\fi

\subsection{Types}

\begin{definition}[Types]\label{def:types} The set of types \types{} is formed by the terms $t$ coinductively produced by the grammar:\vspace{-1.45mm}

\begin{definition}[Types]\label{def:types}

%\iflongversion%%%%%%%

The set of types \types{} is formed by the terms $t$ coinductively produced by the grammar:\vspace{-1.45mm}

\[

\begin{array}{lrcl}

\textbf{Types}& t & ::=& b\alt t\to t\alt t\times t\alt t\vee t \alt\neg t \alt\Empty

...

...

@@ -18,6 +19,17 @@ and that satisfy the following conditions

\item (contractivity) every infinite branch of a term contains an infinite number of occurrences of the

arrow or product type constructors.\vspace{-1mm}

\end{itemize}

\iffalse%%%%%%%%%%%%%%%%%%%%%%%%%%

A type $t\in\types{}$ is a term coinductively produced by the grammar:\vspace{-1.45mm}

\[

\begin{array}{lrcl}

\textbf{Types}& t & ::=& b\alt t\to t\alt t\times t\alt t\vee t \alt\neg t \alt\Empty

\end{array}

\]

that satisfies the following conditions: $(1)$\emph{Regularity}: the

term has a finite number of different sub-terms; $(2)$\emph{Contractivity}: every infinite branch of the term contains an infinite number of occurrences of the

arrow or product type constructors.\vspace{-1mm}

\fi%%%%%%%%%%%%%%%%%%%

\end{definition}

We use the following abbreviations: $

t_1\land t_2\eqdef\neg(\neg t_1\vee\neg t_2)$,

...

...

@@ -31,19 +43,22 @@ ill-formed types such as

$t = t \lor t$ (which does not carry any information about the set

denoted by the type) or $t =\neg t$ (which cannot represent any

set).

\iflongversion%%%%%%%%%%%%%%%%%%

It also ensures that the binary relation $\vartriangleright

\,\subseteq\!\types^{2}$ defined by $t_1\lor t_2\vartriangleright

t_i$, $t_1\land t_2\vartriangleright

t_i$, $\neg t \vartriangleright t$ is Noetherian.

This gives an induction principle on $\types$ that we

will use without any further explicit reference to the relation.\footnote{In a nutshell, we can do proofs by induction on the structure of unions and negations---and, thus, intersections---but arrows, products, and basic types are the base cases for the induction.}

\fi%%%%%%%%%%%%%%%%%%%%%%

We refer to $ b $, $\times$, and $\to$ as \emph{type constructors}

and to $\lor$, $\land$, $\lnot$, and $\setminus$

as \emph{type connectives}.

The subtyping relation for these types, noted $\leq$, is the one defined

by~\citet{Frisch2008} to which the reader may refer for the formal

definition (see~\cite{types18post} for a simpler alternative definition). A detailed description of the algorithm to decide it can be found in~\cite{Cas15}.

definition (see~\cite{types18post} for a simpler alternative

definition that we recall in Appendix~\ref{sec:subtyping}). A detailed description of the algorithm to decide it can be found in~\cite{Cas15}.

For this presentation it suffices to consider that

types are interpreted as sets of \emph{values} ({i.e., either

constants, $\lambda$-abstractions, or pairs of values: see

...

...

@@ -255,11 +270,11 @@ expression whose type environment contains an empty assumption:

Once more, this kind of deduction was already present in the system

by~\citet{Frisch2008} to type full fledged overloaded functions,

though it was embedded in the typing rule for the type-case.%

\ifsubmission%

~\pagebreak

\else

\fi%

%\ifsubmission%

%~\pagebreak

%\else

%

%\fi%

Here we

need the rule \Rule{Efq}, which is more general, to ensure the

The \emph{interpretation domain}$\Domain$ is the set of finite terms $ d $

produced inductively by the following grammar

...

...

@@ -30,7 +30,11 @@ supertype of all function types: if we used $d$ instead of $\domega$,

then every well-typed function could be subsumed to $\Any\to\Any$

and, therefore, every application could be given the type $\Any$,

independently from its argument as long as this argument is typable (see Section 4.2 of~\cite{Frisch2008} for details).

The restriction to \emph{finite} relations was explained in the introduction.

The restriction to \emph{finite} relations corresponds to the intuition

that the denotational semantics of a function is given by the set of

its finite approximations, where finiteness is a restriction necessary

(for cardinality reasons) to give the

semantics to higher-order functions.

We define the interpretation $\TypeInter{t}$ of a type $ t $

so that it satisfies the following equalities,

...

...

@@ -47,15 +51,22 @@ where $ \Pf $ denotes the restriction of the powerset to finite subsets:

\span\span

\span\span

\end{align*}

where $\ConstantsInBasicType{()}$ is the function

that assigns to each basic type the set of constants of that type, so

that $ c\in\ConstantsInBasicType(\basic{c})$.

We cannot take the equations above

directly as an inductive definition of $\TypeInter{}$

because types are not defined inductively but coinductively.

Therefore we give the following definition (due to~\citet{types18post}

Notice however that the contractivity condition of

Definition~\ref{def:types} ensures that the binary relation $\vartriangleright

\,\subseteq\!\types^{2}$ defined by $t_1\lor t_2\vartriangleright

t_i$, $t_1\land t_2\vartriangleright

t_i$, $\neg t \vartriangleright t$ is Noetherian.

This gives an induction principle \footnote{In a nutshell, we can do proofs by induction on the structure of unions and negations---and, thus, intersections---but arrows, products, and basic types are the base cases for the induction.} on $\types$ that we

we use to give the following definition (due to~\citet{types18post}

and equivalent to but simpler than the definition in~\cite{Frisch2008}),

which validates these equalities

and which uses the induction principle on types based on the relation $\vartriangleright$

and structural induction on $\Domain$.

which validates these equalities.

\begin{definition}[Set-theoretic interpretation of types~\cite{types18post}]\label{def:interpretation-of-types}