Space-Efficient Manifest Contracts

TL;DR

This paper presents a method to achieve sound space-efficient manifest contracts by restructuring contract checks into coercions, preventing duplication, and maintaining observable behavior.

Contribution

It introduces a coercion-based approach that ensures space efficiency for manifest contracts with strong predicates, addressing an open problem in gradual typing.

Findings

Achieves bounded, sound space consumption for manifest contracts

Defines a framework with three space-efficient calculi

Demonstrates observational equivalence to standard semantics

Abstract

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.