Research Repository

See what's under the surface

Call-by-need is clairvoyant call-by-value

Hackett, Jennifer; Hutton, Graham


Jennifer Hackett


Call-by-need evaluation, also known as lazy evaluation, provides two key benefits: compositional programming and infinite data. The standard semantics for laziness is Launchbury’s natural semantics, which uses a heap to memoise the results of delayed evaluations. However, the stateful nature of this heap greatly complicates reasoning about the operational behaviour of lazy programs. In this article, we propose an alternative semantics for laziness, clairvoyant evaluation, that replaces the state effect with nondeterminism, and prove this semantics equivalent in a strong sense to the standard semantics. We show how this new semantics greatly simplifies operational reasoning, admitting much simpler proofs of a number of results from the literature, and how it leads to the first denotational cost semantics for lazy evaluation.

Start Date Aug 19, 2019
Publication Date Aug 21, 2019
Publisher Association for Computing Machinery (ACM)
Volume 3
Series Title Proceedings of the ACM on Programming Languages
Institution Citation Hackett, J., & Hutton, G. (2019). Call-by-need is clairvoyant call-by-value. doi:10.1145/3341718
Additional Information Published In: Proceedings of the ACM on Programming Languages, Volume 3, Issue ICFP, Article 114, August 2019.


You might also like

Downloadable Citations