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.
Supplemental Material
- 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). Google ScholarDigital Library
- Jeff Bezanson. 2015. Abstraction in technical computing. Ph.D. Dissertation. Massachusetts Institute of Technology. http://hdl.handle.net/1721.1/99811Google Scholar
- Jeff Bezanson, Alan Edelman, Stefan Karpinski, and Viral B. Shah. 2017. Julia: A Fresh Approach to Numerical Computing. SIAM Rev. 59, 1 (2017).Google ScholarDigital Library
- Ambrose Bonnaire-Sergeant, Rowan Davies, and Sam Tobin-Hochstadt. 2016. Practical optional types for Clojure. In European Symposium on Programming (ESOP).Google ScholarCross Ref
- François Bourdoncle and Stephan Merz. 1997. Type Checking Higher-order Polymorphic Multi-methods. In Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- Nicholas Cameron, Sophia Drossopoulou, and Erik Ernst. 2008. A Model for Java with Wildcards. In European Conference on Object-Oriented Programming (ECOOP). Google ScholarDigital Library
- 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). Google ScholarDigital Library
- 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). Google ScholarDigital Library
- Giuseppe Castagna and Benjamin C. Pierce. 1994. Decidable Bounded Quantification. In Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- Craig Chambers and Gary T. Leavens. 1994. Typechecking and Modules for Multi-methods. In Conference on Object-oriented Programming Systems, Languages and Applications (OOPSLA). Google ScholarDigital Library
- John Chambers. 2014. Object-Oriented Programming, Functional Programming and R. Statist. Sci. 2 (2014). Issue 29.Google Scholar
- 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. Google ScholarDigital Library
- 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). Google ScholarDigital Library
- Linda DeMichiel and Richard Gabriel. 1987. The Common Lisp Object System: An Overview. In European Conference on Object-Oriented Programming (ECOOP). Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. 2002. Semantic Subtyping. In Symposium on Logic in Computer Science (LICS). Google ScholarDigital Library
- 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). Google ScholarDigital Library
- Radu Grigore. 2017. Java Generics Are Turing Complete. In Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- 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/Google Scholar
- 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. Google ScholarDigital Library
- Vassily Litvinov. 2003. Constraint-Bounded Polymorphism: an Expressive and Practical Type System for Object-Oriented Languages. Ph.D. Dissertation. University of Washington. Google ScholarDigital Library
- 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.Google Scholar
- Benjamin C. Pierce. 1992. Bounded Quantification is Undecidable. In Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- Allison Randal, Dan Sugalski, and Leopold Toetsch. 2003. Perl 6 and Parrot Essentials. O’Reilly.Google Scholar
- 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). Google ScholarDigital Library
- Ross Tate, Alan Leung, and Sorin Lerner. 2011. Taming Wildcards in Java’s Type System. In Conference on Programming Language Design and Implementation (PLDI). Google ScholarDigital Library
- The Julia Language. 2018. Manual: Diagonal Types. Retrieved 2018-07-24 from https://docs.julialang.org/en/v0.6.1/devdocs/ types/#Diagonal- types- 1Google Scholar
- Jerome Vouillon. 2004. Subtyping Union Types. In Computer Science Logic (CSL).Google Scholar
- Stefan Wehr and Peter Thiemann. 2009. On the Decidability of Subtyping with Bounded Existential Types. In Programming Languages and Systems (ESOP). Google ScholarDigital Library
- 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/Google Scholar
- Steve Zdancewic. 2006. A Note on “Type Inference for Java 5”. https://web.archive.org/web/20060920024504/http: //www.cis.upenn.edu/~stevez/note.htmlGoogle Scholar
Index Terms
- Julia subtyping: a rational reconstruction
Recommendations
Integrating coercion with subtyping and multiple dispatch
Coercion can greatly improve the readability of programs, especially in arithmetic expressions. However, coercion interacts with other features of programming languages, particularly subtyping and overloaded functions and operators, in ways that can ...
Subtyping delimited continuations
ICFP '11: Proceedings of the 16th ACM SIGPLAN international conference on Functional programmingWe present a type system with subtyping for first-class delimited continuations that generalizes Danvy and Filinski's type system for shift and reset by maintaining explicit information about the types of contexts in the metacontext. We exploit this ...
Unifying typing and subtyping
In recent years dependent types have become a hot topic in programming language research. A key reason why dependent types are interesting is that they allow unifying types and terms, which enables both additional expressiveness and economy of concepts. ...
Comments