Parametric Subtyping for Structural Parametric Polymorphism
Recursive types, generics (sometimes called parametric polymorphism), and subtyping are all essential features for modern programming languages across numerous paradigms. However, structural subtyping is undecidable in the presence of recursive types and generics. In our POPL 2024 paper and its accompanying implementation, we propose a reconstruction of the interaction between recursive types, generics, and structural subtyping from first principles. We present a notion of parametricity for type constructors that forms the basis of a suitable, decidable fragment of structural subtyping, which we call parametric subtyping.
