TY - JOUR
T1 - Space-efficient manifest contracts
AU - Greenberg, Michael
PY - 2015/1
Y1 - 2015/1
N2 - 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.
AB - 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.
KW - Coercions
KW - Contracts
KW - Function proxy
KW - Pre- and post-conditions
KW - Space efficiency
UR - http://www.scopus.com/inward/record.url?scp=84950316954&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84950316954&partnerID=8YFLogxK
U2 - 10.1145/2676726.2676967
DO - 10.1145/2676726.2676967
M3 - Article
AN - SCOPUS:84950316954
SN - 1523-2867
VL - 50
SP - 181
EP - 194
JO - ACM SIGPLAN Notices
JF - ACM SIGPLAN Notices
IS - 1
ER -