Abstract

A Theory of Tracing Pure Functional Programs

Tracing enables us to see how different parts of a program cause a computation to perform its observable input/output actions. Thus tracing supports understanding how a program works and locating the source of runtime errors. For declarative languages tracing methods that are different from, and arguable 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 Haskell, demonstrating the practical viability of different tracing methods. However, combining different methods and generalising them further proves hard to do and many anomalies and defects in existing systems have come to light. To overcome these problems we need simple models of the tracing systems. We need a theoretical foundation for tracing. It is the aim of an EPSRC project starting right now to provide this foundation.

In the talk I will describe several tracing methods. I continue with a number of problems and shortcomings that have come to light. Finally I will outline the semantical theory that we intend to establish. The theory will describe both strict and non-strict languages and prove the correctness of various fault location algorithms.