Dependent Object Types

We propose a new type-theoretic foundation of Scala and languages like it: the Dependent Object Types (DOT) calculus. DOT models Scala’s path-dependent types, abstract type members and its mixture of nominal and structural typing through the use of refinement types. The core formalism makes no attempt to model inheritance and mixin composition. DOT normalizes Scala’s type system by unifying the constructs for type members and by providing classical intersection and union types which simplify greatest lower bound and least upper bound computations. In this paper, we present the DOT calculus, both formally and informally. We also discuss our work-in-progress to prove typesafety of the calculus.

Presented at:
19th International Workshop on Foundations of Object-Oriented Languages, Tucson, Arizona, USA, October 22, 2012

 Record created 2013-01-10, last modified 2018-03-17

Publisher's version:
Download fulltextPDF
External link:
Download fulltextURL
Rate this document:

Rate this document:
(Not yet reviewed)