000207233 001__ 207233
000207233 005__ 20181203023824.0
000207233 0247_ $$2doi$$a10.1145/2660193.2660216
000207233 022__ $$a0362-1340
000207233 02470 $$2ISI$$a000348907400014
000207233 037__ $$aARTICLE
000207233 245__ $$aFoundations of Path-Dependent Types
000207233 260__ $$aNew York$$bAssoc Computing Machinery$$c2014
000207233 269__ $$a2014
000207233 300__ $$a17
000207233 336__ $$aJournal Articles
000207233 520__ $$aA 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.
000207233 6531_ $$aLanguages
000207233 6531_ $$aTheory
000207233 6531_ $$acalculus
000207233 6531_ $$aobjects
000207233 6531_ $$adependent types
000207233 700__ $$0246589$$aAmin, Nada$$g164625$$uEcole Polytech Fed Lausanne, Lausanne, Switzerland
000207233 700__ $$0243345$$aRompf, Tiark$$g185682$$uEcole Polytech Fed Lausanne, Lausanne, Switzerland
000207233 700__ $$0241835$$aOdersky, Martin$$g126003$$uEcole Polytech Fed Lausanne, Lausanne, Switzerland
000207233 773__ $$j49$$k10$$q233-249$$tAcm Sigplan Notices
000207233 909C0 $$0252187$$pLAMP$$xU10409
000207233 909CO $$ooai:infoscience.tind.io:207233$$pIC$$particle
000207233 917Z8 $$x166927
000207233 937__ $$aEPFL-ARTICLE-207233
000207233 973__ $$aEPFL$$rREVIEWED$$sPUBLISHED
000207233 980__ $$aARTICLE