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.
Web
link
One motivation for using a functional programming language is that
it is more difficult (or even impossible) to make low-level mistakes,
and it is easier to reason about programs. But even the most advanced
functional programmers are not infallible; they misunderstand the
properties of their own programs, or those of others, and so commit
errors. We therefore aim to provide functional programmers with
tools for testing and tracing programs. In broad terms, testing
means first specifying what behaviour is acceptable in principle,
then finding out whether behaviour in practice matches up to it across
the input space. Tracing means first recording the internal details
of a computation, then examining what is recorded to gain insight, to
check hypotheses or to locate faults. We concentrate on QuickCheck,
a tool for testing Haskell programs, and Hat, a tool for tracing them.
Each tool is useful in its own right, but they are even more useful
in combination: testing using QuickCheck can identify failing cases,
tracing using Hat can reveal the causes of failure.
Postscript (preliminary version) (103 KB)
LNCS abstract and PDF (final version)
Hat is a programmer's tool for generating a trace of a computation of
a Haskell 98 program and viewing such a trace in various different
ways. Applications include program comprehension and debugging.
A new version of Hat uses a stand-alone program transformation to
produce self-tracing Haskell programs. The transformation is small
and works with any Haskell 98 compiler that implements the standard
foreign function interface. We present general techniques for
building compiler independent tools similar to Hat based on program
transformation. We also point out which features of Haskell 98 caused
us particular grief.
Postscript (preliminary version) (84 KB)
We define a small step operational semantics for a core of Haskell. We modify
this semantics to generate traces, specifically Augmented Redex Trails. This
small and direct definition of Augmented Redex Trails shall improve our
understanding of them and shall help to extend them systematically.
Postscript (44 KB)
Different tracing systems for Haskell give different views of a
program at work. In practice, several views are complementary
and can productively be used together. Until now each system has
generated its own trace, containing only the information needed for
its particular view. Here we present the design of a trace that can
serve several views. The trace is generated and written to file as
the computation proceeds. We have implemented both the generation
of the trace and several different viewers.
Postscript (106 KB)
In this paper we compare three systems for tracing and debugging
Haskell programs: Freja, Hat and Hood. We evaluate their usefulness in
practice by applying them to a number of moderately complex programs
in which errors had deliberately been introduced. We identify the
strengths and weaknesses of each system and then form ideas on how
the systems can be improved further.
Postscript (84 KB)
The type systems of most typed functional programming languages
are based on the Hindley-Milner type system. A practical problem
with these type systems is that it is often hard to understand why a
program is not type correct or a function does not have the intended
type. We suggest that at the core of this problem is the difficulty
of explaining why a given expression has a certain type. The type
system is not defined compositionally. We propose to explain types
using a variant of the Hindley-Milner type system that defines a
compositional type explanation graph of principal typings. We describe
how the programmer understands types by interactive navigation through
the explanation graph. Furthermore, the explanation graph can be
the foundation for algorithmic debugging of type errors, that is,
semi-automatic localisation of the source of a type error without
even having to understand the type inference steps. We implemented a
prototype of a tool to explore the usefulness of the proposed methods.
Postscript (139 KB)
There are several Haskell libraries for converting tree structured data
into indented text, but they all make use of some backtracking. Over
twenty years ago Oppen published a more efficient imperative
implementation of a pretty printer without backtracking. We show that
the same efficiency is also obtainable without destructive updates
by developing a similar but purely functional Haskell implementation
with the same complexity bounds. At its heart lie two lazy double
ended queues.
Postscript (138 KB)