Title: Towards Algorithmic Typing for DOT,
Abstract: 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.