Parametric Subtyping for Structural Parametric Polymorphism
Programming Languages
2023-10-30 v2 Logic in Computer Science
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.
Cite
@article{arxiv.2307.13661,
title = {Parametric Subtyping for Structural Parametric Polymorphism},
author = {Henry DeYoung and Andreia Mordido and Frank Pfenning and Ankush Das},
journal= {arXiv preprint arXiv:2307.13661},
year = {2023}
}
Comments
36 pages