Space-Efficient Manifest Contracts

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 the design space with three different space-efficient manifest calculi. We examine the diverse correctness criteria for contract semantics; we conclude with a coercion-based language whose contracts enjoy (galactically) bounded, sound space consumption—they are observationally equivalent to the standard, space-inefficient semantics. This is an extended version of Greenberg [2015], with a great deal of material that does not appear in the conference paper: an exploration of the design space with two other space-efficient calculi and complete proofs.