Programming Languages (cs.PL)

  • Aug 21 2017 cs.PL arXiv:1708.05437v1
    PDF
    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 typing and subtyping rules, as opposed to algorithmic. 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$_{<:}$. We prove these relations sound and decidable. They are not complete with respect to the original D$_{<:}$ rules.