Space-Efficient Latent Contracts
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.
Cite
@article{arxiv.1604.02474,
title = {Space-Efficient Latent Contracts},
author = {Michael Greenberg},
journal= {arXiv preprint arXiv:1604.02474},
year = {2017}
}
Comments
In post-proceedings of TFP 2016. Second revision extends to dependency; third fixes typos in the abstract; fourth is long version of what will be the final TFP publication