Parametric Subtyping for Structural Parametric Polymorphism

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 con...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2023-10
Main Authors: DeYoung, Henry, Mordido, Andreia, Pfenning, Frank, Das, Ankush
Format: Article
Language:English
Subjects:
Polymorphism
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422