
TL;DR
This paper extends the 'Theorems for Free' technique to derive quantitative, cost-related properties of programs from their types, demonstrating a general, principled approach with potential for complex applications like short-cut fusion.
Contribution
It introduces a novel extension of the 'Theorems for Free' technique that enables deriving cost-related statements from types, broadening its applicability beyond extensional semantics.
Findings
Developed a theoretical framework for quantitative theorems from types
Provided example derivations illustrating the technique
Identified potential for applying the method to complex cases like short-cut fusion
Abstract
"Theorems for Free!" (Wadler, FPCA 1989) is a slogan for a technique that allows to derive statements about functions just from their types. So far, the statements considered have always had a purely extensional flavor: statements relating the value semantics of program expressions, but not statements relating their runtime (or other) cost. Here we study an extension of the technique that allows precisely statements of the latter flavor, by deriving quantitative theorems for free. After developing the theory, we walk through a number of example derivations. Probably none of the statements derived in those simple examples will be particularly surprising to most readers, but what is maybe surprising, and at the very least novel, is that there is a general technique for obtaining such results on a quantitative level in a principled way. Moreover, there is good potential to bring that…
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.
