Decidable Subtyping of Existential Types for Julia
Article No.: 191, Pages 1091 - 1114
Abstract
Julia is a modern scientific-computing language that relies on multiple dispatch to implement generic libraries. While the language does not have a static type system, method declarations are decorated with expressive type annotations to determine when they are applicable. To find applicable methods, the implementation uses subtyping at run-time. We show that Julia's subtyping is undecidable, and we propose a restriction on types to recover decidability by stratifying types into method signatures over value types---where the former can freely use bounded existential types but the latter are restricted to use-site variance. A corpus analysis suggests that nearly all Julia programs written in practice already conform to this restriction.
Supplementary Material
This material is an extension of the PLDI 2024 paper with a technical appendix.
- Download
- 1.61 MB
References
[1]
Alexander Aiken and Edward L. Wimmers. 1993. Type inclusion constraints and type inference. In Conference on Functional Programming Languages and Computer Architecture (FPCA). https://doi.org/10.1145/165180.165188
[2]
Julia Belyakova. 2023. Decidable Subtyping of Existential Types for the Julia Language. Ph. D. Dissertation. Northeastern University. https://onesearch.library.northeastern.edu/permalink/01NEU_INST/87npqb/cdi_proquest_journals_2853689755
[3]
Jeff Bezanson. 2015. Abstraction in technical computing. Ph. D. Dissertation. Massachusetts Institute of Technology. http://hdl.handle.net/1721.1/99811
[4]
Jeff Bezanson, Jiahao Chen, Ben Chung, Stefan Karpinski, Viral B. Shah, Jan Vitek, and Lionel Zoubritzky. 2018. Julia: Dynamism and Performance Reconciled by Design. Proc. ACM Program. Lang., 2, OOPSLA (2018), https://doi.org/10.1145/3276490
[5]
Jeff Bezanson, Alan Edelman, Stefan Karpinski, and Viral B. Shah. 2017. Julia: A Fresh Approach to Numerical Computing. SIAM Rev., 59, 1 (2017), https://doi.org/10.1137/141000671
[6]
Daniel G. Bobrow, Kenneth Kahn, Gregor Kiczales, Larry Masinter, Mark Stefik, and Frank Zdybel. 1986. CommonLoops: Merging Lisp and Object-Oriented Programming. In Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA). https://doi.org/10.1145/28697.28700
[7]
Francois Bourdoncle and Stephan Merz. 1997. Type checking higher-order polymorphic multi-methods. In Symposium on Principles of Programming Languages (POPL). https://doi.org/10.1145/263699.263743
[8]
Nicholas Cameron, Sophia Drossopoulou, and Erik Ernst. 2008. A Model for Java with Wildcards. In European Conference on Object-Oriented Programming (ECOOP). https://doi.org/10.1007/978-3-540-70592-5_2
[9]
Luca Cardelli, Simone Martini, John C. Mitchell, and Andre Scedrov. 1991. An Extension of System F with Subtyping. In Theoretical Aspects of Computer Software (TACS). https://doi.org/10.1007/3-540-54415-1_73
[10]
Luca Cardelli and Peter Wegner. 1985. On Understanding Types, Data Abstraction, and Polymorphism. ACM Comput. Surv., 17, 4 (1985), https://doi.org/10.1145/6041.6042
[11]
Giuseppe Castagna and Alain Frisch. 2005. A Gentle Introduction to Semantic Subtyping. In Principles and Practice of Declarative Programming (PPDP). https://doi.org/10.1145/1069774.1069793
[12]
Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, and Pietro Abate. 2015. Polymorphic Functions with Set-Theoretic Types: Part 2: Local Type Inference and Type Reconstruction. In Symposium on Principles of Programming Languages (POPL). https://doi.org/10.1145/2676726.2676991
[13]
Satish Chandra, Colin S. Gordon, Jean-Baptiste Jeannin, Cole Schlesinger, Manu Sridharan, Frank Tip, and Youngil Choi. 2016. Type inference for static compilation of JavaScript. https://doi.org/10.1145/2983990.2984017
[14]
Avik Chaudhuri, Panagiotis Vekris, Sam Goldman, Marshall Roch, and Gabriel Levi. 2017. Fast and precise type checking for JavaScript. Proc. ACM Program. Lang., 1, OOPSLA (2017), https://doi.org/10.1145/3133872
[15]
Benjamin Chung. 2023. A type system for Julia. Ph. D. Dissertation. Northeastern University. arxiv:2310.16866
[16]
Benjamin Chung, Francesco Zappa Nardelli, and Jan Vitek. 2019. Julia’s Efficient Algorithm for Subtyping Unions and Covariant Tuples. In European Conference on Object-Oriented Programming (ECOOP). https://doi.org/10.4230/LIPIcs.ECOOP.2019.24
[17]
Pierre-Louis Curien and Giorgio Ghelli. 1990. Coherence of subsumption. In Colloquium on Trees in Algebra and Programming (CAAP). https://doi.org/10.1007/3-540-52590-4_45
[18]
Luis Damas and Robin Milner. 1982. Principal type-schemes for functional programs. In Symposium on Principles of Programming Languages (POPL). https://doi.org/10.1145/582153.582176
[19]
Jean-Yves Girard. 1987. Linear logic. Theoretical Computer Science, https://doi.org/10.1016/0304-3975(87)90045-4
[20]
Ben Greenman, Fabian Muehlboeck, and Ross Tate. 2014. Getting F-Bounded Polymorphism into Shape. In Conference on Programming Language Design and Implementation (PLDI). https://doi.org/10.1145/2594291.2594308
[21]
Radu Grigore. 2017. Java Generics Are Turing Complete. In Symposium on Principles of Programming Languages (POPL). https://doi.org/10.1145/3009837.3009871
[22]
Roger Hindley. 1969. The Principal Type-Scheme of an Object in Combinatory Logic. Trans. Amer. Math. Soc., https://doi.org/10.2307/1995158
[23]
John Hopcroft and Jeffrey Ullman. 1990. Introduction To Automata Theory, Languages, And Computation. Addison-Wesley.
[24]
Jason Z. S. Hu and Ondřej Lhoták. 2019. Undecidability of D<: And Its Decidable Fragments. Proc. ACM Program. Lang., 4, POPL (2019), https://doi.org/10.1145/3371077
[25]
Atsushi Igarashi and Mirko Viroli. 2002. On Variance-Based Subtyping for Parametric Types. In European Conference on Object-Oriented Programming (ECOOP). https://doi.org/10.1007/3-540-47993-7_19
[26]
Andrew Kennedy and Benjamin C. Pierce. 2007. On Decidability of Nominal Subtyping with Variance. In Foundations and Developments of Object-Oriented Languages (FOOL). https://www.microsoft.com/en-us/research/publication/on-decidability-of-nominal-subtyping-with-variance/
[27]
Kresten Krab Thorup and Mads Torgersen. 1999. Unifying Genericity. In European Conference on Object-Oriented Programming (ECOOP). https://doi.org/10.1007/3-540-48743-3_9
[28]
Julian Mackay, Alex Potanin, Jonathan Aldrich, and Lindsay Groves. 2019. Decidable Subtyping for Path Dependent Types. Proc. ACM Program. Lang., 4, POPL (2019), https://doi.org/10.1145/3371134
[29]
Julian Mackay, Alex Potanin, Jonathan Aldrich, and Lindsay Groves. 2020. Syntactically Restricting Bounded Polymorphism for Decidable Subtyping. In Programming Languages and Systems (APLAS). https://doi.org/10.1007/978-3-030-64437-6_7
[30]
Greg Morrisett, David Walker, Karl Crary, and Neal Glew. 1998. From System F to Typed Assembly Language. In Symposium on Principles of Programming Languages (POPL). https://doi.org/10.1145/268946.268954
[31]
Artem Pelenitsyn, Julia Belyakova, Benjamin Chung, Ross Tate, and Jan Vitek. 2021. Type Stability in Julia: Avoiding Performance Pathologies in JIT Compilation. Proc. ACM Program. Lang., 5, OOPSLA (2021), https://doi.org/10.1145/3485527
[32]
Benjamin C. Pierce. 1992. Bounded Quantification is Undecidable. In Symposium on Principles of Programming Languages (POPL). https://doi.org/10.1145/143165.143228
[33]
François Pottier. 1998. A framework for type inference with subtyping. In International Conference on Functional Programming (ICFP). https://doi.org/10.1145/289423.289448
[34]
Daniel Smith and Robert Cartwright. 2008. Java Type Inference is Broken: Can We Fix It? In Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA). https://doi.org/10.1145/1449764.1449804
[35]
Ross Tate, Juan Chen, and Chris Hawblitzel. 2008. A Flexible Framework for Type Inference with Existential Quantification. https://www.microsoft.com/en-us/research/publication/a-flexible-framework-for-type-inference-with-existential-quantification/
[36]
Ross Tate, Juan Chen, and Chris Hawblitzel. 2010. Inferable object-oriented typed assembly language. In Conference on Programming Language Design and Implementation (PLDI). https://doi.org/10.1145/1806596.1806644
[37]
Ross Tate, Alan Leung, and Sorin Lerner. 2011. Taming Wildcards in Java’s Type System. In Conference on Programming Language Design and Implementation (PLDI). https://doi.org/10.1145/1993498.1993570
[38]
Mads Torgersen, Erik Ernst, and Christian Plesner Hansen. 2005. Wild FJ. In Foundations of Object-Oriented Languages (FOOL). https://homepages.inf.ed.ac.uk/wadler/fool/program/final/14/14_Paper.pdf
[39]
Mads Torgersen, Christian Plesner Hansen, Erik Ernst, Peter von der Ahé, Gilad Bracha, and Neal Gafter. 2004. Adding Wildcards to the Java Programming Language. In Symposium on Applied Computing (SAC). https://doi.org/10.1145/967900.968162
[40]
Valery Trifonov and Scott Smith. 1996. Subtyping constrained types. In Static Analysis Symposium (SAS). https://doi.org/10.1007/3-540-61739-6_52
[41]
Stefan Wehr and Peter Thiemann. 2009. On the Decidability of Subtyping with Bounded Existential Types. In Programming Languages and Systems (ESOP). https://doi.org/10.1007/978-3-642-10672-9_10
[42]
Francesco Zappa Nardelli, Julia Belyakova, Artem Pelenitsyn, Benjamin Chung, Jeff Bezanson, and Jan Vitek. 2018. Julia Subtyping: A Rational Reconstruction. Proc. ACM Program. Lang., 2, OOPSLA (2018), https://doi.org/10.1145/3276483
Index Terms
- Decidable Subtyping of Existential Types for Julia
Recommendations
Decidable subtyping for path dependent types
Path dependent types have long served as an expressive component of the Scala programming language. They allow for the modelling of both bounded polymorphism and a degree of nominal subtyping. Nominality in turn provides the ability to capture first ...
On subtyping, wildcards, and existential types
FTfJP '09: Proceedings of the 11th International Workshop on Formal Techniques for Java-like ProgramsWildcards are an often confusing part of the Java type system: the behaviour of wildcard types is not fully specified by subtyping, due to wildcard capture, and the rules for type checking are often misunderstood. Their very formulation seems somehow '...
Subtyping recursive types
We investigate the interactions of subtyping and recursive types, in a simply typed λ-calculus. The two fundamental questions here are whether two (recursive)types are in the subtype relation and whether a term has a type. To address the first question, ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 20 June 2024
Published in PACMPL Volume 8, Issue PLDI
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
- ERC-CZ
- NSF (National Science Foundation)
- GACR EXPRO
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 382Total Downloads
- Downloads (Last 12 months)382
- Downloads (Last 6 weeks)35
Reflects downloads up to 28 Jan 2025
Other Metrics
Citations
Cited By
View allView Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in