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.