Intersection Subtyping with Constructors
Olivier Laurent (Univ Lyon, EnsL, UCBL, CNRS, LIP, F-69342, LYON Cedex, 07, France)

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.
| var |
| (refl) | ||||
| (trans) | ||||
| () | ||||
| () | ||||
| () | ||||
| () |
| abs app |
| pair |
| wk | ||
| constr |
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Intersection Subtyping with Constructors
Olivier Laurent This work was supported by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program “Investissements d’Avenir” (ANR-11-IDEX-0007), and by the project Elica (ANR-14-CE25-0005), both operated by the French National Research Agency (ANR). This work was also supported by GDRI Linear Logic.Univ Lyon, EnsL, UCBL, CNRS, LIP, F-69342, LYON Cedex 07, France [email protected]
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.
1 Introduction
Intersection type systems are tools for building and analysing models of the -calculus [BCDC83, Bak95, RDRP04, ABDC06]. They also provide ways of characterising reduction properties of -terms such as normalization. The main difference to other type systems is the fact that not only subject reduction holds (if reduces to and then ) but also subject expansion holds (if reduces to and then ). As a consequence it is possible to define a denotational model by associating to each (closed) term the set of its types .
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 -reduction and -expansion for the BCD system. Our presentation stresses the fact that, starting from intersection (and ) 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 of base types denoted , , etc, and consider types built using at least the following constructors:
[TABLE]
Similarly we do not define the exact set of terms (denoted , , etc), but first we only assume they contain a denumerable set of term variables (whose elements are denoted , , etc). A first set of typing rules is given on Table 1, with judgements built from a list of typing declarations for variables (of the shape ), a term and a type . Note these rules rely on a subtyping relation on types, which is here just a parameter.
Lemma 1** **(Weakening)
If and (meaning that, for each in , one can find in with ) then .
Lemma 2** **(Strengthening)
If and then .
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, (), () and () 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 is a preorder relation with as greatest lower bound and as top element. In particular, up to the equivalence relation induced by , is a commutative associative idempotent operation with as unit. As a consequence the notation makes sense (up to the equivalence relation induced by ) for any (possibly empty) finite set .
Lemma 3** **(Generation for Variables)
Assuming that (var) is the only term rule introducing a variable, the only non-term rules are (), () and (), and that the axioms of Table 2 are satisfied, we have: if with then .
Lemma 4** **(Substitution)
If and then .
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 and (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 ), 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 (), () and (), and that the axioms of Table 2 are satisfied, we have: if then there exist two families of types and with and, for each , and .
Lemma 6** **(Generation for Abstraction)
Assuming that (abs) is the only term rule introducing an abstraction, the only non-term rules are (), () and (), and that the axioms of Table 2 are satisfied, we have: if then there exist two families of types and with and, for each , .
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 ( ‣ 2.2), if and then .
Proof.
The key case is . If , by Lemma 5, we have two families and with and, for each , and . For each , by Lemma 6, we have two families and with and, for each , . By ( ‣ 2.2), there exists such that () and . We conclude by using Lemma 4 with :
∎
Proposition 2** **(Subject Expansion)
If and then .
Proof.
The key case is . We first prove that implies that we can find a type such that and , by induction on the derivation of . And then:
abs
app
∎
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 -reduction as soon as the chosen subtyping satisfies the axioms of Table 2 as well as property ( ‣ 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 ( ‣ 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 (), () and (), and that the axioms of Table 2 are satisfied, we have: if then there exist two families of types and with and, for each , and .
Proof.
By induction on the typing derivation of , by looking at each possible last rule which, by assumption, can only be (pair), (), () or ():
- •
(pair) rule: is a singleton and the result is immediate.
- •
() rule: we have with , we apply the induction hypothesis to , and we conclude by (trans).
- •
() rule: we have , by induction hypotheses we obtain families of types indexed by and and we consider . We conclude by using .
- •
() rule: we simply choose . ∎
Lemma 8** **(Generation for Left Projection)
Assuming that () is the only term rule introducing a left projection, the only non-term rules are (), () and (), and that the axioms of Table 2 are satisfied, we have: if then there exist two families of types and with and, for each , .
Proof.
By induction on the typing derivation of , by looking at each possible last rule which, by assumption, can only be (), (), () or ():
- •
() rule: is a singleton and the result is immediate.
- •
() rule: we have with , we apply the induction hypothesis to , and we conclude by (trans).
- •
() rule: we have , by induction hypotheses we obtain families of types indexed by and and we consider . We conclude by using .
- •
() rule: we simply choose . ∎
Lemma 9** **(Generation for Right Projection)
Assuming that () is the only term rule introducing a right projection, the only non-term rules are (), () and (), and that the axioms of Table 2 are satisfied, we have: if then there exist two families of types and with and, for each , .
Proof.
Similar to the proof of Lemma 8. ∎
We consider the reduction 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 ( ‣ 2.3), if and then .
Proof.
The key case is . If , by Lemma 8, we have two families and with and, for each , . For each , by Lemma 7, we have two families and with and, for each , and . By ( ‣ 2.3), . We conclude by:
∎
Proposition 4** **(Subject Expansion for Products)
If and then .
Proof.
The key case is . We have:
pair
∎
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 ( ‣ 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 ( ‣ 2.2) and ( ‣ 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 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 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 of type constructors (denoted , , , etc) which come with a contravariant arity and a covariant arity . We assume that arities are respected when constructing types, so that if and , then is a type when , and are three types. Moreover, for each constructor , a -value 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 where 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. () is obtained by induction on . (ax) is obtained by induction on using (). () is obtained by induction on the premise.
(co) is obtained by induction on the lexicographically ordered pair (size of , height of the proof of the premise), by looking at each possible last rule of the premise. The key case is ():
we apply () and (ex) to the premise to get and we use the induction hypothesis twice.
(cut) is obtained by induction on the lexicographically ordered triple (size of , 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:
- •
() rule on the right:
[TABLE]
we use the induction hypothesis twice with a decreasing height on the right.
- •
() rule on the left and 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 behaves like an atomic type (i.e. either a type constant or a type variable) if , and defines a top type if :
constr
In particular the types obtained with such [math]-ary constructors such that are all equivalent and we denote them . More generally, controls whether distributes over or not. In the case of a constructor with unary covariant arity, determines whether or not.
Proposition 6** **(Kernel Properties)
If we define as in ISC, the axioms of Table 2 are satisfied.
Proof.
(refl) and (trans) correspond to (ax) and (cut) from Proposition 5. () is an instance of () and for () we have:
ax
Finally, if we have a [math]-ary constructor with , we have just seen it satisfies (). ∎
Lemma 10** **(Inversion)
If , there exists such that:
[TABLE]
Proof.
By induction on the derivation of , 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 , , etc, such that ;
- •
a [math]-ary constructor with ;
- •
a constructor with contravariant arity and covariant arity such that ;
- •
a constructor with contravariant arity [math] and covariant arity such that .
By instantiating the rule of Table 7 to this set of constructors, and using the (wk) rule to simplify the and cases, we obtain the rules of Table 8 where .
Theorem 1** **(Equivalence with BCD)
* in ISC with the (constr) rule instantiated as given in Table 8 if and only if 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: implies . From right to left, the key results are in Propositions 5 and 6. Main cases are:
[TABLE]
∎
Lemma 11** **(Inversion for Arrow)
If is obtained from Tables 4 and 6, we have:
[TABLE]
This is the key property of subtyping allowing for subject -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 , thus if , we get by Proposition 5. By applying Lemma 10, we obtain ,…, , with , so that , and we conclude with Theorem 1. ∎
Lemma 12** **(Inversion for Product)
If 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 on types added to the usual and constructors:
[TABLE]
where each constructor satisfies the following subtyping properties:
[TABLE]
This exactly corresponds, in the ISC setting, to a set of constructors all satisfying , and (the constructors and are obtained as before). For example the associated (constr) rule can be derived in the [BCD*+*18] setting:
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 between constructors (with the same arities) leads to , 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}
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 , we can find some type such that and , but we do not find a way to complete the following derivation:
?
\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 reduces to . The idea of introducing some bottom type with a rule
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.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1]
- 2[ABDC 06] Fabio Alessi, Franco Barbanera & Mariangiola Dezani-Ciancaglini (2006): Intersection types and lambda models . Theoretical Computer Science 355(2), pp. 108–126, 10.1016/j.tcs.2006.01.004 . · doi ↗
- 3[Bak 95] Steffen van Bakel (1995): Intersection Type Assignment Systems . Theoretical Computer Science 151(2), pp. 385–435, 10.1016/0304-3975(95)00073-6 . · doi ↗
- 4[BCD + 18] Jan Bessai, Tzu-Chun Chen, Andrej Dudenhefner, Boris Düdder, Ugo de Liguoro & Jakob Rehof (2018): Mixin Composition Synthesis Based on Intersection Types . Logical Methods in Computer Science 14, p. 37, 10.23638/LMCS-14(1:18)2018 . · doi ↗
- 5[BCDC 83] Henk Barendregt, Mario Coppo & Mariangiola Dezani-Ciancaglini (1983): A Filter Lambda Model and the Completeness of Type Assignment . Journal of Symbolic Logic 48, pp. 931–940, 10.2307/2273659 . · doi ↗
- 6[KP 07] Andrew Kennedy & Benjamin Pierce (2007): On Decidability of Nominal Subtyping with Variance . In: International Workshop on Foundations and Developments of Object-Oriented Languages (FOOL/WOOD ’07) . url: http://foolwood 07.cs.uchicago.edu/program/kennedy.pdf .
- 7[Lau 12] Olivier Laurent (2012): A syntactic introduction to intersection types . Unpublished note. url: %****␣bcdc.bbl␣Line␣75␣****http://perso.ens-lyon.fr/olivier.laurent/tutinter.pdf .
- 8[RDRP 04] Simona Ronchi Della Rocca & Luca Paolini (2004): The Parametric Lambda Calculus . Texts in Theoretical Computer Science, Springer, 10.1007/978-3-662-10394-4 . · doi ↗
