The Essence of Dependent Object Types

Amin, Nada; Grütter, Karl Samuel; Odersky, Martin; Rompf, Tiark; Stucki, Sandro

doi:10.1007/978-3-319-30936-1_14

The Essence of Dependent Object Types

Amin, Nada ; Grütter, Karl Samuel ; Odersky, Martin ; Rompf, Tiark[...]

Focusing on path-dependent types, the paper develops foundations for Scala from first principles. Starting from a simple calculus D-<: of dependent functions, it adds records, intersections and recursion to arrive at DOT, a calculus for dependent object types. The paper shows an encoding of System F with subtyping in D-<: and demonstrates the expressiveness of DOT by modeling a range of Scala constructs in it.

Editor(s):

Lindley, Sam
McBride, Conor
Trinder, Phil
Sannella, Don

Published in:

A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, 249-272

Presented at:

WadlerFest 2016, Edinburgh, UK, April 11-12, 2016

Year:

2016

Publisher:

Springer International Publishing

ISBN:

978-3-319-30936-1