Fabian Muehlboeck
Ross Tate
Skip Abstract Section
Skip Supplemental Material SectionAbstract
Union and intersection types are both simple and powerful but have seen limited adoption. The problem is that, so far, subtyping algorithms for type systems extended with union and intersections have typically been either unreliable or insufficiently expressive. We present a simple and composable framework for empowering union and intersection types so that they interact with the rest of the type system in an intuitive and yet still decidable manner. We demonstrate the utility of this framework by illustrating the impact it has made throughout the design of the Ceylon programming language developed by Red Hat.
Supplemental Material
- Coşku Acay and Frank Pfenning. 2017. Intersections and Unions of Session Types . Electronic Proceedings in Theoretical Computer Science 242, ITRS (2017), 4–19.Google Scholar
Cross Ref
- Alexander Aiken and Edward L. Wimmers. 1993. Type Inclusion Constraints and Type Inference . In FPCA. ACM, New York, NY, USA, 31–41. Google ScholarDigital Library
- Davide Ancona and Andrea Corradi. 2016. Semantic Subtyping for Imperative Object-oriented Languages . In OOPSLA. ACM, New York, NY, USA, 568–587. Google ScholarDigital Library
- Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. 2014. NetKAT: Semantic Foundations for Networks . In POPL. ACM, New York, NY, USA, 113–126. Google ScholarDigital Library
- Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Ugo de’Liguoro. 1995. Intersection and Union Types: Syntax and Semantics . Information and Computation 119, 2 (1995), 202–230. Google ScholarDigital Library
- Jeff Bezanson, Alan Edelman, Stefan Karpinski, and Viral B. Shah. 2017. Julia: A Fresh Approach to Numerical Computing . SIAM Rev. 59, 1 (2017), 65–98.Google ScholarDigital Library
- Gavin Bierman, Martín Abadi, and Mads Torgersen. 2014. Understanding TypeScript . In ECOOP. Springer Berlin Heidelberg, Berlin, Heidelberg, DE, 257–281. Google ScholarDigital Library
- Filippo Bonchi and Damien Pous. 2013. Checking NFA Equivalence with Bisimulations up to Congruence . In POPL. ACM, New York, NY, USA, 457–468. Google ScholarDigital Library
- Michael Brandt and Fritz Henglein. 1998. Coinductive Axiomatization of Recursive Type Equality and Subtyping . Fundamenta Informaticae 33, 4 (1998), 309–338. Google ScholarDigital Library
- Giuseppe Castagna and Zhiwu Xu. 2011. Set-Theoretic Foundation of Parametric Polymorphism and Subtyping . In ICFP. ACM, New York, NY, USA, 94–106. Google ScholarDigital Library
- Sylvan Clebsch, Sophia Drossopoulou, Sebastian Blessing, and Andy McNeil. 2015. Deny Capabilities for Safe, Fast Actors . In AGERE! ACM, New York, NY, USA, 1–12. Google ScholarDigital Library
- Mario Coppo and Mariangiola Dezani-Ciancaglini. 1978. A New Type Assignment for λ-Terms . Archiv für Mathematische Logik und Grundlagenforschung 19, 1 (1978), 139–156.Google ScholarCross Ref
- Mario Coppo, Mariangiola Dezani-Ciancaglini, and Patrick Sallé. 1979. Functional Characterization of Some Semantic Equalities Inside λ-Calculus . Automata, Languages and Programming 71 (1979), 133–146. Google ScholarDigital Library
- Pierre-Louis Curien and Giorgio Ghelli. 1992. Coherence of Subsumption, Minimum Typing and Type-Checking in F ≤ . Mathematical Structures in Computer Science 2, 1 (1992), 55—-91.Google ScholarCross Ref
- Luís Damas and Robin Milner. 1982. Principal Type-Schemes for Functional Programs . In POPL. ACM, New York, NY, USA, 207–212. Google ScholarDigital Library
- Ornela Dardha, Daniele Gorla, and Daniele Varacca. 2013. Semantic Subtyping for Objects and Classes . In MOODS/FORTE. Springer Berlin Heidelberg, Berlin, Heidelberg, DEU, 66–82.Google Scholar
- Facebook. 2014. The Flow Static Type Checker Documentation .Google Scholar
- Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. 2002. Semantic Subtyping . In LICS. IEEE, Washington, DC, USA, 137–146. Google ScholarDigital Library
- Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. 2008. Semantic Subtyping: Dealing Set-Theoretically with Function, Union, Intersection, and Negation Types . Journal of the ACM 55, 4, Article 19 (2008), 64 pages. Google ScholarDigital Library
- Nils Gesbert, Pierre Genevès, and Nabil Layaïda. 2015. A Logical Approach to Deciding Semantic Subtyping . TOPLAS 38, 1, Article 3 (2015), 31 pages. Google ScholarDigital Library
- Paul Gochet, Pascal Gribomont, and Didier Rossetto. 2005. Algorithms for Relevant Logic . In Logic, Thought and Action. Springer Netherlands, Dordrecht, NLD, 479–496.Google Scholar
- James Gosling, Bill Joy, Guy Steele, and Gilad Bracha. 2005. The Java™ Language Specification, 3rd Edition . Addison-Wesley Professional, Boston, MA, USA. Google ScholarDigital Library
- Ben Greenman, Fabian Muehlboeck, and Ross Tate. 2014. Getting F-Bounded Polymorphism into Shape . In PLDI. ACM, New York, NY, USA, 89–99. Google ScholarDigital Library
- Anders Hejlsberg, Scott Wiltamuth, and Peter Golde. 2005. C# Language Specification 2.0 . Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA. Google ScholarDigital Library
- Fritz Henglein and Lasse Nielsen. 2011. Regular Expression Containment: Coinductive Axiomatization and Computational Interpretation . In POPL. ACM, New York, NY, USA, 385–398. Google ScholarDigital Library
- Haruo Hosoya and Benjamin C. Pierce. 2003. XDuce: A Statically Typed XML Processing Language . ACM Transactions on Internet Technology 3, 2 (2003), 117–148. Google ScholarDigital Library
- Haruo Hosoya, Jérôme Vouillon, and Benjamin C. Pierce. 2000. Regular Expression Types for XML . In ICFP. ACM, New York, NY, USA, 11–22. Google ScholarDigital Library
- Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. 2017. CoCaml: Functional Programming with Regular Coinductive Types . Fundamenta Informaticae 150, 3/4 (2017), 347–377.Google ScholarDigital Library
- Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. 2007. Practical Type Inference for Arbitrary-Rank Types . Journal of Functional Programming 17, 1 (2007), 1–82. Google ScholarDigital Library
- Andrew J. Kennedy and Benjamin C. Pierce. 2007. On Decidability of Nominal Subtyping with Variance . In FOOL. ACM, New York, NY, USA, Article 5, 12 pages.Google Scholar
- Gavin King. 2013. The Ceylon Language Specification, Version 1.0 .Google Scholar
- Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. 1995. Efficient Recursive Subtyping . Mathematical Structures in Computer Science 5, 1 (1995), 113–125.Google ScholarCross Ref
- Luigi Liquori and Claude Stolze. 2017. A Decidable Subtyping Logic for Intersection and Union Types . In Topics in Theoretical Computer Science. Springer International Publishing, Cham, CHE, 74–90.Google Scholar
- Microsoft. 2012. TypeScript .Google Scholar
- Microsoft. 2018. The Typescript Handbook .Google Scholar
- John C. Mitchell. 1988. Polymorphic Type Inference and Containment . Information and Computation 76, 2/3 (1988), 211–249. Google ScholarDigital Library
- Fabian Muehlboeck and Ross Tate. 2018. Artifact for Article “Empowering Union and Intersection Types with Integrated Subtyping” . In OOPSLA. ACM, New York, NY, USA.Google Scholar
- Martin Odersky and Konstantin Läufer. 1996. Putting Type Annotations to Work . In POPL. ACM, New York, NY, USA, 54–67. Google ScholarDigital Library
- Jens Palsberg and Christina Pavlopoulou. 1998. From Polyvariant Flow Information to Intersection and Union Types . In POPL. ACM, New York, NY, USA, 197–208. Google ScholarDigital Library
- Benjamin C. Pierce. 1989. A Decision Procedure for the Subtype Relation on Intersection Types with Bounded Variables . Technical Report CMU-CS-89-169. Carnegie Mellon University.Google Scholar
- Benjamin C. Pierce. 1991. Programming with Intersection Types, Union Types, and Polymorphism . Technical Report CMU-CS-91-106. Carnegie Mellon University.Google Scholar
- Benjamin C. Pierce. 2002. Types and Programming Languages . MIT Press, Boston, MA, USA. Google ScholarDigital Library
- Garrell Pottinger. 1980. A Type Assignment for the Strongly Normalizable λ-Terms . In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, London, GBR, New York, NY, USA.Google Scholar
- John C. Reynolds. 1988. Preliminary Design of the Programming Language Forsythe . Technical Report CMU-CS-88-159. Carnegie Mellon University.Google Scholar
- John C. Reynolds. 1997. Design of the Programming Language Forsythe . In ALGOL-like Languages. Birkhäuser Boston, Boston, MA, USA, 173–233.Google Scholar
- Tiark Rompf and Nada Amin. 2016. Type Soundness for Dependent Object Types (DOT) . In OOPSLA. ACM, New York, NY, USA, 624–641. Google ScholarDigital Library
- Richard Routley and Robert K. Meyer. 1972. The Semantics of Entailment: III . Journal of Philosophical Logic 1, 2 (1972), 192–208.Google ScholarCross Ref
- Ross Tate, Alan Leung, and Sorin Lerner. 2011. Taming Wildcards in Java’s Type System . In PLDI. ACM, New York, NY, USA, 614–627. Google ScholarDigital Library
- The Coq Development Team. 1984. The Coq Proof Assistant .Google Scholar
- The Dotty Development Team. 2015. Dotty .Google Scholar
- Sam Tobin-Hochstadt and Matthias Felleisen. 2008. The Design and Implementation of Typed Scheme . In POPL. ACM, New York, NY, USA, 395–406. Google ScholarDigital Library
- Steffen van Bakel, Mariangiola Dezani-Ciancaglini, Ugo de’Liguoro, and Yoko Motohama. 2000. The Minimal Relevant Logic and the Call-by-Value Lambda Calculus . Technical Report TR-ARP-05-2000. Australian National University.Google Scholar
- Adriaan van Wijngaarden, Barry J. Mailloux, John E. L. Peck, Cornelis H. A. Koster, Michel Sintzoff, Charles H. Lindsey, Lambert G. L. T. Meertens, and Richard G. Fisker (Eds.). 1975. Revised Report on the Algorithmic Language ALGOL 68 . Acta Informatica 5 (1975), 1–236. Google ScholarDigital Library
- Luca Viganò. 2000. An O(n log n)-Space Decision Procedure for the Relevance Logic B+ . Studia Logica 66, 3 (2000), 385–407.Google ScholarCross Ref
- Mirko Viroli. 2000. On the Recursive Generation of Parametric Types . Technical Report DEIS-LIA-00-002. University of Bologna.Google Scholar
- Joe B. Wells, Allyn Dimock, Robert Muller, and Franklyn Turbak. 2002. A Calculus with Polymorphic and Polyvariant Flow Types . Journal of Functional Programming 12, 3 (2002), 183–227. Google ScholarDigital Library
- Francesco Zappa Nardelli, Julia Belyakova, Artem Pelenitsyn, Benjamin Chung, Jeff Bezanson, and Jan Vitek. 2018. Julia Subtyping: A Rational Reconstruction . In OOPSLA. ACM, New York, NY, USA, Article 113, 28 pages. Google ScholarDigital Library
Index Terms
- Empowering union and intersection types with integrated subtyping
Recommendations
Distributing intersection and union types with splits and duality (functional pearl)
Subtyping with intersection and union types is nowadays common in many programming languages. From the perspective of logic, the subtyping problem is essentially the problem of determining logical entailment: does a logical statement follow from another ...
Gradual typing with union and intersection types
We propose a type system for functional languages with gradual types and set-theoretic type connectives and prove its soundness. In particular, we show how to lift the definition of the domain and result type of an application from non-gradual types to ...
Decidable tag-based semantic subtyping for nominal types, tuples, and unions
FTfJP '19: Proceedings of the 21st Workshop on Formal Techniques for Java-like ProgramsSemantic subtyping enables simple, set-theoretical reasoning about types by interpreting a type as the set of its values. Previously, semantic subtyping has been studied primarily in the context of statically typed languages with structural typing. In ...
Comments