File Download
Links for fulltext
(May Require Subscription)
- Publisher Website: 10.4230/LIPIcs.ECOOP.2020.29
- Scopus: eid_2-s2.0-85113351130
- Find via
Supplementary
-
Citations:
- Scopus: 0
- Appears in Collections:
Conference Paper: The Duality of Subtyping
Title | The Duality of Subtyping |
---|---|
Authors | |
Keywords | DuoTyping OOP Duality Subtyping Supertyping |
Issue Date | 2020 |
Publisher | Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH. The Journal's web site is located at hhttp://www.dagstuhl.de/publikationen/lipics/ |
Citation | The 34th European Conference on Object-Oriented Programming (ECOOP 2020), Virtual Conference, Berlin, Germany, 15-17 November 2020. In Hirschfeld, R & Pape, T (Eds.). LIPICS - Leibniz International Proceedings in Informatics, 2020, v. 166, article no. 29, p. 29:1-29:29 How to Cite? |
Abstract | Subtyping is a concept frequently encountered in many programming languages and calculi. Various forms of subtyping exist for different type system features, including intersection types, union types or bounded quantification. Normally these features are designed independently of each other, without exploiting obvious similarities (or dualities) between features. This paper proposes a novel methodology for designing subtyping relations that exploits duality between features. At the core of our methodology is a generalization of subtyping relations, which we call Duotyping. Duotyping is parameterized by the mode of the relation. One of these modes is the usual subtyping, while another mode is supertyping (the dual of subtyping). Using the mode it is possible to generalize the usual rules of subtyping to account not only for the intended behaviour of one particular language construct, but also of its dual. Duotyping brings multiple benefits, including: shorter specifications and implementations, dual features that come essentially for free, as well as new proof techniques for various properties of subtyping. To evaluate a design based on Duotyping against traditional designs, we formalized various calculi with common OOP features (including union types, intersection types and bounded quantification) in Coq in both styles. Our results show that the metatheory when using Duotyping does not come at a significant cost: the metatheory with Duotyping has similar complexity and size compared to the metatheory for traditional designs. However, we discover new features as duals to well-known features. Furthermore, we also show that Duotyping can significantly simplify transitivity proofs for many of the calculi studied by us. |
Persistent Identifier | http://hdl.handle.net/10722/301310 |
ISSN | 2023 SCImago Journal Rankings: 0.796 |
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Dos Santos Oliveira, BC | - |
dc.contributor.author | Cui, S | - |
dc.contributor.author | Rehman, B | - |
dc.date.accessioned | 2021-07-27T08:09:14Z | - |
dc.date.available | 2021-07-27T08:09:14Z | - |
dc.date.issued | 2020 | - |
dc.identifier.citation | The 34th European Conference on Object-Oriented Programming (ECOOP 2020), Virtual Conference, Berlin, Germany, 15-17 November 2020. In Hirschfeld, R & Pape, T (Eds.). LIPICS - Leibniz International Proceedings in Informatics, 2020, v. 166, article no. 29, p. 29:1-29:29 | - |
dc.identifier.issn | 1868-8969 | - |
dc.identifier.uri | http://hdl.handle.net/10722/301310 | - |
dc.description.abstract | Subtyping is a concept frequently encountered in many programming languages and calculi. Various forms of subtyping exist for different type system features, including intersection types, union types or bounded quantification. Normally these features are designed independently of each other, without exploiting obvious similarities (or dualities) between features. This paper proposes a novel methodology for designing subtyping relations that exploits duality between features. At the core of our methodology is a generalization of subtyping relations, which we call Duotyping. Duotyping is parameterized by the mode of the relation. One of these modes is the usual subtyping, while another mode is supertyping (the dual of subtyping). Using the mode it is possible to generalize the usual rules of subtyping to account not only for the intended behaviour of one particular language construct, but also of its dual. Duotyping brings multiple benefits, including: shorter specifications and implementations, dual features that come essentially for free, as well as new proof techniques for various properties of subtyping. To evaluate a design based on Duotyping against traditional designs, we formalized various calculi with common OOP features (including union types, intersection types and bounded quantification) in Coq in both styles. Our results show that the metatheory when using Duotyping does not come at a significant cost: the metatheory with Duotyping has similar complexity and size compared to the metatheory for traditional designs. However, we discover new features as duals to well-known features. Furthermore, we also show that Duotyping can significantly simplify transitivity proofs for many of the calculi studied by us. | - |
dc.language | eng | - |
dc.publisher | Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH. The Journal's web site is located at hhttp://www.dagstuhl.de/publikationen/lipics/ | - |
dc.relation.ispartof | LIPICS - Leibniz International Proceedings in Informatics | - |
dc.relation.ispartof | The 34th European Conference on Object-Oriented Programming (ECOOP 2020 | - |
dc.rights | This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License. | - |
dc.subject | DuoTyping | - |
dc.subject | OOP | - |
dc.subject | Duality | - |
dc.subject | Subtyping | - |
dc.subject | Supertyping | - |
dc.title | The Duality of Subtyping | - |
dc.type | Conference_Paper | - |
dc.identifier.email | Dos Santos Oliveira, BC: bruno@cs.hku.hk | - |
dc.identifier.authority | Dos Santos Oliveira, BC=rp01786 | - |
dc.description.nature | published_or_final_version | - |
dc.identifier.doi | 10.4230/LIPIcs.ECOOP.2020.29 | - |
dc.identifier.scopus | eid_2-s2.0-85113351130 | - |
dc.identifier.hkuros | 323737 | - |
dc.identifier.volume | 166 | - |
dc.identifier.spage | 29:1 | - |
dc.identifier.epage | 29:29 | - |
dc.publisher.place | Germany | - |