Parametric Subtyping for Structural Parametric Polymorphism

TL;DR

This paper introduces a decidable and expressive fragment of structural subtyping called parametric subtyping, which leverages parametricity for type constructors to handle recursive types.

Contribution

It defines parametric subtyping for recursive type constructors, proving its correctness and implementing an effective decision procedure.

Findings

Parametric subtyping generalizes rigid subtyping.

The decision procedure is effective and correct.

Implementation is available online.

Abstract

We study the interaction of structural subtyping with parametric polymorphism and recursively defined type constructors. Although structural subtyping is undecidable in this setting, we describe a notion of parametricity for type constructors and then exploit it to define parametric subtyping, a conceptually simple, decidable, and expressive fragment of structural subtyping that strictly generalizes rigid subtyping. We present and prove correct an effective saturation-based decision procedure for parametric subtyping, demonstrating its applicability using a variety of examples. We also provide an implementation of this decision procedure online.