Amin, Nada
Rompf, Tiark
Odersky, Martin
Foundations of Path-Dependent Types
Acm Sigplan Notices
Acm Sigplan Notices
Acm Sigplan Notices
Acm Sigplan Notices
17
49
10
Languages
Theory
calculus
objects
dependent types
2014
2014
A scalable programming language is one in which the same concepts can describe small as well as large parts. Towards this goal, Scala unifies concepts from object and module systems. An essential ingredient of this unification is the concept of objects with type members, which can be referenced through path-dependent types. Unfortunately, path-dependent types are not well-understood, and have been a roadblock in grounding the Scala type system on firm theory. We study several calculi for path-dependent types. We present mu DOT which captures the essence - DOT stands for Dependent Object Types. We explore the design space bottom-up, teasing apart inherent from accidental complexities, while fully mechanizing our models at each step. Even in this simple setting, many interesting patterns arise from the interaction of structural and nominal features. Whereas our simple calculus enjoys many desirable and intuitive properties, we demonstrate that the theory gets much more complicated once we add another Scala feature, type refinement, or extend the subtyping relation to a lattice. We discuss possible remedies and trade-offs in modeling type systems for Scala-like languages.
Assoc Computing Machinery
0362-1340
Acm Sigplan Notices
Journal Articles
10.1145/2660193.2660216