Document Open Access Logo

Row and Bounded Polymorphism via Disjoint Polymorphism

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

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2020.27.pdf
  • Filesize: 0.68 MB
  • 30 pages

Document Identifiers

Author Details

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

Funding

This work has been sponsored by Hong Kong Research Grant Council projects number 17210617 and 17209519, and by the Research Foundation - Flanders.

Acknowledgements

We thank the anonymous reviewers for their helpful comments.

Cite AsGet BibTex

Ningning Xie, Bruno C. d. S. Oliveira, Xuan Bi, and Tom Schrijvers. Row and Bounded Polymorphism via Disjoint Polymorphism. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 27:1-27:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ECOOP.2020.27

Abstract

Polymorphism and subtyping are important features in mainstream OO languages. The most common way to integrate the two is via 𝖥_{< :} style bounded quantification. A closely related mechanism is row polymorphism, which provides an alternative to subtyping, while still enabling many of the same applications. Yet another approach is to have type systems with intersection types and polymorphism. A recent addition to this design space are calculi with disjoint intersection types and disjoint polymorphism. With all these alternatives it is natural to wonder how they are related. This paper provides an answer to this question. We show that disjoint polymorphism can recover forms of both row polymorphism and bounded polymorphism, while retaining key desirable properties, such as type-safety and decidability. Furthermore, we identify the extra power of disjoint polymorphism which enables additional features that cannot be easily encoded in calculi with row polymorphism or bounded quantification alone. Ultimately we expect that our work is useful to inform language designers about the expressive power of those common features, and to simplify implementations and metatheory of feature-rich languages with polymorphism and subtyping.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Software and its engineering → Object oriented languages
  • Software and its engineering → Polymorphism
Keywords
  • Intersection types
  • bounded polymorphism
  • row polymorphism

Metrics

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

Supplementary Materials

References

  1. Amal Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In European Symposium on Programming (ESOP), 2006. Google Scholar
  2. João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi. Disjoint polymorphism. In European Symposium on Programming (ESOP), 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. Bernard Berthomieu and Camille Le Monies De Sagazan. A calculus of tagged types, with applications to process languages. Types for Program Analysis, page 1, 1995. Google Scholar
  6. Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. The essence of nested composition. In European Conference on Object-Oriented Programming (ECOOP), 2018. Google Scholar
  7. Xuan Bi, Ningning Xie, Bruno C. d. S. Oliveira, and Tom Schrijvers. Distributive disjoint polymorphism for compositional programming. In European Symposium on Programming (ESOP), 2019. Google Scholar
  8. Gilad Bracha. The programming language jigsaw: mixins, modularity and multiple inheritance. PhD thesis, Dept. of Computer Science, University of Utah, 1992. Google Scholar
  9. 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
  10. Luca Cardelli. Extensible records in a pure calculus of subtyping. Digital. Systems Research Center, 1992. Google Scholar
  11. Luca Cardelli and John C Mitchell. Operations on records. In International Conference on Mathematical Foundations of Programming Semantics, 1989. Google Scholar
  12. Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism. ACM Computing Surveys, 17(4):471-523, 1985. Google Scholar
  13. Felice Cardone. Relational semantics for recursive types and bounded quantification. In International Colloquium on Automata, Languages, and Programming, pages 164-178. Springer, 1989. Google Scholar
  14. Giuseppe Castagna, Giorgio Ghelli, and Giuseppe Longo. A calculus for overloaded functions with subtyping. In Conference on LISP and Functional Programming, 1992. Google Scholar
  15. Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, and Pietro Abate. Polymorphic functions with set-theoretic types: part 2: local type inference and type reconstruction. In Principles of Programming Languages (POPL), 2015. Google Scholar
  16. Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, Hyeonseung Im, Sergueï Lenglet, and Luca Padovani. Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation. In Principles of Programming Languages (POPL), 2014. Google Scholar
  17. Giuseppe Castagna, Tommaso Petrucciani, and Kim Nguyen. Set-theoretic types for polymorphic variants. In International Conference on Functional Programming (ICFP), 2016. Google Scholar
  18. Giuseppe Castagna and Benjamin C Pierce. Decidable bounded quantification. In Principles of Programming Languages (POPL), 1994. Google Scholar
  19. Giuseppe Castagna and Zhiwu Xu. Set-theoretic foundation of parametric polymorphism and subtyping. In International Conference on Functional Programming (ICFP), 2011. Google Scholar
  20. C. Chambers, D. Ungar, B.W. Chang, and U. Hölzle. Parents are shared parts of objects: Inheritance and encapsulation in SELF. Lisp and Symbolic Computation, 4(3):207-222, 1991. Google Scholar
  21. Adriana B Compagnoni and Benjamin C Pierce. Higher-order intersection types and multiple inheritance. Mathematical Structures in Computer Science (MSCS), 6(5):469-501, 1996. Google Scholar
  22. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Patrick Sallé. Functional characterization of some semantic equalities inside λ-calculus. In International Colloquium on Automata, Languages, and Programming, pages 133-146. Springer, 1979. Google Scholar
  23. Pierre-Louis Curien and Giorgio Ghelli. Coherence of subsumption, minimum typing and type-checking in f≤. Mathematical structures in computer science, 2(1):55-91, 1992. Google Scholar
  24. Rowan Davies. Practical refinement-type checking. PhD thesis, School of Computer Science, Carnegie Mellon University, 2005. Google Scholar
  25. Mariangiola Dezani-Ciancaglini, Elena Giachino, Sophia Drossopoulou, and Nobuko Yoshida. Bounded session types for object oriented languages. In Formal Methods for Components and Objects, pages 207-245. Springer, 2007. Google Scholar
  26. Stephen Dolan and Alan Mycroft. Polymorphism, subtyping, and type inference in mlsub. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pages 60-72, New York, NY, USA, 2017. ACM. URL: https://doi.org/10.1145/3009837.3009882.
  27. Joshua Dunfield. Refined typechecking with stardust. In PLPV, 2007. Google Scholar
  28. Joshua Dunfield. Elaborating intersection and union types. Journal of Functional Programming (JFP), 24(2-3):133-165, 2014. Google Scholar
  29. Erik Ernst. Family polymorphism. In European Conference on Object-Oriented Programming (ECOOP), 2001. Google Scholar
  30. Erik Ernst. The expression problem, scandinavian style. On Mechanisms For Specialization, page 27, 2004. Google Scholar
  31. Facebook. Flow. https://flow.org/, 2014.
  32. Matthew Flatt, Robert Bruce Findler, and Matthias Felleisen. Scheme with classes, mixins, and traits. In Programming Languages and Systems (APLAS), 2006. Google Scholar
  33. Simon J Gay. Bounded polymorphism in session types. Mathematical Structures in Computer Science, 18(5):895-930, 2008. Google Scholar
  34. Robert Harper and Benjamin Pierce. A record calculus based on symmetric concatenation. In Principles of Programming Languages (POPL), 1991. Google Scholar
  35. Daan Leijen. Extensible records with scoped labels. Trends in Functional Programming, 5:297-312, 2005. Google Scholar
  36. Daan Leijen. Type directed compilation of row-typed algebraic effects. In Principles of Programming Languages (POPL), 2017. Google Scholar
  37. Sam Lindley and James Cheney. Row-based effect types for database integration. In Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation, pages 91-102. ACM, 2012. Google Scholar
  38. Sam Lindley and J Garrett Morris. Lightweight functional session types. Behavioural Types: from Theory to Tools. River Publishers, pages 265-286, 2017. Google Scholar
  39. Simon Martini. Bounded quantifiers have interval models. In Proceedings of the 1988 ACM conference on LISP and functional programming, pages 164-173. ACM, 1988. Google Scholar
  40. Microsoft. Typescript. https://www.typescriptlang.org/, 2012.
  41. Microsoft. https://www.typescriptlang.org/docs/handbook/advanced-types.html, 2019. Online; accessed 16 June 2019.
  42. J. Garrett Morris and James McKinna. Abstracting extensible data types: or, rows by any other name. In Principles of Programming Languages (POPL), 2019. Google Scholar
  43. Fabian Muehlboeck and Ross Tate. Empowering union and intersection types with integrated subtyping. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2018. 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. Martin Odersky and Konstantin Läufer. Putting type annotations to work. In Symposium on Principles of Programming Languages (POPL), 1996. Google Scholar
  46. Bruno C. d. S. Oliveira, Zhiyuan Shi, and João Alpuim. Disjoint intersection types. In International Conference on Functional Programming (ICFP), 2016. Google Scholar
  47. Bruno C. d. S. Oliveira, Tijs Van Der Storm, Alex Loh, and William R Cook. Feature-oriented programming with object algebras. In European Conference on Object-Oriented Programming (ECOOP), 2013. Google Scholar
  48. Benjamin C Pierce. Programming with intersection types and bounded polymorphism. PhD thesis, University of Pennsylvania, 1991. Google Scholar
  49. Benjamin C Pierce. Bounded quantification is undecidable. Information and Computation, 112(1):131-165, 1994. Google Scholar
  50. Benjamin C Pierce and David N Turner. Local type argument synthesis with bounded quantification. Technical report, Technical Report 495, Computer Science Department, Indiana University, 1997. Google Scholar
  51. Garrel Pottinger. A type assignment for the strongly normalizable λ-terms. To HB Curry: essays on combinatory logic, lambda calculus and formalism, pages 561-577, 1980. Google Scholar
  52. Redhat. Ceylon. https://ceylon-lang.org/, 2011.
  53. Didier Rémy. Type inference for records in a natural extension of ML. Theoretical Aspects Of Object-Oriented Programming. Types, Semantics and …, 1993. Google Scholar
  54. Tillmann Rendel, Jonathan Immanuel Brachthäuser, and Klaus Ostermann. From object algebras to attribute grammars. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA ’14, page 377–395, New York, NY, USA, 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2660193.2660237.
  55. John C Reynolds. Preliminary design of the programming language forsythe. Technical report, Carnegie Mellon University, 1988. Google Scholar
  56. 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
  57. John C Reynolds. Design of the programming language forsythe. In ALGOL-like languages, pages 173-233. Birkhauser Boston Inc., 1997. Google Scholar
  58. Tiark Rompf and Nada Amin. Type soundness for dependent object types (DOT). In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2016. Google Scholar
  59. Patrick Salle. Une extension de la theorie des types en lambda-calcul. In Proceedings of the Fifth Colloquium on Automata, Languages and Programming, pages 398-410, London, UK, UK, 1978. Springer-Verlag. Google Scholar
  60. Mark Shields and Erik Meijer. Type-indexed rows. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '01, pages 261-275, New York, NY, USA, 2001. ACM. URL: https://doi.org/10.1145/360204.360230.
  61. Asumu Takikawa, T. Stephen Strickland, Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. Gradual typing for first-class classes. In Object-oriented Programming: Systems, Languages and Applications (OOPSLA), 2012. Google Scholar
  62. Philip Wadler. The expression problem. Java-genericity mailing list, 1998. Google Scholar
  63. Mitchell Wand. Complete type inference for simple objects. In Symposium on Logic in Computer Science (LICS), 1987. Google Scholar
  64. Mitchell Wand. Type inference for record concatenation and multiple inheritance. In Symposium on Logic in Computer Science (LICS), 1989. Google Scholar
  65. Mathhias Zenger and Martin Odersky. Independently extensible solutions to the expression problem. In Foundations of Object-Oriented Languages, 2005. 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