Document Open Access Logo

Union Types with Disjoint Switches

Authors Baber Rehman , Xuejing Huang , Ningning Xie, Bruno C. d. S. Oliveira

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2022.25.pdf
  • Filesize: 1.06 MB
  • 31 pages

Document Identifiers

Author Details

Baber Rehman
  • The University of Hong Kong, China
Xuejing Huang
  • The University of Hong Kong, China
Ningning Xie
  • University of Cambridge, UK
Bruno C. d. S. Oliveira
  • The University of Hong Kong, China

Funding

This research was funded by the University of Hong Kong and Hong Kong Research Grants Council projects number 17209519, 17209520 and 17209821.

Acknowledgements

We thank the anonymous reviewers for their helpful and constructive comments.

Cite AsGet BibTex

Baber Rehman, Xuejing Huang, Ningning Xie, and Bruno C. d. S. Oliveira. Union Types with Disjoint Switches. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 25:1-25:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ECOOP.2022.25

Abstract

Union types are nowadays a common feature in many modern programming languages. This paper investigates a formulation of union types with an elimination construct that enables case analysis (or switches) on types. The interesting aspect of this construct is that each clause must operate on disjoint types. By using disjoint switches, it is possible to ensure exhaustiveness (i.e. all possible cases are handled), and that none of the cases overlap. In turn, this means that the order of the cases does not matter and that reordering the cases has no impact on the semantics, helping with program understanding and refactoring. While implemented in the Ceylon language, disjoint switches have not been formally studied in the research literature, although a related notion of disjointness has been studied in the context of disjoint intersection types. We study union types with disjoint switches formally and in a language independent way. We first present a simplified calculus, called the union calculus (λ_u), which includes disjoint switches and prove several results, including type soundness and determinism. The notion of disjointness in λ_u is in essence the dual notion of disjointness for intersection types. We then present a more feature-rich formulation of λ_u, which includes intersection types, distributive subtyping and a simple form of nominal types. This extension reveals new challenges. Those challenges require us to depart from the dual notion of disjointness for intersection types, and use a more general formulation of disjointness instead. Among other applications, we show that disjoint switches provide an alternative to certain forms of overloading, and that they enable a simple approach to nullable (or optional) types. All the results about λ_u and its extensions have been formalized in the Coq theorem prover.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Union types
  • switch expression
  • disjointness
  • intersection types

Metrics

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

Related Versions

Supplementary Materials

References

  1. Disjointness in ceylon. URL: http://web.mit.edu/ceylon_v1.3.3/ceylon-1.3.3/doc/en/spec/html_single.
  2. Overloading in ceylon. URL: https://github.com/ceylon/ceylon-spec/issues/73.
  3. Union types in typescript. URL: https://www.typescriptlang.org/docs/handbook/unions-and-intersections.html.
  4. João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi. Disjoint polymorphism. In European Symposium on Programming (ESOP), 2017. Google Scholar
  5. Davide Ancona and Andrea Corradi. Sound and complete subtyping between coinductive types for object-oriented languages. In European Conference on Object-Oriented Programming, pages 282-307. Springer, 2014. Google Scholar
  6. Davide Ancona and Andrea Corradi. Semantic subtyping for imperative object-oriented languages. ACM SIGPLAN Notices, 51(10):568-587, 2016. Google Scholar
  7. Inc Apple. Swift language guide, 2021. URL: https://docs.swift.org/swift-book/LanguageGuide/TheBasics.html.
  8. Subarno Banerjee, Lazaro Clapp, and Manu Sridharan. Nullaway: Practical type-based null safety for java. In Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pages 740-750, 2019. Google Scholar
  9. Franco Barbanera, Mariangiola Dezaniciancaglini, and Ugo Deliguoro. Intersection and union types: syntax and semantics. Information and Computation, 119(2):202-230, 1995. Google Scholar
  10. Véronique Benzaken, Giuseppe Castagna, and Alain Frisch. Cduce: an xml-centric general-purpose language. ACM SIGPLAN Notices, 38(9):51-63, 2003. Google Scholar
  11. 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
  12. Xuan Bi, Ningning Xie, Bruno C. d. S. Oliveira, and Tom Schrijvers. Distributive disjoint polymorphism for compositional programming. In Luís Caires, editor, Programming Languages and Systems, pages 381-409, Cham, 2019. Springer International Publishing. Google Scholar
  13. Gavin Bierman, Martín Abadi, and Mads Torgersen. Understanding typescript. In European Conference on Object-Oriented Programming, pages 257-281. Springer, 2014. Google Scholar
  14. Olivier Blanvillain, Jonathan Immanuel Brachthäuser, Maxime Kjaer, and Martin Odersky. Type-level programming with match types. Proc. ACM Program. Lang., 6(POPL), January 2022. URL: https://doi.org/10.1145/3498698.
  15. R. M. Burstall, D. B. MacQueen, and D. T. Sannella. Hope: An experimental applicative language. Technical Report CSR-62-80, Computer Science Dept, Univ. of Edinburgh, 1981. Google Scholar
  16. Peter Canning, William Cook, Walter Hill, Walter Olthoff, and John C Mitchell. F-bounded polymorphism for object-oriented programming. In Proceedings of the fourth international conference on functional programming languages and computer architecture, pages 273-280, 1989. 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. Giuseppe Castagna and Alain Frisch. A gentle introduction to semantic subtyping. In Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, pages 198-199, 2005. Google Scholar
  19. Giuseppe Castagna, Giorgio Ghelli, and Giuseppe Longo. A calculus for overloaded functions with subtyping. Information and Computation, 117(1):115-135, 1995. Google Scholar
  20. Giuseppe Castagna and Victor Lanvin. Gradual typing with union and intersection types. Proceedings of the ACM on Programming Languages, 1(ICFP):1-28, 2017. Google Scholar
  21. Giuseppe Castagna, Victor Lanvin, Mickaël Laurent, and Kim Nguyen. Revisiting occurrence typing. arXiv preprint arXiv:1907.05590, 2019. Google Scholar
  22. 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 Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pages 5-17, New York, NY, USA, 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2535838.2535840.
  23. Craig Chambers. Object-oriented multi-methods in Cecil. In Ole Lehrmann Madsen, editor, ECOOP '92, European Conference on Object-Oriented Programming, Utrecht, The Netherlands, volume 615, pages 33-56. Springer-Verlag, 1992. Google Scholar
  24. Avik Chaudhuri. Flow: a static type checker for javascript. SPLASH-I In Systems, Programming, Languages and Applications: Software for Humanity, 2015. Google Scholar
  25. Avik Chaudhuri, Panagiotis Vekris, Sam Goldman, Marshall Roch, and Gabriel Levi. Fast and precise type checking for javascript. Proceedings of the ACM on Programming Languages, 1(OOPSLA):1-30, 2017. Google Scholar
  26. Curtis Clifton, Gary T. Leavens, Craig Chambers, and Todd Millstein. Multijava: Modular open classes and symmetric multiple dispatch for java. In Proceedings of the 15th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA '00, pages 130-145, 2000. Google Scholar
  27. Ornela Dardha, Daniele Gorla, and Daniele Varacca. Semantic subtyping for objects and classes. In Formal Techniques for Distributed Systems, pages 66-82. Springer, 2013. Google Scholar
  28. Rowan Davies and Frank Pfenning. Intersection types and computational effects. In Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, pages 198-208, 2000. Google Scholar
  29. Joshua Dunfield. Elaborating intersection and union types. Journal of Functional Programming, 24(2-3):133-165, 2014. Google Scholar
  30. Joshua Dunfield and Frank Pfenning. Type assignment for intersections and unions in call-by-value languages. In International Conference on Foundations of Software Science and Computation Structures, pages 250-266. Springer, 2003. Google Scholar
  31. Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. Semantic subtyping. In Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pages 137-146. IEEE, 2002. Google Scholar
  32. Jacques Garrigue. Programming with polymorphic variants. In ML workshop, 1998. Google Scholar
  33. James Gosling, Bill Joy, Guy Steele, Gilad Bracha, Alex Buckley, Daniel Smith, and Gavin Bierman. The java language specification, 2021. URL: https://docs.oracle.com/javase/specs/jls/se14/html/index.html.
  34. Eric Gunnerson. Nullable types. In A Programmer’s Guide to C# 5.0, pages 247-250. Springer, 2012. Google Scholar
  35. Haruo Hosoya and Benjamin C Pierce. Xduce: A statically typed xml processing language. ACM Transactions on Internet Technology (TOIT), 3(2):117-148, 2003. Google Scholar
  36. Xuejing Huang and Bruno C d S Oliveira. Distributing intersection and union types with splits and duality (functional pearl). Proceedings of the ACM on Programming Languages, 5(ICFP):1-24, 2021. Google Scholar
  37. Atsushi Igarashi and Hideshi Nagira. Union types for object-oriented programming. In Proceedings of the 2006 ACM symposium on Applied computing, pages 1435-1441, 2006. Google Scholar
  38. Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight java: a minimal core calculus for java and gj. ACM Trans. Program. Lang. Syst., 23(3):396-450, 2001. URL: https://doi.org/10.1145/503502.503505.
  39. Gavin King. The ceylon language specification, version 1.0, 2013. Google Scholar
  40. Foundation Kotlin. Kotlin programming language, 2021. URL: https://kotlinlang.org/.
  41. David MacQueen, Gordon Plotkin, and Ravi Sethi. An ideal model for recursive polymorphic types. In Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 165-174, 1984. Google Scholar
  42. Fabian Muehlboeck and Ross Tate. Empowering union and intersection types with integrated subtyping. Proceedings of the ACM on Programming Languages, 2(OOPSLA):1-29, 2018. Google Scholar
  43. Abel Nieto, Yaoyu Zhao, Ondřej Lhoták, Angela Chang, and Justin Pu. Scala with Explicit Nulls. In 34th European Conference on Object-Oriented Programming (ECOOP 2020), Leibniz International Proceedings in Informatics (LIPIcs), pages 25:1-25:26, 2020. Google Scholar
  44. Martin Odersky. Scala 3: A next generation compiler for scala, 2021. URL: https://dotty.epfl.ch.
  45. Bruno C. d. S. Oliveira, Zhiyuan Shi, and Joao Alpuim. Disjoint intersection types. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, pages 364-377, 2016. Google Scholar
  46. Matthew M Papi, Mahmood Ali, Telmo Luis Correa Jr, Jeff H Perkins, and Michael D Ernst. Practical pluggable types for java. In Proceedings of the 2008 international symposium on Software testing and analysis, pages 201-212, 2008. Google Scholar
  47. Benjamin C Pierce. Programming with intersection types, union types. Technical report, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, 1991. Google Scholar
  48. Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 1st edition, 2002. Google Scholar
  49. John C Reynolds. Preliminary design of the programming language forsythe, 1988. Google Scholar
  50. Richard Routley and Robert K Meyer. The semantics of entailment—iii. Journal of philosophical logic, 1(2):192-208, 1972. Google Scholar
  51. Sam Tobin-Hochstadt and Matthias Felleisen. The design and implementation of typed scheme. ACM SIGPLAN Notices, 43(1):395-406, 2008. Google Scholar
  52. Sam Tobin-Hochstadt and Matthias Felleisen. Logical types for untyped languages. In Proceedings of the 15th ACM SIGPLAN international conference on Functional programming, pages 117-128, 2010. Google Scholar
  53. Steffen van Bakel, Mariangiola Dezani-Ciancaglini, Ugo de’Liguoro, and Yoko Motohoma. The minimal relevant logic and the call-by-value lambda calculus. Technical report, Citeseer, 2000. Google Scholar
  54. Adriaan Van Wijngaarden, Barry J Mailloux, John EL Peck, Cornelius HA Koster, M Sintzoff, CH Lindsey, LGLT Meertens, and RG Fisker. Report on the algorithmic language algol 68. Numerische Mathematik, 14(1):79-218, 1969. Google Scholar
  55. Adriaan van Wijngaarden, Barry James Mailloux, John Edward Lancelot Peck, Cornelis HA Koster, CH Lindsey, M Sintzoff, Lambert GLT Meertens, and RG Fisker. Revised report on the algorithmic language Algol 68. Springer Science & Business Media, 2012. Google Scholar
  56. Philip Wadler and Stephen Blott. How to make ad-hoc polymorphism less ad hoc. In Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 60-76, 1989. Google Scholar
  57. 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):1-27, 2018. 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