From stack traces to lazy rewriting sequences

Reasoning about misbehaving lazy functional programs can be confusing, particularly for novice programmers. Unfortunately, the complicated nature of laziness also renders most debugging tools ineffective at clarifying this confusion. In this paper, we introduce a new lazy debugging tool for novice programmers, an algebraic stepper that presents computation as a sequence of parallel rewriting steps. Parallel program rewriting represents sharing accurately and enables debugging at the level of source syntax, minimizing the presentation of low-level details or the effects of distorting transformations that are typical for other lazy debuggers. Semantically, our rewriting system represents a compromise between Launchbury's store-based semantics and an axiomatic description of lazy computation as sharing-via-parameters. Finally, we prove the correctness of our tool by showing that the stepper's run-time machinery reconstructs the expected lazy rewriting sequence.