Towards Algorithmic Typing for DOT (Short Paper)
The Dependent Object Types (DOT) calculus formalizes key features of Scala. The D<: calculus is the core of DOT. To date, presentations of D<: have used declarative, as opposed to algorithmic, typing and subtyping rules. Unfortunately, algorithmic typing for full D<: is known to be an undecidable problem.
We explore the design space for a restricted version of D<: that has decidable typechecking. Even in this simplified D<:, algorithmic typing and subtyping are tricky, due to the ``bad bounds'' problem. The Scala compiler bypasses bad bounds at the cost of a loss in expressiveness in its type system. Based on the approach taken in the Scala compiler, we present the Step Typing and Step Subtyping relations for D<:. These relations are sound and decidable. They are not complete with respect to the original D<: typing rules.
|Towards Algorithmic Typing for DOT (slides) (pres.pdf)||252KiB|
Sun 22 OctDisplayed time zone: Tijuana, Baja California change
10:30 - 12:00
TypesScala 2017 at Regency C
Chair(s): Anthony Sloane Macquarie University
|Towards Algorithmic Typing for DOT (Short Paper)|
Abel Nieto University of WaterlooDOI Pre-print File Attached
|The Limitations of Type Classes as Subtyped Implicits (Short Paper)|
Adelbert Chang UnaffiliatedDOI Pre-print
|Rust-Like Borrowing with 2nd-Class Values (Short Paper)|
Leo Osvald Purdue University, USA, Tiark Rompf Purdue UniversityDOI Media Attached