A Theory of Tracing Pure Functional Programs

Olaf Chitil and Yong Luo

EPSRC grant EP/C516605/1
1 April 2005 - 31 October 2007

Tracing Functional Programs

Tracing enables the programmer to see how different parts of the program cause a computation to perform its observed input/output actions. Tracing is used primarily for debugging, that is, for localising the faulty program part that causes an undesirable observable behaviour. For declarative languages new tracing methods that are different from, and arguably more powerful than, conventional methods for imperative languages have been developed. These methods take advantage of the purity of declarative languages, that is, explicit data flow and absence of side effects. Functional languages are particularly suitable for these methods, because they have simple and well-studied semantics, and lazy functional languages are the most widely used completely pure programming languages. There now exist several tracing systems for the standard lazy functional language Haskell, demonstrating the practical viability of different tracing methods.

Challenges and Aims

During the development of the Haskell tracer Hat, which combines the tracing methods of several preceding systems, numerous inconsistencies, anomalies and defects in all existing systems came to light. Experience in using the systems suggests desirable generalisations that are hard to realise. At the root of both problems is that the development of the existing systems was implementation-driven, guided mostly by intuition. There is a surprising lack of theoretical foundations for tracing. To resolve the inconsistencies and enable generalisations, this project aims at establishing a semantical theory of tracing pure functional programs, both eager and lazy, that describes different methods, links information gained from tracing to specific program parts, and establishes the correctness of fault location algorithms.

Relevance

The results of this project will provide the basis for the improvement of existing tracing systems and the construction of new, more powerful tracing systems for declarative languages. All programmers using these systems will profit from the systems' support for the development of correct software. The availability of powerful tracing tools will also strengthen the case for using declarative programming languages more widely.

Talks

Papers

Hat Days