Space-Efficient Manifest Contracts

作者：Greenberg Michael^*

来源：ACM Sigplan Notices, 2015, 50(1): 181-194.

DOI：10.1145/2676726.2676967

• contracts
• pre- and post-conditions
• function proxy
• coercions
• space efficiency

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.

• 出版日期2015-1