Towards Algorithmic Typing for DOT

TL;DR

This paper investigates a restricted, decidable version of the D<: calculus from Scala's DOT type system, introducing step relations for algorithmic typing and subtyping, and proving their soundness and decidability.

Contribution

It proposes a simplified D<: calculus with decidable typechecking, along with step relations for algorithmic typing and subtyping, inspired by Scala's compiler approach.

Findings

Proved the soundness of step typing and subtyping relations.

Established the decidability of the proposed relations.

Highlighted the trade-off between expressiveness and decidability.

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.