Abstract
Dependent Object Types (DOT) is intended to be a core calculus for modelling Scala. Its distinguishing feature is abstract type members, fields in objects that hold types rather than values. Proving soundness of DOT has been surprisingly challenging, and existing proofs are complicated, and reason about multiple concepts at the same time (e.g. types, values, evaluation). To serve as a core calculus for Scala, DOT should be easy to experiment with and extend, and therefore its soundness proof needs to be easy to modify.
This paper presents a simple and modular proof strategy for reasoning in DOT. The strategy separates reasoning about types from other concerns. It is centred around a theorem that connects the full DOT type system to a restricted variant in which the challenges and paradoxes caused by abstract type members are eliminated. Almost all reasoning in the proof is done in the intuitive world of this restricted type system. Once we have the necessary results about types, we observe that the other aspects of DOT are mostly standard and can be incorporated into a soundness proof using familiar techniques known from other calculi.
- Martín Abadi and Luca Cardelli. 1996. A Theory of Objects. Springer. Google ScholarCross Ref
- Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016. The Essence of Dependent Object Types. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday (Lecture Notes in Computer Science), Sam Lindley, Conor McBride, Philip W. Trinder, and Donald Sannella (Eds.), Vol. 9600. Springer, 249–272. DOI: Google ScholarCross Ref
- Nada Amin, Adriaan Moors, and Martin Odersky. 2012. Dependent Object Types. In International Workshop on Foundations of Object-Oriented Languages (FOOL 2012).Google Scholar
- Nada Amin and Tiark Rompf. 2017. Type soundness proofs with definitional interpreters. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 666–679. DOI: Google ScholarDigital Library
- Nada Amin, Tiark Rompf, and Martin Odersky. 2014. Foundations of path-dependent types. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2014, part of SPLASH 2014, Portland, OR, USA, October 20-24, 2014, Andrew P. Black and Todd D. Millstein (Eds.). ACM, 233–249. DOI: Google ScholarDigital Library
- Nada Amin and Ross Tate. 2016. Java and Scala’s type systems are unsound: the existential crisis of null pointers. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, October 30 - November 4, 2016, Eelco Visser and Yannis Smaragdakis (Eds.). ACM, 838–848. DOI: Google ScholarDigital Library
- Dave Clarke, Sophia Drossopoulou, James Noble, and Tobias Wrigstad. 2007. Tribe: a simple virtual class calculus. In Proceedings of the 6th International Conference on Aspect-Oriented Software Development, AOSD 2007, Vancouver, British Columbia, Canada, March 12-16, 2007 (ACM International Conference Proceeding Series), Brian M. Barry and Oege de Moor (Eds.), Vol. 208. ACM, 121–134. DOI: Google ScholarDigital Library
- Vincent Cremet, François Garillot, Sergueï Lenglet, and Martin Odersky. 2006. A Core Calculus for Scala Type Checking. In Mathematical Foundations of Computer Science, 31st International Symposium, Slovakia. Google ScholarDigital Library
- Erik Ernst. 1999. gbeta – a Language with Virtual Attributes, Block Structure, and Propagating, Dynamic Inheritance. Ph.D. Dissertation. Department of Computer Science, University of Aarhus, Århus, Denmark.Google Scholar
- Erik Ernst. 2001. Family Polymorphism. In ECOOP 2001 - Object-Oriented Programming, 15th European Conference, Budapest, Hungary, June 18-22, 2001, Proceedings (Lecture Notes in Computer Science), Jørgen Lindskov Knudsen (Ed.), Vol. 2072. Springer, 303–326. DOI: Google ScholarCross Ref
- Erik Ernst, Klaus Ostermann, and William R. Cook. 2006. A virtual class calculus. In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006, J. Gregory Morrisett and Simon L. Peyton Jones (Eds.). ACM, 270–282. DOI: Google ScholarDigital Library
- Ole Lehrmann Madsen and Birger Møller-Pedersen. 1989. Virtual Classes: A Powerful Mechanism in Object-Oriented Programming. In Conference on Object-Oriented Programming: Systems, Languages, and Applications (OOPSLA’89), New Orleans, Louisiana, USA, October 1-6, 1989, Proceedings., George Bosworth (Ed.). ACM, 397–406. DOI: Google ScholarDigital Library
- Adriaan Moors, Frank Piessens, and Martin Odersky. 2008. Safe type-level abstraction in Scala. In International Workshop on Foundations of Object-Oriented Languages (FOOL 2008).Google Scholar
- Martin Odersky, Vincent Cremet, Christine Röckl, and Matthias Zenger. 2003. A Nominal Theory of Objects with Dependent Types. In ECOOP 2003 - Object-Oriented Programming, 17th European Conference, Darmstadt, Germany, July 21-25, 2003, Proceedings (Lecture Notes in Computer Science), Luca Cardelli (Ed.), Vol. 2743. Springer, 201–224. DOI: Google ScholarCross Ref
- Martin Odersky and Matthias Zenger. 2005. Scalable component abstractions. In Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2005, October 16-20, 2005, San Diego, CA, USA, Ralph E. Johnson and Richard P. Gabriel (Eds.). ACM, 41–57. DOI: Google ScholarDigital Library
- Leo Osvald, Grégory M. Essertel, Xilun Wu, Lilliam I. González Alayón, and Tiark Rompf. 2016. Gentrification gone too far? affordable 2nd-class values for fun and (co-)effect. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, October 30 - November 4, 2016, Eelco Visser and Yannis Smaragdakis (Eds.). ACM, 234–251. DOI: Google ScholarDigital Library
- Benjamin C. Pierce. 2002. Types and programming languages. MIT Press.Google ScholarDigital Library
- Marianna Rapoport and Ondřej Lhoták. 2017. Mutable WadlerFest DOT. In Proceedings of the 19th Workshop on Formal Techniques for Java-like Programs (FTFJP’17). ACM, New York, NY, USA, Article 7, 6 pages. DOI: Google ScholarDigital Library
- Tiark Rompf and Nada Amin. 2016. Type soundness for dependent object types (DOT). In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, October 30 - November 4, 2016, Eelco Visser and Yannis Smaragdakis (Eds.). ACM, 624–641. DOI: Google ScholarDigital Library
- Alceste Scalas and Nobuko Yoshida. 2016. Lightweight Session Programming in Scala. In 30th European Conference on Object-Oriented Programming, ECOOP 2016, July 18-22, 2016, Rome, Italy (LIPIcs), Shriram Krishnamurthi and Benjamin S. Lerner (Eds.), Vol. 56. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 21:1–21:28. DOI: Google ScholarCross Ref
- Andrew K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. Inf. Comput. 115, 1 (1994), 38–94. Google ScholarDigital Library
Index Terms
- A simple soundness proof for dependent object types
Recommendations
Type soundness for dependent object types (DOT)
OOPSLA 2016: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and ApplicationsScala’s type system unifies aspects of ML modules, object- oriented, and functional programming. The Dependent Object Types (DOT) family of calculi has been proposed as a new theoretic foundation for Scala and similar expressive languages. ...
Dependent object types with implicit functions
Scala '19: Proceedings of the Tenth ACM SIGPLAN Symposium on ScalaDOT (Dependent Object Types) is an object calculus with path-dependent types and abstract type members, developed to serve as a theoretical foundation for the Scala programming language. As yet, DOT does not model all of Scala's features, but a small ...
Type soundness for dependent object types (DOT)
OOPSLA '16Scala’s type system unifies aspects of ML modules, object- oriented, and functional programming. The Dependent Object Types (DOT) family of calculi has been proposed as a new theoretic foundation for Scala and similar expressive languages. ...
Comments