Foundations of Path-Dependent Types
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 muDOT 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.
|Foundations of Path-Dependent Types (oopsla2014-amin.pdf)||1.27MiB|
Thu 23 OctDisplayed time zone: Tijuana, Baja California change
10:30 - 12:00
Type SystemsOOPSLA at Salon E
Chair(s): Ravi Chugh University of Chicago
|Rate Types for Stream Programs|
Thomas W. Bartenstein SUNY Binghamton, Yu David Liu State University of New York (SUNY) BinghamtonLink to publication File Attached
|Foundations of Path-Dependent Types|
Nada Amin EPFL, Tiark Rompf Purdue & Oracle Labs, Martin Odersky Ecole Polytechnique Federale de LausanneLink to publication File Attached
|Confined Gradual Typing|
Esteban Allende , Johan Fabry University of Chile, Ronald Garcia University of British Columbia, Éric Tanter University of ChileLink to publication
|Refactoring Java Generics by Inferring Wildcards, In Practice|
John Altidor University of Massachusetts, Yannis Smaragdakis University of AthensLink to publication File Attached