Skip to main content

Research Repository

Advanced Search

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

Hackett, Jennifer; Hutton, Graham

Authors



Abstract

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.

Citation

Hackett, J., & Hutton, G. (2019). Call-by-need is clairvoyant call-by-value. Proceedings of the ACM on Programming Languages, 3(ICFP), 1-21. https://doi.org/10.1145/3341718

Journal Article Type Article
Conference Name 24th ACM SIGPLAN International Conference on Functional Programming
Start Date Aug 19, 2019
End Date Aug 21, 2019
Acceptance Date Jun 14, 2019
Online Publication Date Aug 21, 2019
Publication Date Aug 21, 2019
Deposit Date Jun 24, 2019
Publicly Available Date Oct 22, 2019
Electronic ISSN 2475-1421
Publisher Association for Computing Machinery (ACM)
Peer Reviewed Peer Reviewed
Volume 3
Issue ICFP
Pages 1-21
DOI https://doi.org/10.1145/3341718
Public URL https://nottingham-repository.worktribe.com/output/2222777
Publisher URL https://dl.acm.org/citation.cfm?doid=3352468.3341718

Files





You might also like



Downloadable Citations