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


Publié dans:
Acm Sigplan Notices, 49, 10, 233-249
Année
2014
Publisher:
New York, Assoc Computing Machinery
ISSN:
0362-1340
Mots-clefs:
Laboratoires:




 Notice créée le 2015-04-13, modifiée le 2018-12-03


Évaluer ce document:

Rate this document:
1
2
3
 
(Pas encore évalué)