Document Open Access Logo

The Essence of Nested Composition

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

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2018.22.pdf
  • Filesize: 0.65 MB
  • 33 pages

Document Identifiers

Author Details

Xuan Bi
  • The University of Hong Kong, Hong Kong, China
Bruno C. d. S. Oliveira
  • The University of Hong Kong, Hong Kong, China
Tom Schrijvers
  • KU Leuven, Belgium

Funding

  • Oliveira, Bruno C. d. S.: Funded by Hong Kong Research Grant Council projects number 17210617 and 17258816
  • Schrijvers, Tom: Funded by The Research Foundation - Flanders

Cite As Get BibTex

Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. The Essence of Nested Composition. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 22:1-22:33, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.ECOOP.2018.22

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.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Object oriented languages
Keywords
  • nested composition
  • family polymorphism
  • intersection types
  • coherence

Metrics

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

Supplementary Materials

References

  1. Amal Jamil Ahmed. Semantics of types for mutable state. PhD thesis, Princeton University, 2004. Google Scholar
  2. João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi. Disjoint polymorphism. In European Symposium on Programming, 2017. Google Scholar
  3. Nada Amin, Adriaan Moors, and Martin Odersky. Dependent object types. In Workshop on Foundations of Object-Oriented Languages, 2012. Google Scholar
  4. Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. The journal of symbolic logic, 48(04):931-940, 1983. Google Scholar
  5. Jan Bessai, Boris Düdder, Andrej Dudenhefner, Tzu-Chun Chen, and Ugo de'Liguoro. Typing classes and mixins with intersection types. In Workshop on Intersection Types and Related Systems (ITRS), 2014. Google Scholar
  6. Jan Bessai, Andrej Dudenhefner, Boris Düdder, and Jakob Rehof. Extracting a formally verified subtyping algorithm for intersection types from ideals and filters. In TYPES, 2016. Google Scholar
  7. Xuan Bi and Bruno C. d. S. Oliveira. Typed first-class traits. In European Conference on Object-Oriented Programming, 2018. Google Scholar
  8. Dariusz Biernacki and Piotr Polesiuk. Logical relations for coherence of effect subtyping. In LIPIcs, 2015. Google Scholar
  9. Gilad Bracha and William R. Cook. Mixin-based inheritance. In International Conference on Object-Oriented Programming, Systems, Languages, and Applications, 1990. Google Scholar
  10. Val Breazu-Tannen, Thierry Coquand, Carl A. Gunter, and Andre Scedrov. Inheritance as implicit coercion. Information and Computation, 93(1):172-221, 1991. Google Scholar
  11. Kim Bruce, Luca Cardelli, Giuseppe Castagna, Gary T Leavens, Benjamin Pierce, et al. On binary methods. In Theory and Practice of Object Systems, 1996. Google Scholar
  12. Kim B. Bruce, Angela Schuett, and Robert van Gent. Polytoil: A type-safe polymorphic object-oriented language. In European Conference on Object-Oriented Programming, 1995. Google Scholar
  13. Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism. ACM Computing Surveys, 17(4):471-523, 1985. Google Scholar
  14. Jacques Carette, Oleg Kiselyov, and Chung-Chieh Shan. Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. Journal of Functional Programming, 19(05):509, 2009. Google Scholar
  15. Giuseppe Castagna, Giorgio Ghelli, and Giuseppe Longo. A calculus for overloaded functions with subtyping. In LFP, 1992. Google Scholar
  16. David Clarke, Sophia Drossopoulou, James Noble, and Tobias Wrigstad. Tribe: More Types for Virtual Classes. In AOSD, 2007. Google Scholar
  17. Adriana B Compagnoni and Benjamin C Pierce. Higher-order intersection types and multiple inheritance. MSCS, 6(5):469-501, 1996. Google Scholar
  18. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Functional characters of solvable terms. Mathematical Logic Quarterly, 1981. Google Scholar
  19. Andrea Corradi, Marco Servetto, and Elena Zucca. DeepFJig emdash modular composition of nested classes. The Journal of Object Technology, 11(2):1:1, 2012. Google Scholar
  20. Pierre-Louis Curien and Giorgio Ghelli. Coherence of subsumption, minimum typing and type-checking in f ≤. MSCS, 2(01):55, 1992. Google Scholar
  21. Rowan Davies and Frank Pfenning. Intersection types and computational effects. In International Conference on Functional Programming, 2000. Google Scholar
  22. Stéphane Ducasse, Oscar Nierstrasz, Nathanael Schärli, Roel Wuyts, and Andrew P Black. Traits: A mechanism for fine-grained reuse. ACM Transactions on Programming Languages and Systems (TOPLAS), 28(2):331-388, 2006. Google Scholar
  23. Joshua Dunfield. Elaborating intersection and union types. Journal of Functional Programming, 24:133-165, 2014. Google Scholar
  24. Joshua Dunfield and Frank Pfenning. Type assignment for intersections and unions in call-by-value languages. In Foundations of Software Science and Computation Structure (FoSSaCS), 2003. Google Scholar
  25. Erik Ernst. Family polymorphism. In European Conference on Object-Oriented Programming, 2001. Google Scholar
  26. Erik Ernst. Higher-order hierarchies. In European Conference on Object-Oriented Programming, 2003. Google Scholar
  27. Erik Ernst, Klaus Ostermann, and William R. Cook. A virtual class calculus. In Symposium on Principles of Programming Languages, 2006. Google Scholar
  28. Facebook. Flow. https://flow.org/, 2014.
  29. Kathleen Fisher and John Reppy. A typed calculus of traits. In Workshop on Foundations of Object-Oriented Languages, 2004. Google Scholar
  30. Tim Freeman and Frank Pfenning. Refinement types for ML. In Conference on Programming Language Design and Implementation, 1991. Google Scholar
  31. Robert Harper. Practical Foundations for Programming Languages. Cambridge University Press, 2016. Google Scholar
  32. Fritz Henglein. Dynamic typing: syntax and proof theory. Science of Computer Programming, 22(3):197-230, jun 1994. Google Scholar
  33. David Herman, Aaron Tomb, and Cormac Flanagan. Space-efficient gradual typing. Higher-Order and Symbolic Computation, 23(2):167, 2010. Google Scholar
  34. Paul Jolly, Sophia Drossopoulou, Christopher Anderson, and Klaus Ostermann. Simple dependent types: Concord. In European Conference on Object-Oriented Programming Workshop on Formal Techniques for Java Programs (FTfJP), 2004. Google Scholar
  35. Toshihiko Kurata and Masako Takahashi. Decidable properties of intersection type systems. Typed Lambda Calculi and Applications, pages 297-311, 1995. Google Scholar
  36. Olivier Laurent. Intersection types with subtyping by means of cut elimination. Fundamenta Informaticae, 121(1-4):203-226, 2012. Google Scholar
  37. Olivier Laurent. A syntactic introduction to intersection types. Unpublished note, 2012. Google Scholar
  38. O. L. Madsen and B. Moller-Pedersen. Virtual classes: a powerful mechanism in object-oriented programming. In International Conference on Object-Oriented Programming, Systems, Languages, and Applications, 1989. Google Scholar
  39. Microsoft. Typescript. https://www.typescriptlang.org/, 2012.
  40. Eugenio Moggi. Notions of computation and monads. Information and Computation, 93(1):55-92, 1991. Google Scholar
  41. James Hiram Morris Jr. Lambda-calculus models of programming languages. PhD thesis, Massachusetts Institute of Technology, 1969. Google Scholar
  42. Nathaniel Nystrom, Stephen Chong, and Andrew C. Myers. Scalable extensibility via nested inheritance. In International Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2004. Google Scholar
  43. Nathaniel Nystrom, Xin Qi, and Andrew C. Myers. J&: Nested Intersection for Scalable Software Composition. In International Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2006. Google Scholar
  44. 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. Technical report, EPFL, 2004. Google Scholar
  45. Bruno C. d. S. Oliveira and William R. Cook. Extensibility for the masses. In European Conference on Object-Oriented Programming, 2012. Google Scholar
  46. Bruno C. d. S. Oliveira, Zhiyuan Shi, and João Alpuim. Disjoint intersection types. In International Conference on Functional Programming, 2016. Google Scholar
  47. Benjamin C Pierce. A decision procedure for the subtype relation on intersection types with bounded variables. Technical report, Carnegie Mellon University, 1989. Google Scholar
  48. Gordon Plotkin. Lambda-definability and logical relations. Edinburgh University, 1973. Google Scholar
  49. Garrel Pottinger. A type assignment for the strongly normalizable λ-terms. To HB Curry: essays on combinatory logic, lambda calculus and formalism, 1980. Google Scholar
  50. Xin Qi and Andrew C. Myers. Sharing classes between families. In Conference on Programming Language Design and Implementation, 2009. Google Scholar
  51. Redhat. Ceylon. https://ceylon-lang.org/, 2011.
  52. Jakob Rehof and Paweł Urzyczyn. Finite combinatory logic with intersection types. In International Conference on Typed Lambda Calculi and Applications, 2011. Google Scholar
  53. John C. Reynolds. Types, abstraction and parametric polymorphism. In IFIP, 1983. Google Scholar
  54. John C Reynolds. Preliminary design of the programming language forsythe. Technical report, Carnegie Mellon University, 1988. Google Scholar
  55. John C. Reynolds. The coherence of languages with intersection types. In Lecture Notes in Computer Science (LNCS), pages 675-700. Springer Berlin Heidelberg, 1991. Google Scholar
  56. Chieri Saito and Atsushi Igarashi. Matching ThisType to subtyping. In Symposium on Applied Computing (SAC), 2009. Google Scholar
  57. Chieri Saito, Atsushi Igarashi, and Mirko Viroli. Lightweight family polymorphism. Journal of Functional Programming, 18(03), 2007. Google Scholar
  58. Nathanael Schärli, Stéphane Ducasse, Oscar Nierstrasz, and Andrew P Black. Traits: Composable units of behaviour. In European Conference on Object-Oriented Programming, 2003. Google Scholar
  59. Jan Schwinghammer. Coherence of subsumption for monadic types. Journal of Functional Programming, 19(02):157, 2008. Google Scholar
  60. Jeremy Siek, Peter Thiemann, and Philip Wadler. Blame and coercion: together again for the first time. In Conference on Programming Language Design and Implementation, 2015. Google Scholar
  61. Richard Statman. Logical relations and the typed λ-calculus. Information and Control, 65(2-3):85-97, 1985. Google Scholar
  62. Rick Statman. A finite model property for intersection types. Electronic Proceedings in Theoretical Computer Science, 177:1-9, 2015. Google Scholar
  63. W. W. Tait. Intensional interpretations of functionals of finite type i. The Journal of symbolic logic, 32(2):198-212, 1967. Google Scholar
  64. Philip Wadler. The expression problem. Java-genericity mailing list, 1998. Google Scholar
  65. Yanlin Wang and Bruno C d S Oliveira. The expression problem, trivially! In Proceedings of the 15th International Conference on Modularity, 2016. Google Scholar
  66. Yizhou Zhang and Andrew C. Myers. Familia: unifying interfaces, type classes, and family polymorphism. In International Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2017. 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 About DROPS Imprint Privacy Contact