Space-Efficient Latent Contracts

TL;DR

This paper introduces a space-efficient contract monitoring framework for higher-order contracts, especially focusing on latent contracts with dependencies, ensuring tail recursion and bounded space usage in many cases.

Contribution

It adapts existing space-efficient semantics to latent contracts with dependencies, providing guarantees when no dependency is used and a flexible framework otherwise.

Findings

Guarantees space efficiency without dependencies

Provides a case-by-case approach for dependency-involving programs

Restores tail recursion and bounds space complexity

Abstract

Standard higher-order contract monitoring breaks tail recursion and leads to space leaks that can change a program's asymptotic complexity; space-efficiency restores tail recursion and bounds the amount of space used by contracts. Space-efficient contract monitoring for contracts enforcing simple type disciplines (a/k/a gradual typing) is well studied. Prior work establishes a space-efficient semantics for manifest contracts without dependency (Greenberg 2015); we adapt that work to a latent calculus with dependency. We guarantee space efficiency when no dependency is used; we cannot generally guarantee space efficiency when dependency is used, but instead offer a framework for making such programs space efficient on a case-by-case basis.