The interaction of contracts and laziness

Markus Degen, Peter Thiemann, and Stefan Wehr

Higher-Order and Symbolic Computation, 25:85-125, 2012.

Abstract

Contract monitoring for strict higher-order functional languages has an intuitive meaning, an established theoretical basis, and a standard implementation. For lazy functional languages, the situation is less clear-cut. There is no agreed-upon intended meaning or theory, and there are competing implementations with subtle semantic differences.

This paper proposes meaning preservation and completeness as formally defined properties for evaluating implementations of contract monitoring. Both properties have definitions that can be checked by straightforward inductive proof. A survey of existing suggestions for lazy contract systems reveals that some are meaning preserving, some are complete, and some have neither property. The main result is that contract monitoring for lazy functional languages cannot be complete and meaning preserving at the same time, although each property can be achieved in isolation.

Bibtex

@ARTICLE{DegenThiemannWehr2012HOSC,
  author = {Markus Degen and Peter Thiemann and Stefan Wehr},
  title = {The interaction of contracts and laziness},
  journal = {Higher-Order and Symbolic Computation},
  volume = 25,
  issue = 1,
  year = 2012,
  pages = {85-125},
  publisher = {Springer}
}