TL;DR
This paper introduces a straightforward method to derive free theorems using dinaturality, simplifying the process and making it more accessible for teaching and mechanized generation.
Contribution
It presents a simple, direct approach to obtain dinaturality-related free theorems from relational parametricity, enhancing clarity and ease of implementation.
Findings
Method is conceptually appealing and easy to control.
Haskell implementation demonstrates practicality.
Simplifies derivation of free theorems using dinaturality.
Abstract
Free theorems are a popular tool in reasoning about parametrically polymorphic code. They are also of instructive use in teaching. Their derivation, though, can be tedious, as it involves unfolding a lot of definitions, then hoping to be able to simplify the resulting logical formula to something nice and short. Even in a mechanised generator it is not easy to get the right heuristics in place to achieve good outcomes. Dinaturality is a categorical abstraction that captures many instances of free theorems. Arguably, its origins are more conceptually involved to explain, though, and generating useful statements from it also has its pitfalls. We present a simple approach for obtaining dinaturality-related free theorems from the standard formulation of relational parametricity in a rather direct way. It is conceptually appealing and easy to control and implement, as the provided Haskell…
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.