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.