License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2018.22
URN: urn:nbn:de:0030-drops-92275
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9227/
Go to the corresponding LIPIcs Volume Portal

Bi, Xuan ; Oliveira, Bruno C. d. S. ; Schrijvers, Tom

The Essence of Nested Composition

pdf-format:
LIPIcs-ECOOP-2018-22.pdf (0.7 MB)

Abstract

Calculi with disjoint intersection types support an introduction form for intersections called the merge operator, while retaining a coherent semantics. Disjoint intersections types have great potential to serve as a foundation for powerful, flexible and yet type-safe and easy to reason OO languages. This paper shows how to significantly increase the expressive power of disjoint intersection types by adding support for nested subtyping and composition, which enables simple forms of family polymorphism to be expressed in the calculus. The extension with nested subtyping and composition is challenging, for two different reasons. Firstly, the subtyping relation that supports these features is non-trivial, especially when it comes to obtaining an algorithmic version. Secondly, the syntactic method used to prove coherence for previous calculi with disjoint intersection types is too inflexible, making it hard to extend those calculi with new features (such as nested subtyping). We show how to address the first problem by adapting and extending the Barendregt, Coppo and Dezani (BCD) subtyping rules for intersections with records and coercions. A sound and complete algorithmic system is obtained by using an approach inspired by Pierce's work. To address the second problem we replace the syntactic method to prove coherence, by a semantic proof method based on logical relations. Our work has been fully formalized in Coq, and we have an implementation of our calculus.

BibTeX - Entry

@InProceedings{bi_et_al:LIPIcs:2018:9227,
  author =	{Xuan Bi and Bruno C. d. S. Oliveira and Tom Schrijvers},
  title =	{{The Essence of Nested Composition}},
  booktitle =	{32nd European Conference on Object-Oriented Programming  (ECOOP 2018)},
  pages =	{22:1--22:33},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-079-8},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{109},
  editor =	{Todd Millstein},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9227},
  URN =		{urn:nbn:de:0030-drops-92275},
  doi =		{10.4230/LIPIcs.ECOOP.2018.22},
  annote =	{Keywords: nested composition, family polymorphism, intersection types, coherence}
}

Keywords: nested composition, family polymorphism, intersection types, coherence
Collection: 32nd European Conference on Object-Oriented Programming (ECOOP 2018)
Issue Date: 2018
Date of publication: 10.07.2018
Supplementary Material: ECOOP Artifact Evaluation approved artifact available at http://dx.doi.org/10.4230/DARTS.4.3.5

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI