Intersection Subtyping with Constructors

TL;DR

This paper extends the BCD intersection type system with product types and a generic subtyping relation, ensuring type preservation during reduction and expansion, and introduces a unified framework for these extensions.

Contribution

It introduces a novel extension of the BCD intersection type system with product types and a generic subtyping relation, maintaining key properties.

Findings

Unified subtyping relation for intersection, omega, arrow, and product types.

Preservation of typing during reduction and expansion.

Framework based on a subformula property.

Abstract

We study the question of extending the BCD intersection type system with additional type constructors. On the typing side, we focus on adding the usual rules for product types. On the subtyping side, we consider a generic way of defining a subtyping relation on families of types which include intersection types. We find back the BCD subtyping relation by considering the particular case where the type constructors are intersection, omega and arrow. We obtain an extension of BCD subtyping to product types as another instance. We show how the preservation of typing by both reduction and expansion is satisfied in all the considered cases. Our approach takes benefits from a "subformula property" of the proposed presentation of the subtyping relation.

Tables

Table 1. Table 1: Typing Rules with Subtyping and Intersection.

var   $\Gamma ,x:A,\Delta ⊢x:A$   $\Gamma ⊢t:A$         $A\le B$  $\le$           $\Gamma ⊢t:B$   $\Gamma ⊢t:A$         $\Gamma ⊢t:B$  $\cap$          $\Gamma ⊢t:A\cap B$           $\Omega$   $\Gamma ⊢t:\Omega$

Table 2. Table 2: Kernel Properties of Subtyping.

	$A$	$\le A$		(refl)
	$A\le B\wedge B\le C$	$\Rightarrow A\le C$		(trans)
	$A\cap B$	$\le A$		(${\cap }_l^1$)
	$A\cap B$	$\le B$		(${\cap }_l^2$)
	$C\le A\wedge C\le B$	$\Rightarrow C\le A\cap B$		(${\cap }_r$)
	$A$	$\le \Omega$		(${\Omega }_r$)

Table 3. Table 3: Typing Rules for Arrow.

$\Gamma ,x:A⊢t:B$    abs   $\Gamma ⊢\lambda x.t:A\to B$                $\Gamma ⊢t:A\to B$         $\Gamma ⊢u:A$    app              $\Gamma ⊢tu:B$

Table 4. Table 4: BCD Subtyping Rules.

	$A\le A$   $A\le B$         $B\le C$           $A\le C$           $A\le \Omega$
	$A\cap B\le A$              $A\cap B\le B$             $A\le A\cap A$   $A\le C$         $B\le D$     $A\cap B\le C\cap D$
	$C\le A$         $B\le D$      $A\to B\le C\to D$                            $\left(A\to B\right)\cap \left(A\to C\right)\le A\to \left(B\cap C\right)$             $\Omega \le \Omega \to \Omega$

Table 5. Table 5: Typing Rules for Product.

$\Gamma ⊢t:A$         $\Gamma ⊢u:B$    pair        $\Gamma ⊢⟨t,u⟩:A\times B$                $\Gamma ⊢t:A\times B$    ${\text{proj}}_1$     $\Gamma ⊢{\pi }_{1}t:A$                $\Gamma ⊢t:A\times B$    ${\text{proj}}_2$     $\Gamma ⊢{\pi }_{2}t:B$

Table 6. Table 6: BCD -Style Subtyping Rules for Products.

$A\le C$         $B\le D$       $A\times B\le C\times D$                                                $\left(A\times B\right)\cap \left(C\times D\right)\le \left(A\cap C\right)\times \left(B\cap D\right)$

Table 7. Table 7: ISC Deduction System.

	$\Gamma ,\Delta ⊢C$  wk   $\Gamma ,\kappa (\overrightarrow{A};\overrightarrow{B}),\Delta ⊢C$   $\Gamma ⊢A$         $\Gamma ⊢B$  $\cap R$        $\Gamma ⊢A\cap B$    $\Gamma ,A,B,\Delta ⊢C$  $\cap L$   $\Gamma ,A\cap B,\Delta ⊢C$
	$\begin{array}{c}{A}_1⊢A_1^1\cdots A_1⊢A_1^k\\ ⋮\\ A_{{\alpha }_{\kappa }}⊢A_{{\alpha }_{\kappa }}^1\cdots A_{{\alpha }_{\kappa }}⊢A_{{\alpha }_{\kappa }}^k\end{array}$         $\begin{array}{c}{B}_1^1,\dots ,B_1^k⊢B_1\\ ⋮\\ B_{{\beta }_{\kappa }}^1,\dots ,B_{{\beta }_{\kappa }}^k⊢B_{{\beta }_{\kappa }}\end{array}$         $0pt\kappa \le k$  constr   $\kappa (A_1^1,\dots ,A_{{\alpha }_{\kappa }}^1;B_1^1,\dots ,B_{{\beta }_{\kappa }}^1),\dots ,\kappa (A_1^k,\dots ,A_{{\alpha }_{\kappa }}^k;B_1^k,\dots ,B_{{\beta }_{\kappa }}^k)⊢\kappa (A_1,\dots ,A_{{\alpha }_{\kappa }};B_1,\dots ,B_{{\beta }_{\kappa }})$

Table 8. Table 8: ISC Deduction System with → → \rightarrow and × \times .

	${\text{ax}}_{\text{at}}$   $X⊢X$        $\Omega$   $⊢\Omega$   $A⊢A_1$         $\cdots$         $A⊢A_k$         $B_1,\dots ,B_k⊢B$  $\to$               $A_1\to B_1,\dots ,A_k\to B_k⊢A\to B$      $⊢B$  ${\to }_0$   $⊢A\to B$
	$A_1,\dots ,A_k⊢A$         $B_1,\dots ,B_k⊢B$  $\times$     $A_1\times B_1,\dots ,A_k\times B_k⊢A\times B$

Equations

$$A,B::=X\mid A\cap B\mid \Omega \mid \dots$$

$$A,B::=X\mid A\cap B\mid \Omega \mid A\to B\mid \dots t,u::=x\mid \lambda x.t\mid tu\mid \dots$$

$$\bigcap _{i\in I}(A_i\to B_i)\le A\to B\Rightarrow \exists J\subseteq I,\left(\bigcap _{i\in J}{B}_i\le B\wedge \forall i\in J,A\le A_i\right)$$

$$A,B::=X\mid A\cap B\mid \Omega \mid A\to B\mid A\times B\mid \dots t,u::=x\mid \lambda x.t\mid tu\mid ⟨t,u⟩\mid {\pi }_{1}t\mid {\pi }_{2}t\mid \dots$$

$${\pi }_1⟨t,u⟩{\to }_{\pi }t{\pi }_2⟨t,u⟩{\to }_{\pi }u$$

$$\bigcap _{i\in I}(A_i\times B_i)\le A\times B\Rightarrow \bigcap _{i\in I}{A}_i\le A\wedge \bigcap _{i\in I}{B}_i\le B$$

$$A,B::=A\cap B\mid \kappa (\vec{A};\vec{B})$$

$$A_1,\dots ,A_k⊢B\text{“means”}{A}_1\cap \cdots \cap A_k\le B\text{(thus if k=0, B is a top type)}.$$

$$\displaystyle\begin{array}[]{c}\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower 25.19443pt\hbox{\vbox{\hbox{\hskip 4.0pt\hbox{$\Gamma\vdash C$}\hskip 4.0pt}\vskip 0.04723pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox to33.77904pt{\xleaders\hrule\hfill}\lower 1.95277pt\hbox{\hskip 3.0pt$\textit{ex}$}}\vskip 0.04723pt\nointerlineskip\hbox{\hskip 0.61885pt\hbox{\hbox{\hskip 4.0pt\hbox{$\Gamma^{\prime}\vdash C$}\hskip 4.0pt}}}}}\ignorespaces\\[8.61108pt] \text{$\Gamma^{\prime}$ permutation of $\Gamma$}\end{array}\qquad\qquad\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower 25.44444pt\hbox{\vbox{\hbox{\hskip 5.97221pt\hbox{\hskip 4.0pt\hbox{$\Gamma,\Delta\vdash C$}\hskip 4.0pt}}\vskip-2.41945pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox to57.39012pt{\xleaders\hrule\hfill}\lower 2.125pt\hbox{\hskip 3.0pt$\textit{wk}_{gen}$}}\vskip-2.41943pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$\Gamma,A,\Delta\vdash C$}\hskip 4.0pt}}}}\ignorespaces\qquad\qquad\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower 24.47221pt\hbox{\vbox{\hbox{\hskip 13.33328pt\hbox{\hskip 4.0pt\hbox{$$

}\hskip 4.0pt}}\vskip 0.04723pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox to34.66656pt{\xleaders\hrule\hfill}\lower 1.95277pt\hbox{\hskip 3.0pt$\text{ax}$}}\vskip 0.04723pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$A⊢A$}\hskip 4.0pt}}}}\ignorespaces$$

$$\Gamma ,A\cap B,\Delta ⊢C$$

$${\pi }_1$$

$$\begin{array}[]{c}\dotsb\quad A_{1}\vdash A_{1}^{i}\quad\dotsb\\ \vdots\\ \dotsb\quad A_{\alpha}\vdash A_{\alpha}^{i}\quad\dotsb\end{array}$$

$$⇝\text{scalebox}0.65\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{leavevmode}\text{lower}51.84386pt\text{vbox}\cdots \text{vbox}{C}_p⊢A_p{A}_p⊢A_p^i\text{vskip}-0.8754pt\text{nointerlineskip}\text{lower}-0.2ptto89.86397pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}2.8754pt\text{cut}\text{vskip}-0.8754pt\text{nointerlineskip}{C}_p⊢A_p^i\cdots \text{vbox}\dots ,B_p^i,\dots ⊢B_p\dots ,B_p,\dots ⊢D_p\text{vskip}-0.8754pt\text{nointerlineskip}\text{lower}-0.2ptto136.7632pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}2.8754pt\text{cut}\text{vskip}-0.8754pt\text{nointerlineskip}\dots ,B_p^i,\dots ⊢D_p\cdots \text{vskip}-0.8754pt\text{nointerlineskip}\text{lower}-0.2ptto364.72006pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}2.8754pt\text{constr}\text{vskip}-0.8754pt\text{nointerlineskip}\dots ,\kappa (A_1^i,\dots ,A_{\alpha }^i;B_1^i,\dots ,B_{\beta }^i),\dots ⊢\kappa (C_1,\dots ,C_{\alpha };D_1,\dots ,D_{\beta })\text{ignorespaces}$$

$$A_1⊢A_1^{i_1}\cdots A_1⊢A_1^{i_p}\cdots A_{{\alpha }_{\kappa }}⊢A_{{\alpha }_{\kappa }}^{i_1}\cdots A_{{\alpha }_{\kappa }}⊢A_{{\alpha }_{\kappa }}^{i_p}\text{and}{B}_1^{i_1},\dots ,B_1^{i_p}⊢B_1\cdots B_{{\beta }_{\kappa }}^{i_1},\dots ,B_{{\beta }_{\kappa }}^{i_p}⊢B_{{\beta }_{\kappa }}$$

$$C⊢C$$

$$A⊢A$$

$$\bigcap _{i\in I}(A_i\to B_i)\le A\to B\Rightarrow \exists J\subseteq I,\left(\bigcap _{i\in J}{B}_i\le B\wedge \forall i\in J,A\le A_i\right)$$

$$\bigcap _{i\in I}(A_i\times B_i)\le A\times B\Rightarrow \bigcap _{i\in I}{A}_i\le A\wedge \bigcap _{i\in I}{B}_i\le B$$

$$A,B::=X\mid A\to B\mid A\cap B\mid \Omega \mid \kappa (A)$$

$$A\le B$$

Full text

1 Introduction

Intersection type systems are tools for building and analysing models of the $\lambda$-calculus [BCDC83, Bak95, RDRP04, ABDC06]. They also provide ways of characterising reduction properties of $\lambda$-terms such as normalization. The main difference to other type systems is the fact that not only subject reduction holds (if $t$ reduces to $u$ and $\Gamma\vdash t:A$ then $\Gamma\vdash u:A$) but also subject expansion holds (if $t$ reduces to $u$ and $\Gamma\vdash u:A$ then $\Gamma\vdash t:A$). As a consequence it is possible to define a denotational model by associating to each (closed) term the set of its types $\llbracket t\rrbracket=\{A\mid{}\vdash t:A\}$.

The most famous intersection type system is probably the BCD system [BCDC83], and this is the one we are focusing on. While BCD insists on the interaction between arrow types and intersection types, we want to consider more general sets of type constructors, following [BCD*+*18]. The BCD type system can be decomposed into two parts: typing rules and subtyping rules. They are related through the subsumption rule. Our main contribution is a derivation system for the subtyping relation which allows us to deal with generic type constructors while satisfying a “subformula property”. Alternative presentations of BCD subtyping are studied in [Ven94]. In contrast with  [BCD*+*18], we allow contravariant type constructors so that even the arrow constructor can be defined as an instance of our generic pattern, and only intersection has a specific status.

In Section 2, we recall standard syntactic proofs [ABDC06, Lau12] of preservation of typing by $\beta$-reduction and $\beta$-expansion for the BCD system. Our presentation stresses the fact that, starting from intersection (and $\Omega$) only, type constructors can be added in a modular way. In Section 2.2, we consider the arrow types, thus obtaining the usual BCD rules. We extend the results to product types in Section 2.3. The main part of the paper is then Section 3 where we propose a sequent-style derivation system for defining BCD-like subtyping relations for extensions of intersection types to generic sets of constructors. Starting from a transitivity/cut admissibility property, we prove that instances of our system are equivalent with variants of the BCD subtyping relation.

Key results on subtyping (Propositions 5 and 6, and Theorem 1) are formalized in Coq:

https://perso.ens-lyon.fr/olivier.laurent/bcdc/

2 Intersection Typing

We present the system we are looking at, which is mainly BCD [BCDC83] extended with product types. Type constructors are introduced in an incremental and modular way.

2.1 Intersection Types

Let us first consider an at most countable set $\mathcal{X}$ of base types denoted $X$, $Y$, etc, and consider types built using at least the following constructors:

[TABLE]

Similarly we do not define the exact set of terms (denoted $t$, $u$, etc), but first we only assume they contain a denumerable set of term variables $\mathcal{V}$ (whose elements are denoted $x$, $y$, etc). A first set of typing rules is given on Table 1, with judgements $\Gamma\vdash t:A$ built from a list $\Gamma$ of typing declarations for variables (of the shape $x:B$), a term $t$ and a type $A$. Note these rules rely on a subtyping relation $\leq$ on types, which is here just a parameter.

Lemma 1** **(Weakening)

If $\Gamma\vdash t:A$ and $\Delta\leq\Gamma$ (meaning that, for each $x:B$ in $\Gamma$, one can find $x:B^{\prime}$ in $\Delta$ with $B^{\prime}\leq B$) then $\Delta\vdash t:A$.

Lemma 2** **(Strengthening)

If $\Gamma,x:B,\Delta\vdash t:A$ and $x\notin t$ then $\Gamma,\Delta\vdash t:A$.

Because it makes hypotheses on the term in conclusion, the rule (var) is called a term rule (the introduced term must be a variable). In the opposite, ($\leq$), ($\cap$) and ($\Omega$) rules are called non-term as they apply on any term without any constraint on its main constructor. As a term rule, (var) admits a so-called generation lemma analysing how variables can by typed. For this, we make some hypotheses on the subtyping relation (see Table 2).

Note in passing, that the axioms of Table 2 are equivalent to say that $\leq$ is a preorder relation with $\cap$ as greatest lower bound and $\Omega$ as top element. In particular, up to the equivalence relation induced by $\leq$, $\cap$ is a commutative associative idempotent operation with $\Omega$ as unit. As a consequence the notation $\bigcap_{i\in I}A_{i}$ makes sense (up to the equivalence relation induced by $\leq$) for any (possibly empty) finite set $I$.

Lemma 3** **(Generation for Variables)

Assuming that (var) is the only term rule introducing a variable, the only non-term rules are ($\leq$), ($\cap$) and ($\Omega$), and that the axioms of Table 2 are satisfied, we have: if $\Gamma\vdash x:A$ with $x:B\in\Gamma$ then $B\leq A$.

Lemma 4** **(Substitution)

If $\Gamma,x:A,\Delta\vdash t:B$ and $\Gamma,\Delta\vdash u:A$ then $\Gamma,\Delta\vdash t[{{}^{u}/_{x}}]:B$.

2.2 Arrow Types

We now assume types contain an arrow constructor and terms are extended correspondingly:

[TABLE]

The associated typing rules are given on Table 3. Note the two new rules are term rules corresponding respectively to $\lambda x.t$ and $t\,u$ (no new non-term rule).

By adding new cases corresponding to the added rules in the proofs, one can check that Lemmas 1 and 2 still hold. Moreover the hypotheses of Lemma 3 are still satisfied, and finally Lemma 4 (which only relies on the previous lemmas) is still true as well. Since terms may now contain binders (such as $\lambda x.\_$), substitution has to be considered as being capture-avoiding substitution.

Lemma 5** **(Generation for Application)

Assuming that (app) is the only term rule introducing an application, the only non-term rules are ($\leq$), ($\cap$) and ($\Omega$), and that the axioms of Table 2 are satisfied, we have: if $\Gamma\vdash t\,u:B$ then there exist two families of types $(A_{i})_{i\in I}$ and $(B_{i})_{i\in I}$ with $\bigcap_{i\in I}B_{i}\leq B$ and, for each $i\in I$, $\Gamma\vdash t:A_{i}\rightarrow B_{i}$ and $\Gamma\vdash u:A_{i}$.

Lemma 6** **(Generation for Abstraction)

Assuming that (abs) is the only term rule introducing an abstraction, the only non-term rules are ($\leq$), ($\cap$) and ($\Omega$), and that the axioms of Table 2 are satisfied, we have: if $\Gamma\vdash\lambda x.t:A$ then there exist two families of types $(B_{i})_{i\in I}$ and $(C_{i})_{i\in I}$ with $\bigcap_{i\in I}(B_{i}\rightarrow C_{i})\leq A$ and, for each $i\in I$, $\Gamma,x:B_{i}\vdash t:C_{i}$.

We now have the requested material to prove subject reduction and subject expansion. However a specific property on subtyping is still missing:

[TABLE]

The study of this property will be at the heart of Section 3.

Proposition 1** **(Subject Reduction)

Assuming ($\rightarrow\leq\rightarrow$ ‣ 2.2), if $t_{1}\rightarrow_{\beta}t_{2}$ and $\Gamma\vdash t_{1}:A$ then $\Gamma\vdash t_{2}:A$.

Proof.

The key case is $(\lambda x.t)\,u\rightarrow_{\beta}t[{{}^{u}/_{x}}]$. If $\Gamma\vdash(\lambda x.t)\,u:A$, by Lemma 5, we have two families $(B_{i})_{i\in I}$ and $(C_{i})_{i\in I}$ with $\bigcap_{i\in I}C_{i}\leq A$ and, for each $i\in I$, $\Gamma\vdash\lambda x.t:B_{i}\rightarrow C_{i}$ and $\Gamma\vdash u:B_{i}$. For each $i\in I$, by Lemma 6, we have two families $(B^{\prime}_{j})_{j\in J_{i}}$ and $(C^{\prime}_{j})_{j\in J_{i}}$ with $\bigcap_{j\in J_{i}}(B^{\prime}_{j}\rightarrow C^{\prime}_{j})\leq B_{i}\rightarrow C_{i}$ and, for each $j\in J_{i}$, $\Gamma,x:B^{\prime}_{j}\vdash t:C^{\prime}_{j}$. By ($\rightarrow\leq\rightarrow$ ‣ 2.2), there exists $K_{i}\subseteq J_{i}$ such that $B_{i}\leq B^{\prime}_{j}$ ($j\in K_{i}$) and $\bigcap_{j\in K_{i}}C^{\prime}_{j}\leq C_{i}$. We conclude by using Lemma 4 with $\Gamma\vdash u:B^{\prime}_{j}$:

$\dotsb$       

$\dotsb$         $\Gamma\vdash t[{{}^{u}/_{x}}]:C^{\prime}_{j}$         $\dotsb$

$\cap$

$\Gamma\vdash t[{{}^{u}/_{x}}]:\bigcap_{j\in K_{i}}C^{\prime}_{j}$

       $\bigcap_{j\in K_{i}}C^{\prime}_{j}\leq C_{i}$

$\leq$

$\Gamma\vdash t[{{}^{u}/_{x}}]:C_{i}$

       $\dotsb$

$\cap$

$\Gamma\vdash t[{{}^{u}/_{x}}]:\bigcap_{i\in I}C_{i}$

       $\bigcap_{i\in I}C_{i}\leq A$

$\leq$

$\Gamma\vdash t[{{}^{u}/_{x}}]:A$

∎

Proposition 2** **(Subject Expansion)

If $t_{1}\rightarrow_{\beta}t_{2}$ and $\Gamma\vdash t_{2}:A$ then $\Gamma\vdash t_{1}:A$.

Proof.

The key case is $(\lambda x.t)\,u\rightarrow_{\beta}t[{{}^{u}/_{x}}]$. We first prove that $\Gamma\vdash t[{{}^{u}/_{x}}]:B$ implies that we can find a type $A$ such that $\Gamma,x:A\vdash t:B$ and $\Gamma\vdash u:A$, by induction on the derivation of $\Gamma\vdash t[{{}^{u}/_{x}}]:B$. And then:

$\Gamma,x:A\vdash t:B$

abs

$\Gamma\vdash\lambda x.t:A\rightarrow B$

       $\Gamma\vdash u:A$

app

$\Gamma\vdash(\lambda x.t)\,u:B$

∎

To sum up, we have shown that, given the typing rules of Tables 1 and 3, the subject reduction and subject expansion properties hold for $\beta$-reduction as soon as the chosen subtyping satisfies the axioms of Table 2 as well as property ($\rightarrow\leq\rightarrow$ ‣ 2.2). The historical example from the literature is the BCD system [BCDC83] corresponding to the subtyping relation of Table 4. We will come back to the fact that ($\rightarrow\leq\rightarrow$ ‣ 2.2) holds for this BCD relation (Lemma 11).

2.3 Product Types

We now assume types contain a product constructor and terms are extended correspondingly:

[TABLE]

The associated typing rules are given on Table 5. Note the new rules are all term rules (no non-term rule added). Lemmas 1, 2, 3 and 4 still hold. It is also easy to check that the new rules do not break Propositions 1 and 2.

Lemma 7** **(Generation for Pairing)

Assuming that (pair) is the only term rule introducing a pair, the only non-term rules are ($\leq$), ($\cap$) and ($\Omega$), and that the axioms of Table 2 are satisfied, we have: if $\Gamma\vdash\langle t,u\rangle:A$ then there exist two families of types $(B_{i})_{i\in I}$ and $(C_{i})_{i\in I}$ with $\bigcap_{i\in I}(B_{i}\times C_{i})\leq A$ and, for each $i\in I$, $\Gamma\vdash t:B_{i}$ and $\Gamma\vdash u:C_{i}$.

Proof.

By induction on the typing derivation of $\Gamma\vdash\langle t,u\rangle:A$, by looking at each possible last rule which, by assumption, can only be (pair), ($\leq$), ($\cap$) or ($\Omega$):

• •

(pair) rule: $I$ is a singleton and the result is immediate.

• •

($\leq$) rule: we have $\Gamma\vdash\langle t,u\rangle:A^{\prime}$ with $A^{\prime}\leq A$, we apply the induction hypothesis to $\Gamma\vdash\langle t,u\rangle:A^{\prime}$, and we conclude by (trans).

• •

($\cap$) rule: we have $A=A^{\prime}\cap A^{\prime\prime}$, by induction hypotheses we obtain families of types indexed by $I^{\prime}$ and $I^{\prime\prime}$ and we consider $I=I^{\prime}\uplus I^{\prime\prime}$. We conclude by using $E_{1}\leq E_{2}\;\wedge\;F_{1}\leq F_{2}\;\Rightarrow\;E_{1}\cap F_{1}\leq E_{2}\cap F_{2}$.

• •

($\Omega$) rule: we simply choose $I=\emptyset$. ∎

Lemma 8** **(Generation for Left Projection)

Assuming that ($\textit{proj}_{1}$) is the only term rule introducing a left projection, the only non-term rules are ($\leq$), ($\cap$) and ($\Omega$), and that the axioms of Table 2 are satisfied, we have: if $\Gamma\vdash\pi_{1}\,t:A$ then there exist two families of types $(B_{i})_{i\in I}$ and $(C_{i})_{i\in I}$ with $\bigcap_{i\in I}B_{i}\leq A$ and, for each $i\in I$, $\Gamma\vdash t:B_{i}\times C_{i}$.

Proof.

By induction on the typing derivation of $\Gamma\vdash\pi_{1}\,t:A$, by looking at each possible last rule which, by assumption, can only be ($\textit{proj}_{1}$), ($\leq$), ($\cap$) or ($\Omega$):

• •

($\textit{proj}_{1}$) rule: $I$ is a singleton and the result is immediate.

• •

($\leq$) rule: we have $\Gamma\vdash\pi_{1}\,t:A^{\prime}$ with $A^{\prime}\leq A$, we apply the induction hypothesis to $\Gamma\vdash\pi_{1}\,t:A^{\prime}$, and we conclude by (trans).

• •

($\cap$) rule: we have $A=A^{\prime}\cap A^{\prime\prime}$, by induction hypotheses we obtain families of types indexed by $I^{\prime}$ and $I^{\prime\prime}$ and we consider $I=I^{\prime}\uplus I^{\prime\prime}$. We conclude by using $E_{1}\leq E_{2}\;\wedge\;F_{1}\leq F_{2}\;\Rightarrow\;E_{1}\cap F_{1}\leq E_{2}\cap F_{2}$.

• •

($\Omega$) rule: we simply choose $I=\emptyset$. ∎

Lemma 9** **(Generation for Right Projection)

Assuming that ($\textit{proj}_{2}$) is the only term rule introducing a right projection, the only non-term rules are ($\leq$), ($\cap$) and ($\Omega$), and that the axioms of Table 2 are satisfied, we have: if $\Gamma\vdash\pi_{2}\,t:A$ then there exist two families of types $(B_{i})_{i\in I}$ and $(C_{i})_{i\in I}$ with $\bigcap_{i\in I}C_{i}\leq A$ and, for each $i\in I$, $\Gamma\vdash t:B_{i}\times C_{i}$.

Proof.

Similar to the proof of Lemma 8. ∎

We consider the reduction $\rightarrow_{\pi}$ to be the congruence generated by:

[TABLE]

Similarly to the arrow case, we ask for an additional property of the subtyping relation in order to deduce subject reduction:

[TABLE]

Proposition 3** **(Subject Reduction for Products)

Assuming ($\times\leq\times$ ‣ 2.3), if $t_{1}\rightarrow_{\pi}t_{2}$ and $\Gamma\vdash t_{1}:A$ then $\Gamma\vdash t_{2}:A$.

Proof.

The key case is $\pi_{1}\,\langle t,u\rangle\rightarrow_{\pi}t$. If $\Gamma\vdash\pi_{1}\,\langle t,u\rangle:A$, by Lemma 8, we have two families $(B_{i})_{i\in I}$ and $(C_{i})_{i\in I}$ with $\bigcap_{i\in I}B_{i}\leq A$ and, for each $i\in I$, $\Gamma\vdash\langle t,u\rangle:B_{i}\times C_{i}$. For each $i\in I$, by Lemma 7, we have two families $(B^{\prime}_{j})_{j\in J_{i}}$ and $(C^{\prime}_{j})_{j\in J_{i}}$ with $\bigcap_{j\in J_{i}}(B^{\prime}_{j}\times C^{\prime}_{j})\leq B_{i}\times C_{i}$ and, for each $j\in J_{i}$, $\Gamma\vdash t:B^{\prime}_{j}$ and $\Gamma\vdash u:C^{\prime}_{j}$. By ($\times\leq\times$ ‣ 2.3), $\bigcap_{j\in J_{i}}B^{\prime}_{j}\leq B_{i}$. We conclude by:

$\dotsb$       

$\dotsb$         $\Gamma\vdash t:B^{\prime}_{j}$         $\dotsb$

$\cap$

$\Gamma\vdash t:\bigcap_{j\in J_{i}}B^{\prime}_{j}$

       $\bigcap_{j\in J_{i}}B^{\prime}_{j}\leq B_{i}$

$\leq$

$\Gamma\vdash t:B_{i}$

       $\dotsb$

$\cap$

$\Gamma\vdash t:\bigcap_{i\in I}B_{i}$

       $\bigcap_{i\in I}B_{i}\leq A$

$\leq$

$\Gamma\vdash t:A$

∎

Proposition 4** **(Subject Expansion for Products)

If $t_{1}\rightarrow_{\pi}t_{2}$ and $\Gamma\vdash t_{2}:A$ then $\Gamma\vdash t_{1}:A$.

Proof.

The key case is $\pi_{1}\,\langle t,u\rangle\rightarrow_{\pi}t$. We have:

$\Gamma\vdash t:A$       

$\Omega$

$\Gamma\vdash u:\Omega$

pair

$\Gamma\vdash\langle t,u\rangle:A\times\Omega$

$\textit{proj}_{1}$

$\Gamma\vdash\pi_{1}\,\langle t,u\rangle:A$

∎

Following [BCD*+*18] in extending BCD subtyping in the context of additional type constructors, we can consider the rules of Table 6 for subtyping with products. This system satisfies property ($\times\leq\times$ ‣ 2.3) (Lemma 12).

While the present section focused on the product extension of BCD, our purpose is to use it as a concrete application of a more general pattern of subtyping between types which include intersection as well as other type constructors. What should be remembered from what we have done so far, is that we can get subject reduction and subject expansion as soon as the subtyping relation satisfies Table 2 as well as ($\rightarrow\leq\rightarrow$ ‣ 2.2) and ($\times\leq\times$ ‣ 2.3). The next section provides a general approach to these results.

3 Intersection Subtyping

Inspired by [BCD*+*18], we directly consider types built with an arbitrary set of constructors. The case of $\times$ for example will be obtained as a particular instance. We go in fact one step further than [BCD*+*18] by allowing enough generality in the treatment of constructors so that $\rightarrow$ appears as a constructor among others and not as a specific one as given in [BCD*+*18].

3.1 Generic Subtyping with Constructors

We consider a given set $\mathcal{K}$ of type constructors (denoted $\kappa$, $\kappa_{1}$, $\kappa_{2}$, etc) which come with a contravariant arity $\alpha_{\kappa}$ and a covariant arity $\beta_{\kappa}$. We assume that arities are respected when constructing types, so that if $\alpha_{\kappa}=2$ and $\beta_{\kappa}=1$, then $\kappa(A,B;C)$ is a type when $A$, $B$ and $C$ are three types. Moreover, for each constructor $\kappa$, a $\{0,1\}$-value $0pt{\kappa}$ defines its behaviour with respect to top types (see below).

Types are thus generated through:

[TABLE]

Base types are provided by constructors with zero arities.

We introduce a sequent-calculus-style derivation system ISC to define the subtyping relation on these types. We will show that applying proof-theoretical methods, such as cut elimination, allows us to deduce easily some properties of subtyping such as Lemma 10.

Sequents are of the shape $\Gamma\vdash A$ where $\Gamma$ is a (possibly empty) list of types. The intended meaning is:

[TABLE]

The derivation rules are given in Table 7 and satisfy the subformula property.

Proposition 5** **(Admissible Rules)

The following rules are admissible in ISC:

[TABLE]

Proof.

(ex) is obtained by induction on the proof of the premise. ($\textit{wk}_{gen}$) is obtained by induction on $A$. (ax) is obtained by induction on $A$ using ($\textit{wk}_{gen}$). (${\cap}L_{e}$) is obtained by induction on the premise.

(co) is obtained by induction on the lexicographically ordered pair (size of $A$, height of the proof of the premise), by looking at each possible last rule of the premise. The key case is (${\cap}L$):

$\Gamma,A,B,A\cap B,\Delta\vdash C$

${\cap}L$

$\Gamma,A\cap B,A\cap B,\Delta\vdash C$

we apply (${\cap}L_{e}$) and (ex) to the premise to get $\Gamma,A,A,B,B,\Delta\vdash C$ and we use the induction hypothesis twice.

(cut) is obtained by induction on the lexicographically ordered triple (size of $A$, height of the proof of the left premise, height of the proof of the right premise), by looking at possible last rules of the premises. Let us focus on the main cases:

• •

(${\cap}R$) rule on the right:

[TABLE]

we use the induction hypothesis twice with a decreasing height on the right.

• •

(${\cap}R$) rule on the left and $({\cap}L)$ rule on the right:

[TABLE]

we use the induction hypothesis twice with smaller cut formulas.

• •

(constr) rules on both sides (in which we only write the key parts):

[TABLE]

we use the induction hypothesis many times (always with smaller cut formulas). ∎

Note a [math]-ary constructor $\kappa$ behaves like an atomic type (i.e. either a type constant or a type variable) if $0pt{\kappa}=1$, and defines a top type if $0pt{\kappa}=0$:

$0pt{\kappa}\leq 0$

constr

$\vdash\kappa$

$\textit{wk}_{gen}$

$A\vdash\kappa$

In particular the types obtained with such [math]-ary constructors $\kappa$ such that $0pt{\kappa}=0$ are all equivalent and we denote them $\Omega$. More generally, $0pt{\kappa}$ controls whether $\kappa$ distributes over $\Omega$ or not. In the case of a constructor with unary covariant arity, $0pt{\kappa}$ determines whether $\kappa(\vec{A};\Omega)=\Omega$ or not.

Proposition 6** **(Kernel Properties)

If we define $A\leq B$ as $A\vdash B$ in ISC, the axioms of Table 2 are satisfied.

Proof.

(refl) and (trans) correspond to (ax) and (cut) from Proposition 5. ($\cap_{r}$) is an instance of (${\cap}R$) and for ($\cap_{l}^{1}$) we have:

ax

$A\vdash A$

$\textit{wk}_{gen}$

$A,B\vdash A$

${\cap}L$

$A\cap B\vdash A$

Finally, if we have a [math]-ary constructor $\Omega$ with $0pt{\Omega}=0$, we have just seen it satisfies ($\Omega_{r}$). ∎

Lemma 10** **(Inversion)

If $\kappa(A_{1}^{1},\dotsc,A_{\alpha_{\kappa}}^{1};B_{1}^{1},\dotsc,B_{\beta_{\kappa}}^{1}),\dotsc,\kappa(A_{1}^{k},\dotsc,A_{\alpha_{\kappa}}^{k};B_{1}^{k},\dotsc,B_{\beta_{\kappa}}^{k})\vdash\kappa(A_{1},\dotsc,A_{\alpha_{\kappa}};B_{1},\dotsc,B_{\beta_{\kappa}})$, there exists $\{i_{1},\dotsc,i_{p}\}\subseteq\{1,\dotsc,k\}$ such that:

[TABLE]

Proof.

By induction on the derivation of $\kappa(A_{1}^{1},\dotsc,A_{\alpha_{\kappa}}^{1};B_{1}^{1},\dotsc,B_{\beta_{\kappa}}^{1}),\dotsc,\kappa(A_{1}^{k},\dotsc,A_{\alpha_{\kappa}}^{k};B_{1}^{k},\dotsc,B_{\beta_{\kappa}}^{k})\vdash\kappa(A_{1},\dotsc,A_{\alpha_{\kappa}};B_{1},\dotsc,B_{\beta_{\kappa}})$, with only (wk) and (constr) as possible last rules. ∎

3.2 The Arrow-Product Instance

We consider the following set of constructors:

• •

an at most countable set of [math]-ary constructors denoted $X$, $Y$, etc, such that $0pt{X}=0pt{Y}=\dotsb=1$;

• •

a [math]-ary constructor $\Omega$ with $0pt{\Omega}=0$;

• •

a constructor $\rightarrow$ with contravariant arity $1$ and covariant arity $1$ such that $0pt{\rightarrow}=0$;

• •

a constructor $\times$ with contravariant arity [math] and covariant arity $2$ such that $0pt{\times}=1$.

By instantiating the $(\textit{constr})$ rule of Table 7 to this set of constructors, and using the (wk) rule to simplify the $X$ and $\Omega$ cases, we obtain the rules of Table 8 where $k\geq 1$.

Theorem 1** **(Equivalence with BCD)

$A\vdash B$* in ISC with the (constr) rule instantiated as given in Table 8 if and only if $A\leq B$ using the rules of Table 4 extended with the rules of Table 6.*

Proof.

From left to right, we prove a slightly more general statement: $A_{1},\dotsc,A_{k}\vdash B$ implies $\bigcap_{1\leq i\leq k}A_{i}\leq B$. From right to left, the key results are in Propositions 5 and 6. Main cases are:

[TABLE]

∎

Lemma 11** **(Inversion for Arrow)

If $A\leq B$ is obtained from Tables 4 and 6, we have:

[TABLE]

This is the key property of subtyping allowing for subject $\beta$-reduction to hold in the BCD typing system. While the traditional proof goes by induction on the derivation which requires a more general statement to deal with the transitivity rule, we rely here on the subformula property. The traditional approach seems more difficult to use in a context where we may have many type constructors.

Proof.

By Theorem 1, we have $\bigcap_{i\in I}(A_{i}\rightarrow B_{i})\vdash A\rightarrow B$, thus if $I=\{1,\dotsb,k\}$, we get $A_{1}\rightarrow B_{1},\dotsc,A_{k}\rightarrow B_{k}\vdash A\rightarrow B$ by Proposition 5. By applying Lemma 10, we obtain $A\vdash A_{i_{1}}$,…, $A\vdash A_{i_{p}}$, $B_{i_{1}},\dotsc,B_{i_{p}}\vdash B$ with $J=\{i_{1},\dotsc,i_{p}\}\subseteq I$, so that $\bigcap_{i\in J}B_{i}\vdash B$, and we conclude with Theorem 1. ∎

Lemma 12** **(Inversion for Product)

If $A\leq B$ is obtained from Tables 4 and 6, we have:

[TABLE]

Proof.

Similarly by Theorem 1, Proposition 5 and Lemma 10. ∎

3.3 BCD Subtyping with Unary Constructors

Our system ISC also generalises BCD subtyping with unary covariant constructors [BCD*+*18]. In their setting constructors come as a set of unary covariant operations $\kappa$ on types added to the usual $\rightarrow$ and $\Omega$ constructors:

[TABLE]

where each constructor $\kappa$ satisfies the following subtyping properties:

[TABLE]

This exactly corresponds, in the ISC setting, to a set of constructors $\kappa$ all satisfying $\alpha_{\kappa}=0$, $\beta_{\kappa}=1$ and $0pt{\kappa}=1$ (the constructors $\rightarrow$ and $\Omega$ are obtained as before). For example the associated (constr) rule can be derived in the [BCD*+*18] setting:

$\bigcap_{1\leq i\leq k}\kappa(A_{i})\leq\kappa(\bigcap_{1\leq i\leq k}A_{i})$

     

$\bigcap_{1\leq i\leq k}A_{i}\leq A$

$\kappa(\bigcap_{1\leq i\leq k}A_{i})\leq\kappa(A)$

$\bigcap_{1\leq i\leq k}\kappa(A_{i})\leq\kappa(A)$

4 Conclusion

We have presented a general way of defining a subtyping relation on intersection types which allows us to extend the BCD subtyping to generic contravariant/covariant type constructors. It makes easy to derive key properties used to get subject reduction and subject expansion of the induced type systems. As a concrete example we have fully developed the extension of BCD with product types.

Our approach can be extended to the case where a preorder relation $\preccurlyeq$ between constructors (with the same arities) leads to $\kappa_{1}\preccurlyeq\kappa_{2}\;\Rightarrow\;\kappa_{1}(\vec{A};\vec{B})\leq\kappa_{2}(\vec{A};\vec{B})$, by a natural generalisation of the (constr) rule:

\begin{array}[b]{c}\kappa_{1}\preccurlyeq\kappa\\ \vdots\\ \kappa_{k}\preccurlyeq\kappa\end{array}         \begin{array}[b]{c}A_{1}\vdash A_{1}^{1}\quad\dotsb\quad A_{1}\vdash A_{1}^{k}\\ \vdots\\ A_{\alpha_{\kappa}}\vdash A_{\alpha_{\kappa}}^{1}\quad\dotsb\quad A_{\alpha_{\kappa}}\vdash A_{\alpha_{\kappa}}^{k}\end{array}         \begin{array}[b]{c}B_{1}^{1},\dotsc,B_{1}^{k}\vdash B_{1}\\ \vdots\\ B_{\beta_{\kappa}}^{1},\dotsc,B_{\beta_{\kappa}}^{k}\vdash B_{\beta_{\kappa}}\end{array}         $0pt{\kappa}\leq k$

$\kappa_{1}(A_{1}^{1},\dotsc,A_{\alpha_{\kappa}}^{1};B_{1}^{1},\dotsc,B_{\beta_{\kappa}}^{1}),\dotsc,\kappa_{k}(A_{1}^{k},\dotsc,A_{\alpha_{\kappa}}^{k};B_{1}^{k},\dotsc,B_{\beta_{\kappa}}^{k})\vdash\kappa(A_{1},\dotsc,A_{\alpha_{\kappa}};B_{1},\dotsc,B_{\beta_{\kappa}})$

Ordering constructors is natural in the context of object-oriented languages [KP07, BCD*+*18].

Another interesting instance would be the study of sum types, but subject expansion looks more complicated. From $\Gamma\vdash u[{{}^{t}/_{x}}]:C$, we can find some type $A$ such that $\Gamma\vdash t:A$ and $\Gamma,x:A\vdash u:C$, but we do not find a way to complete the following derivation:

$\Gamma\vdash t:A$

$\Gamma\vdash\texttt{inl }t:A+\_$

       $\Gamma,x:A\vdash u:C$       

?

$\Gamma,y:\_\vdash v:C$

\Gamma\vdash\begin{array}[c]{l}\texttt{match inl }t\texttt{ with}\\ \mid\;\texttt{inl }x\;\mapsto\;u\\ \mid\;\texttt{inr }y\;\mapsto\;v\end{array}:C

while  $\texttt{match inl }t\texttt{ with}\mid\texttt{inl }x\;\mapsto\;u\mid\texttt{inr }y\;\mapsto\;v$ reduces to  $u[{{}^{t}/_{x}}]$. The idea of introducing some bottom type $\alpha$ with a rule

$\Gamma,x:\alpha\vdash t:C$

seems too naive and breaks the system.

We also plan to work on the characterisation of normalizability properties of terms through typing properties in intersection type systems: solvability, normalization, strong normalization, etc. We would like to extend the known results [BCDC83] to the case with more type constructors.

Acknowledgements.

We would like to thank to Jan Bessai and Andrej Dudenhefner who suggested investigating BCD with constructors. Thanks also to the anonymous referees for their comments.