research-article

Open access

A path to DOT: formalizing fully path-dependent types

Authors:

Marianna Rapoport,

Ondřej LhotákAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 3, Issue OOPSLA

Article No.: 145, Pages 1 - 29

https://doi.org/10.1145/3360571

Published: 10 October 2019 Publication History

Abstract

The Dependent Object Types (DOT) calculus aims to formalize the Scala programming language with a focus on path-dependent types — types such as x.a₁… a_n.T that depend on the runtime value of a path x.a₁… a_n to an object. Unfortunately, existing formulations of DOT can model only types of the form x.A which depend on variables rather than general paths. This restriction makes it impossible to model nested module dependencies. Nesting small components inside larger ones is a necessary ingredient of a modular, scalable language. DOT’s variable restriction thus undermines its ability to fully formalize a variety of programming-language features including Scala’s module system, family polymorphism, and covariant specialization.

This paper presents the pDOT calculus, which generalizes DOT to support types that depend on paths of arbitrary length, as well as singleton types to track path equality. We show that naive approaches to add paths to DOT make it inherently unsound, and present necessary conditions for such a calculus to be sound. We discuss the key changes necessary to adapt the techniques of the DOT soundness proofs so that they can be applied to pDOT. Our paper comes with a Coq-mechanized type-safety proof of pDOT. With support for paths of arbitrary length, pDOT can realize DOT’s full potential for formalizing Scala-like calculi.

Supplementary Material

a145-rapoport (a145-rapoport.webm)

Presentation at OOPSLA '19

Download
91.69 MB

References

[1]

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. 249–272.

[2]

Nada Amin, Adriaan Moors, and Martin Odersky. 2012. Dependent Object Types. In International Workshop on Foundations of Object-Oriented Languages (FOOL 2012).

[3]

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. 666–679.

Digital Library

[4]

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. 233–249.

Digital Library

[5]

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. 838–848.

Digital Library

[6]

Kim B. Bruce, Martin Odersky, and Philip Wadler. 1998. A Statically Safe Alternative to Virtual Types. In ECOOP’98 -Object-Oriented Programming, 12th European Conference. 523–549.

[7]

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. 121–134.

Digital Library

[8]

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.

Digital Library

[9]

Scala Documentation. 2018. Paths. Retrieved February 26, 2019 from https://www.scala- lang.org/files/archive/spec/2.11/03-types.html#paths

[10]

Derek Dreyer, Karl Crary, and Robert Harper. 2003. A type system for higher-order modules. In Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New Orleans, Louisisana, USA, January 15-17, 2003. 236–249.

Digital Library

[11]

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.

[12]

Erik Ernst. 2001. Family Polymorphism. In ECOOP 2001 - Object-Oriented Programming, 15th European Conference, Budapest, Hungary, June 18-22, 2001, Proceedings. 303–326.

[13]

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. 270–282.

[14]

Robert Harper and Mark Lillibridge. 1994. A Type-Theoretic Approach to Higher-Order Modules with Sharing. In Conference Record of POPL’94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, USA, January 17-21, 1994. 123–137.

Digital Library

[15]

Jaemin Hong, Jihyeok Park, and Sukyoung Ryu. 2018. Path Dependent Types with Path-equality. In Proceedings of the 9th ACM SIGPLAN International Symposium on Scala (Scala 2018). ACM, 35–39.

Digital Library

[16]

Jason Hu and Ondrej Lhoták. 2019. Undecidability of D <: and Its Decidable Fragments. CoRR abs/1908.05294 (2019). http://arxiv.org/abs/1908.05294

[17]

Ifaz Kabir and Ondřej Lhoták. 2018. κDOT: scaling DOT with mutation and constructors. In Proceedings of the 9th ACM SIGPLAN International Symposium on Scala. ACM, 40–50.

Digital Library

[18]

Xavier Leroy. 1994. Manifest Types, Modules, and Separate Compilation. In Conference Record of POPL’94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, USA, January 17-21, 1994. 109–122.

Digital Library

[19]

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. 397–406.

[20]

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).

[21]

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. 201–224.

[22]

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. 41–57.

Digital Library

[23]

Benjamin C. Pierce. 1992. Bounded Quantification is Undecidable. In Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Albuquerque, New Mexico, USA, January 19-22, 1992. 305–315.

Digital Library

[24]

Marianna Rapoport, Ifaz Kabir, Paul He, and Ondřej Lhoták. 2017. A simple soundness proof for dependent object types. PACMPL 1, OOPSLA (2017), 46:1–46:27.

Digital Library

[25]

Marianna Rapoport and Ondrej Lhoták. 2019. A Path To DOT: Formalizing Fully Path-Dependent Types. CoRR abs/1904.07298 (2019). http://arxiv.org/abs/1904.07298

[26]

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. 624–641.

Digital Library

[27]

Andreas Rossberg. 2018. 1ML — Core and modules united. Journal of Functional Programming 28 (2018), e22.

[28]

Andreas Rossberg and Derek Dreyer. 2013. Mixin’ Up the ML Module System. ACM Trans. Program. Lang. Syst. 35, 1 (2013), 2:1–2:84.

Digital Library

[29]

Andreas Rossberg, Claudio V. Russo, and Derek Dreyer. 2014. F-ing modules. J. Funct. Program. 24, 5 (2014), 529–607.

[30]

Christopher A. Stone and Robert Harper. 2006. Extensional equivalence and singleton types. ACM Trans. Comput. Log. 7, 4 (2006), 676–722.

Digital Library

[31]

Fei Wang and Tiark Rompf. 2017. Towards Strong Normalization for Dependent Object Types (DOT). In 31st European Conference on Object-Oriented Programming, ECOOP 2017, June 19-23, 2017, Barcelona, Spain. 27:1–27:25.

[32]

Andrew K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. Inf. Comput. 115, 1 (1994), 38–94.

Digital Library

Cited By

Xu YBoruch-Gruszecki AOdersky M(2024)Degrees of Separation: A Flexible Type System for Safe ConcurrencyProceedings of the ACM on Programming Languages10.1145/36498538:OOPSLA1(1181-1207)Online publication date: 29-Apr-2024
https://doi.org/10.1145/3649853
Lee ESatheeskumar KLhoták OTomb A(2023)Dependency-Free Capture TrackingProceedings of the 25th ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3605156.3606454(39-43)Online publication date: 18-Jul-2023
https://dl.acm.org/doi/10.1145/3605156.3606454
Melicher DXu AZhao VPotanin AAldrich J(2022)Bounded Abstract EffectsACM Transactions on Programming Languages and Systems10.1145/349242744:1(1-48)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3492427
Show More Cited By

Index Terms

A path to DOT: formalizing fully path-dependent types
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

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 ...
Path dependent types with path-equality
Scala 2018: Proceedings of the 9th ACM SIGPLAN International Symposium on Scala

While the Scala type system provides expressive features like objects with type members, the lack of equality checking between path-dependent types prohibits some programming idioms. One such an example is abstract domain combinators in implementing ...
Type soundness for dependent object types (DOT)
OOPSLA 2016: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications

Scala’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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 3, Issue OOPSLA

October 2019

2077 pages

EISSN:2475-1421

DOI:10.1145/3366395

Issue’s Table of Contents

Copyright © 2019 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: 10 October 2019

Published in PACMPL Volume 3, Issue OOPSLA

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Natural Sciences and Engineering Research Council of Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
530
Total Downloads

Downloads (Last 12 months)151
Downloads (Last 6 weeks)20

Reflects downloads up to 19 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Xu YBoruch-Gruszecki AOdersky M(2024)Degrees of Separation: A Flexible Type System for Safe ConcurrencyProceedings of the ACM on Programming Languages10.1145/36498538:OOPSLA1(1181-1207)Online publication date: 29-Apr-2024
https://doi.org/10.1145/3649853
Lee ESatheeskumar KLhoták OTomb A(2023)Dependency-Free Capture TrackingProceedings of the 25th ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3605156.3606454(39-43)Online publication date: 18-Jul-2023
https://dl.acm.org/doi/10.1145/3605156.3606454
Melicher DXu AZhao VPotanin AAldrich J(2022)Bounded Abstract EffectsACM Transactions on Programming Languages and Systems10.1145/349242744:1(1-48)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3492427
Martres GRichard-Foy JDoeraene S(2021)Pathless Scala: a calculus for the rest of ScalaProceedings of the 12th ACM SIGPLAN International Symposium on Scala10.1145/3486610.3486894(12-21)Online publication date: 17-Oct-2021
https://dl.acm.org/doi/10.1145/3486610.3486894
Xu YBoruch-Gruszecki AParreaux LRichard-Foy JDoeraene S(2021)Implementing path-dependent GADT reasoning for Scala 3Proceedings of the 12th ACM SIGPLAN International Symposium on Scala10.1145/3486610.3486892(22-32)Online publication date: 17-Oct-2021
https://dl.acm.org/doi/10.1145/3486610.3486892
Stucki SGiarrusso P(2021)A theory of higher-order subtyping with type intervalsProceedings of the ACM on Programming Languages10.1145/34735745:ICFP(1-30)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473574
Kabir ILi YLhoták O(2020)ιDOT: a DOT calculus with object initializationProceedings of the ACM on Programming Languages10.1145/34282764:OOPSLA(1-28)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428276
Laddad SSen KErwig MGray J(2020)Fluid quotes: metaprogramming across abstraction boundaries with dependent typesProceedings of the 19th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3425898.3426953(98-110)Online publication date: 16-Nov-2020
https://dl.acm.org/doi/10.1145/3425898.3426953
Giarrusso PStefanesco LTimany ABirkedal LKrebbers R(2020)Scala step-by-step: soundness for DOT with step-indexed logical relations in IrisProceedings of the ACM on Programming Languages10.1145/34089964:ICFP(1-29)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408996
BRACHTHÄUSER JSCHUSTER POSTERMANN K(2020)Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in ScalaJournal of Functional Programming10.1017/S095679682000002730Online publication date: 31-Mar-2020
https://doi.org/10.1017/S0956796820000027

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Figures

Tables

Media

View Issue’s Table of Contents