2021/03/31 by Yao Li, Li-yao Xia, Stephanie Weirich
Computer Science · #Computation #Feature (linguistics) #Formal Methods in Verification #Functional programming #Lazy evaluation #Logic, programming, and type systems #Monad (category theory) #Parallel Computing and Optimization Techniques #Principle of compositionality #Simple (philosophy) #Stateful firewall #cs.PL
paper · pdf · doi:10.1145/3473585
28 pages, accepted by ICFP'21
openalex created_date 2021/03/29 · arxiv created 2021/07/02 · arxiv updated 2021/07/05 · openalex publication_date 2021/08/19 · openalex updated_date 2026/08/06
Lazy evaluation is a powerful tool for functional programmers. It enables the concise expression of on-demand computation and a form of compositionality not available under other evaluation strategies. However, the stateful nature of lazy evaluation makes it hard to analyze a program's computational cost, either informally or formally. In this work, we present a novel and simple framework for formally reasoning about lazy computation costs based on a recent model of lazy evaluation: clairvoyant call-by-value. The key feature of our framework is its simplicity, as expressed by our definition of the clairvoyance monad. This monad is both simple to define (around 20 lines of Coq) and simple to reason about. We show that this monad can be effectively used to mechanically reason about the computational cost of lazy functional programs written in Coq.