A theory of higher-order subtyping with type intervals

What is it about?

The Scala programming language has a powerful and expressive type system. This helps programmers write flexible and highly reusable code without giving up the benefits of static typing. Static types provide both a human-readable high-level specification for the code and allow the compiler to catch many potential bugs. But while programmers enjoy the expressiveness of Scala's type system, it complicates the job of compiler developers. Like any piece of complex software, the Scala compiler is itself prone to bugs. One way to reduce the number of such bugs is to create a mathematical model of the type system and prove its correctness. The model can then be used as a blueprint for implementing the compiler. Previous work has developed such a model, called the calculus of Dependent Object Types (DOT). But that model did not cover the full Scala type language. In particular, it was missing a blueprint for Scala's so-called Higher-Kinded (HK) types. This paper develops a formal mathematical model of HK types and proves that it has the crucial property of "type safety" and other desirable properties. The corresponding mathematical proofs are complex. We have therefore formalized and checked them using a special software called a "proof assistant" (the Agda interactive theorem prover).

Featured Image

Photo by Rich Tervet on Unsplash

Photo by Rich Tervet on Unsplash

Why is it important?

Our work helps increase the confidence in the correctness of the Scala type system and its implementation. It has lead to the identification of bugs in the Scala 3 compiler and suggests directions for improving the compiler's design. Ultimately, this should lead to more robust tooling for Scala and languages with similar type systems.