
TL;DR
This paper presents a method to achieve sound space-efficient manifest contracts by restructuring contract checks into coercions, preventing duplication, and maintaining observable behavior.
Contribution
It introduces a coercion-based approach that ensures space efficiency for manifest contracts with strong predicates, addressing an open problem in gradual typing.
Findings
Achieves bounded, sound space consumption for manifest contracts
Defines a framework with three space-efficient calculi
Demonstrates observational equivalence to standard semantics
Abstract
The standard algorithm for higher-order contract checking can lead to unbounded space consumption and can destroy tail recursion, altering a program's asymptotic space complexity. While space efficiency for gradual types---contracts mediating untyped and typed code---is well studied, sound space efficiency for manifest contracts---contracts that check stronger properties than simple types, e.g., "is a natural" instead of "is an integer"---remains an open problem. We show how to achieve sound space efficiency for manifest contracts with strong predicate contracts. The essential trick is breaking the contract checking down into coercions: structured, blame-annotated lists of checks. By carefully preventing duplicate coercions from appearing, we can restore space efficiency while keeping the same observable behavior. Along the way, we define a framework for space efficiency, traversing…
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.
