The Essence of Dependent Object Types

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
Keywords:
Laboratories:




 Record created 2016-01-22, last modified 2018-09-13

Postprint:
Download fulltextPDF
External link:
Download fulltextURL
Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)