Julia subtyping: a rational reconstruction

Abstract

Programming languages that support multiple dispatch rely on an expressive notion of subtyping to specify method applicability. In these languages, type annotations on method declarations are used to select, out of a potentially large set of methods, the one that is most appropriate for a particular tuple of arguments. Julia is a language for scientific computing built around multiple dispatch and an expressive subtyping relation. This paper provides the first formal definition of Julia's subtype relation and motivates its design. We validate our specification empirically with an implementation of our definition that we compare against the existing Julia implementation on a collection of real-world programs. Our subtype implementation differs on 122 subtype tests out of 6,014,476. The first 120 differences are due to a bug in Julia that was fixed once reported; the remaining 2 are under discussion.

References

1. Eric Allen, Justin Hilburn, Scott Kilpatrick, Victor Luchangco, Sukyoung Ryu, David Chase, and Guy Steele. 2011. Type Checking Modular Multiple Dispatch with Parametric Polymorphism and Multiple Inheritance. In Conference on Object Oriented Programming Systems, Languages and Applications (OOPSLA).
2. Jeff Bezanson. 2015. Abstraction in technical computing. Ph.D. Dissertation. Massachusetts Institute of Technology. http://hdl.handle.net/1721.1/99811
3. Jeff Bezanson, Alan Edelman, Stefan Karpinski, and Viral B. Shah. 2017. Julia: A Fresh Approach to Numerical Computing. SIAM Rev. 59, 1 (2017).
4. Ambrose Bonnaire-Sergeant, Rowan Davies, and Sam Tobin-Hochstadt. 2016. Practical optional types for Clojure. In European Symposium on Programming (ESOP).
5. François Bourdoncle and Stephan Merz. 1997. Type Checking Higher-order Polymorphic Multi-methods. In Symposium on Principles of Programming Languages (POPL).
6. Nicholas Cameron, Sophia Drossopoulou, and Erik Ernst. 2008. A Model for Java with Wildcards. In European Conference on Object-Oriented Programming (ECOOP).
7. 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).
8. Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, Hyeonseung Im, Sergueï Lenglet, and Luca Padovani. 2014. Polymorphic Functions with Set-theoretic Types: Part 1: Syntax, Semantics, and Evaluation. In Symposium on Principles of Programming Languages (POPL).
9. Giuseppe Castagna and Benjamin C. Pierce. 1994. Decidable Bounded Quantification. In Symposium on Principles of Programming Languages (POPL).
10. Craig Chambers and Gary T. Leavens. 1994. Typechecking and Modules for Multi-methods. In Conference on Object-oriented Programming Systems, Languages and Applications (OOPSLA).
11. John Chambers. 2014. Object-Oriented Programming, Functional Programming and R. Statist. Sci. 2 (2014). Issue 29.
12. Koen Claessen and John Hughes. 2000. QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP ’00). ACM, New York, NY, USA, 268–279.
13. Curtis Clifton, Gary T. Leavens, Craig Chambers, and Todd Millstein. 2000. MultiJava: Modular Open Classes and Symmetric Multiple Dispatch for Java. In Conference on Object-oriented Programming, Systems, Languages, and Applications (OOPSLA).
14. Linda DeMichiel and Richard Gabriel. 1987. The Common Lisp Object System: An Overview. In European Conference on Object-Oriented Programming (ECOOP).
15. Jonas Duregård, Patrik Jansson, and Meng Wang. 2012. Feat: Functional Enumeration of Algebraic Types. In Proceedings of the 2012 Haskell Symposium (Haskell ’12). ACM, New York, NY, USA, 61–72.
16. Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. 2002. Semantic Subtyping. In Symposium on Logic in Computer Science (LICS).
17. Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. 2008. Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types. J. ACM 55, 4 (2008).
18. Radu Grigore. 2017. Java Generics Are Turing Complete. In Symposium on Principles of Programming Languages (POPL).
19. Andrew Kennedy and Benjamin C. Pierce. 2007. On Decidability of Nominal Subtyping with Variance. In Workshop on Foundations and Developments of Object-Oriented Languages (FOOL/WOOD). https://www.microsoft.com/en- us/research/ publication/on- decidability- of- nominal- subtyping- with- variance/
20. Vassily Litvinov. 1998. Constraint-based Polymorphism in Cecil: Towards a Practical and Static Type System. In Addendum to the Conference on Object-oriented Programming, Systems, Languages, and Applications.
21. Vassily Litvinov. 2003. Constraint-Bounded Polymorphism: an Expressive and Practical Type System for Object-Oriented Languages. Ph.D. Dissertation. University of Washington.
22. Karl Mazurak and Steve Zdancewic. 2005. Type Inference for Java 5: Wildcards, F-Bounds, and Undecidability. (2005). https://pdfs.semanticscholar.org/a73a/aace3ecafb9f8f4f627705647115c29ef63e.pdf unpublished.
23. Benjamin C. Pierce. 1992. Bounded Quantification is Undecidable. In Symposium on Principles of Programming Languages (POPL).
24. Allison Randal, Dan Sugalski, and Leopold Toetsch. 2003. Perl 6 and Parrot Essentials. O’Reilly.
25. 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).
26. Ross Tate, Alan Leung, and Sorin Lerner. 2011. Taming Wildcards in Java’s Type System. In Conference on Programming Language Design and Implementation (PLDI).
27. The Julia Language. 2018. Manual: Diagonal Types. Retrieved 2018-07-24 from https://docs.julialang.org/en/v0.6.1/devdocs/ types/#Diagonal- types- 1
28. Jerome Vouillon. 2004. Subtyping Union Types. In Computer Science Logic (CSL).
29. Stefan Wehr and Peter Thiemann. 2009. On the Decidability of Subtyping with Bounded Existential Types. In Programming Languages and Systems (ESOP).
30. Francesco Zappa Nardelli, Julia Belyakova, Artem Pelenitsyn, Benjamin Chung, Jeff Bezanson, and Jan Vitek. 2018. Julia Subtyping: a Rational Reconstruction — Project Web-Page. Retrieved 2018-07-24 from https://www.di.ens.fr/~zappa/ projects/lambdajulia/
31. Steve Zdancewic. 2006. A Note on “Type Inference for Java 5”. https://web.archive.org/web/20060920024504/http: //www.cis.upenn.edu/~stevez/note.html

Index Terms

• Software and its engineering

  • Software notations and tools

    • Formal language definitions

      • Semantics

    • General programming languages

      • Language features

        • Data types and structures