From Stack Traces to Lazy Rewriting Sequences.
Stephen Chang, John Clements, Eli Barzilay, and Matthias Felleisen.
pre-print.

[ PDF ]

Debugging lazy functional programs poses serious challenges. Due to the complicated nature of lazy evaluation, some debugging tools abandon laziness altogether. Other debuggers preserve laziness but present it in a way that may confuse programmers because the focus of evaluation jumps around in a seemingly random manner.

In this paper, we introduce the algebraic program stepper as a new debugging tool for lazy programs. We conjecture that our tool is suitable for clarifying the confusing nature of laziness. Preliminary classroom experiences have confirmed a prototype implementation of the stepper as a useful tool for novice programmers and programmers new to lazy programming.

Mathematically speaking, our stepper renders lazy computations as the standard rewriting sequences of a program rewriting system. Our lazy semantics introduces lazy evaluation as a form of parallel program rewriting. The semantics resembles graph reduction but remains intuitive for programmers because it emphasizes the source syntax. As a syntactic semantics, our rewriting system represents a compromise between Launchbury's store-based semantics and a simple, axiomatic description of lazy computation as sharing-via-parameters. We prove an equivalence between our system and both of these semantics.

The stepper's implementation leverages Racket's continuation marks for stack trace generation. We can therefore exploit existing models of continuation marks and a correctness proof of Racket's eager algebraic stepper to prove the correctness of our lazy stepper.