Document Open Access Logo

The Duality of Subtyping

Authors Bruno C. d. S. Oliveira, Cui Shaobo, Baber Rehman

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2020.29.pdf
  • Filesize: 0.69 MB
  • 29 pages

Document Identifiers

Author Details

Bruno C. d. S. Oliveira
  • The University of Hong Kong, China
Cui Shaobo
  • University of California San Diego, CA, USA
Baber Rehman
  • The University of Hong Kong, China

Funding

Funded by Hong Kong Research Grant Council projects number 17210617 and 17209519.

Acknowledgements

We thank the anonymous reviewers for their helpful comments.

Cite AsGet BibTex

Bruno C. d. S. Oliveira, Cui Shaobo, and Baber Rehman. The Duality of Subtyping. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 29:1-29:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ECOOP.2020.29

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.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Object oriented languages
Keywords
  • DuoTyping
  • OOP
  • Duality
  • Subtyping
  • Supertyping

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Andreas Abel and Dulma Rodriguez. Syntactic metatheory of higher-order subtyping. In International Workshop on Computer Science Logic, pages 446-460. Springer, 2008. Google Scholar
  2. Robin Adams. Pure type systems with judgemental equality. Journal of Functional Programming, 16(2):219-246, 2006. Google Scholar
  3. Nada Amin, Adriaan Moors, and Martin Odersky. Dependent object types. In 19th International Workshop on Foundations of Object-Oriented Languages, 2012. Google Scholar
  4. Nada Amin and Tiark Rompf. Type soundness proofs with definitional interpreters. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, 2017. Google Scholar
  5. Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth through Proof. Academic Press, Inc., 1986. Google Scholar
  6. Franco Barbanera, Mariangiola Dezaniciancaglini, and Ugo Deliguoro. Intersection and union types: syntax and semantics. Information and Computation, 119(2):202-230, 1995. Google Scholar
  7. Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment 1. The journal of symbolic logic, 48(4):931-940, 1983. Google Scholar
  8. Bruno Barras, Samuel Boutin, Cristina Cornes, Judicael Courant, Jean-Christophe Filliatre, Eduardo Gimenez, Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, et al. The coq proof assistant reference manual: Version 6.1, 1997. Google Scholar
  9. Jon Barwise and Robin Cooper. Generalized quantifiers and natural language. In Philosophy, language, and artificial intelligence, pages 241-301. Springer, 1981. Google Scholar
  10. Giovanni Bernardi, Ornela Dardha, Simon J Gay, and Dimitrios Kouzapas. On duality relations for session types. In International Symposium on Trustworthy Global Computing, pages 51-66. Springer, 2014. Google Scholar
  11. Jan Bessai, Boris Düdder, Andrej Dudenhefner, Tzu-Chun Chen, and Ugo de'Liguoro. Typing classes and mixins with intersection types. arXiv preprint, 2015. URL: http://arxiv.org/abs/1503.04911.
  12. Gavin Bierman, Martín Abadi, and Mads Torgersen. Understanding typescript. In European Conference on Object-Oriented Programming, pages 257-281. Springer, 2014. Google Scholar
  13. David Binder, Julian Jabs, Ingo Skupin, and Klaus Ostermann. Decomposition diversity with symmetric data and codata. Proceedings of the ACM on Programming Languages, 4(POPL):30, 2019. Google Scholar
  14. Richard Bird and Oege de Moor. The Algebra of Programming. Prentice-Hall, 1996. URL: http://www.cs.ox.ac.uk/publications/books/algebra/.
  15. Peter Canning, William Cook, Walter Hill, Walter Olthoff, and John C Mitchell. F-bounded polymorphism for object-oriented programming. In FPCA, volume 89, pages 273-280, 1989. Google Scholar
  16. Luca Cardelli, Simone Martini, John C Mitchell, and Andre Scedrov. An extension of system f with subtyping. Information and Computation, 109(1-2):4-56, 1994. Google Scholar
  17. Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism. ACM Computing Surveys (CSUR), 17(4):471-523, 1985. Google Scholar
  18. Arthur Charguéraud. The locally nameless representation. Journal of Automated Reasoning, 2011. Google Scholar
  19. Avik Chaudhuri. Flow: a static type checker for javascript. SPLASH-I In Systems, Programming, Languages and Applications: Software for Humanity, 2015. Google Scholar
  20. Oliver Danvy and Andrzej Filinski. Representing control: A study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361-391, December 1992. Google Scholar
  21. Kosta Došen. Logical constants as punctuation marks. Notre Dame J. Formal Logic, 30(3):362-381, June 1989. URL: https://doi.org/10.1305/ndjfl/1093635154.
  22. Joshua Dunfield. Elaborating intersection and union types. Journal of Functional Programming, 24(2-3):133-165, 2014. Google Scholar
  23. Joshua Dunfield and Neel Krishnaswami. Bidirectional typing. arXiv preprint, 2019. URL: http://arxiv.org/abs/1908.05839.
  24. Joshua Dunfield and Neelakantan R. Krishnaswami. Complete and easy bidirectional typechecking for higher-rank polymorphism. In ICFP, 2013. Google Scholar
  25. Gerhard Gentzen. Untersuchungen über das logische Schliessen. Mathematische Zeitschrift, 39:176-210, 405-431, 1934. Google Scholar
  26. DeLesley S. Hutchins. Pure subtype systems. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, 2010. Google Scholar
  27. Atsushi Igarashi and Mirko Viroli. On variance-based subtyping for parametric types. In ecoop, pages 441-469, Malaga, Spain, June 2002. sv. To appear in ACM Transactions on Programming Languages and Systems. Google Scholar
  28. LSV Jutting. Typing in pure type systems. Information and Computation, 105(1):30-41, 1993. Google Scholar
  29. Gavin King. The ceylon language specification, version 1.0, 2013. Google Scholar
  30. Saunders Mac Lane. Categories for the Working Mathematician. Number 5 in Graduate Texts in Mathematics. Springer, 2 edition, 1998. Google Scholar
  31. James McKinna and Robert Pollack. Pure type systems formalized. In International Conference on Typed Lambda Calculi and Applications, pages 289-305. Springer, 1993. Google Scholar
  32. Fabian Muehlboeck and Ross Tate. Empowering union and intersection types with integrated subtyping. Proceedings of the ACM on Programming Languages, 2(OOPSLA):112, 2018. Google Scholar
  33. Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. ACM Transactions on Computational Logic (TOCL), 9(3):23, 2008. Google Scholar
  34. Martin Odersky, Philippe Altherr, Vincent Cremet, Burak Emir, Sebastian Maneth, Stéphane Micheloud, Nikolay Mihaylov, Michel Schinz, Erik Stenman, and Matthias Zenger. An overview of the scala programming language, 2004. Google Scholar
  35. Klaus Ostermann and Julian Jabs. Dualizing generalized algebraic data types by matrix transposition. In European Symposium on Programming, pages 60-85. Springer, 2018. Google Scholar
  36. Benjamin C Pierce. Programming with intersection types, union types, and polymorphism, 2002. Google Scholar
  37. Benjamin C. Pierce and David N. Turner. Local type inference. ACM Trans. Program. Lang. Syst., 22(1), 2000. Google Scholar
  38. Dag Prawitz. Proofs and the meaning and completeness of the logical constants. In Essays on Mathematical and Philosophical Logic. Synthese Library (Studies in Epistemology, Logic, Methodology, and Philosophy of Science), 1979. Google Scholar
  39. John C Reynolds. Preliminary design of the programming language forsythe, 1988. Google Scholar
  40. Tiark Rompf and Nada Amin. Type soundness for dependent object types (dot). In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, 2016. Google Scholar
  41. Paula Severi and Erik Poll. Pure type systems with definitions. In International Symposium on Logical Foundations of Computer Science, pages 316-328. Springer, 1994. Google Scholar
  42. Alex K Simpson. The proof theory and semantics of intuitionistic modal logic, 1994. Google Scholar
  43. Martin Steffen and Benjamin Pierce. Higher-order subtyping, 1994. Google Scholar
  44. Tarmo Uustalu and Varmo Vene. Comonadic notions of computation. Electronic Notes in Theoretical Computer Science, 203(5):263-284, 2008. Google Scholar
  45. LS van Benthem Jutting, James McKinna, and Robert Pollack. Checking algorithms for pure type systems. In International Workshop on Types for Proofs and Programs, pages 19-61. Springer, 1993. Google Scholar
  46. Yanpeng Yang and Bruno C. d. S. Oliveira. Unifying typing and subtyping. Proceedings of the ACM on Programming Languages, 1(OOPSLA):47, 2017. Google Scholar
  47. Francesco Zappa Nardelli, Julia Belyakova, Artem Pelenitsyn, Benjamin Chung, Jeff Bezanson, and Jan Vitek. Julia subtyping: a rational reconstruction. Proceedings of the ACM on Programming Languages, 2(OOPSLA):113, 2018. Google Scholar
  48. Jan Zwanenburg. Pure type systems with subtyping. In International Conference on Typed Lambda Calculi and Applications, pages 381-396. Springer, 1999. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact