
TL;DR
This paper introduces paranatural category theory, a new branch centered on paranatural transformations, which generalize natural transformations while maintaining composability, enabling advances in parametric polymorphism and type theory modeling.
Contribution
It defines the category of difunctors and paranatural transformations, proves a diYoneda Lemma, and demonstrates applications in parametric polymorphism, (co)inductive types, and type theory models.
Findings
Paranatural transformations precisely capture parametricity.
The diYoneda Lemma provides a new framework for reasoning about (co)algebras.
Paranatural category theory offers novel tools for type theory modeling.
Abstract
We establish and advocate for a novel branch of category theory, centered around strong dinatural transformations (herein known as "paranatural transformations"). Paranatural transformations generalize natural transformations to mixed-variant difunctors, but, unlike other such generalizations, are composable and exceptionally well-behaved. We define the category of difunctors and paranatural transformations, prove a novel "diYoneda Lemma" for this category, and explore some of the category-theoretic implications. We also develop three compelling uses for paranatural category theory: parametric polymorphism, impredicative encodings of (co)inductive types, and difunctor models of type theory. Paranatural transformations capture the essence of parametricity, with their "paranaturality condition" coinciding exactly with the "free theorem" of the corresponding polymorphic type; the…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Homotopy and Cohomology in Algebraic Topology · Computability, Logic, AI Algorithms
