Reasoning about the garden of forking paths

TL;DR

This paper introduces a simple formal framework based on clairvoyant call-by-value to analyze the computational costs of lazy functional programs, facilitating mechanical reasoning in Coq.

Contribution

It presents a novel, easy-to-understand clairvoyance monad for formal cost analysis of lazy evaluation, implemented in Coq.

Findings

Framework effectively models lazy evaluation costs.

Monadic approach simplifies reasoning about lazy programs.

Implementation in Coq demonstrates practical applicability.

Abstract

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.