Haskelite: A Tracing Interpreter Based on a Pattern-Matching Calculus

TL;DR

This work addresses the difficulty of obtaining textbook-style evaluation traces for lazy Haskell by introducing Haskelite, a web-based tracing interpreter for a subset of Haskell grounded in Kahl's pattern-matching calculus. It defines a small core language, lambdaPMC, and develops both a big-step semantics and a small-step abstract machine to enable step-by-step tracing of lazy evaluations. The approach is demonstrated with concrete translations and examples, highlighting how overlapping patterns, as-patterns, boolean guards, and local bindings are handled, and how the implementation supports educational tracing. The tool aims to complement GHC/GHCi by providing transparent, equationally grounded execution traces that learners can study and reason about.

Abstract

Many Haskell textbooks explain the evaluation of pure functional programs as a process of stepwise rewriting using equations. However, usual implementation techniques perform program transformations that make producing the corresponding tracing evaluations difficult. This paper presents a tracing interpreter for a subset of Haskell based on the pattern matching calculus of Kahl. We start from a big-step semantics in the style of Launchbury and develop a small-step semantics in the style of Sestoft's machines. This machine is used in the implementation of a step-by-step educational interpreter. We also discuss some implementation decisions and present illustrative examples.

Figures (3)

• Figure 1: Evaluation trace for insert 3 [1,2,4].
• Figure 2: Evaluation trace for head (isort [3,2,1]).
• Figure 3: Syntax of $\lambda\textsf{PMC}$.