Space-efficient manifest contracts
From MaRDI portal
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.
Recommendations
Cited in
(11)- Space-efficient latent contracts
- Manifest contracts for datatypes
- An extended account of contract monitoring strategies as patterns of communication
- How to evaluate the performance of gradual type systems
- Blame and coercion: Together again for the first time
- Gradual type theory
- Contracts made manifest
- Stateful manifest contracts
- Contracts made manifest
- Manifest contracts with intersection types
- Type-directed operational semantics for gradual typing
This page was built for publication: Space-efficient manifest contracts
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2819803)
