A Theory of Higher-Order Subtyping with Type Intervals (Extended Version)

TL;DR

This paper introduces $F^omega_{..}$, a theoretical foundation for Scala's higher-kinded types with interval kinds, enhancing type-level computation and subtyping mechanisms.

Contribution

It extends $F^omega_{<:}$ with interval kinds, providing a unified, flexible theory of higher-order subtyping with formal safety and normalization proofs.

Findings

Proves type and kind safety of $F^omega_{..}$

Establishes weak normalization of types

Shows undecidability of subtyping

Abstract

The calculus of Dependent Object Types (DOT) has enabled a more principled and robust implementation of Scala, but its support for type-level computation has proven insufficient. As a remedy, we propose $F^\omega_{..}$, a rigorous theoretical foundation for Scala's higher-kinded types. $F^\omega_{..}$ extends $F^\omega_{<:}$ with interval kinds, which afford a unified treatment of important type- and kind-level abstraction mechanisms found in Scala, such as bounded quantification, bounded operator abstractions, translucent type definitions and first-class subtyping constraints. The result is a flexible and general theory of higher-order subtyping. We prove type and kind safety of $F^\omega_{..}$, as well as weak normalization of types and undecidability of subtyping. All our proofs are mechanized in Agda using a fully syntactic approach based on hereditary substitution.