Hat Day 2006
5 October 2006 at the University of Kent
Hat Day was an informal gathering of people interested in the development of the Haskell tracer Hat and related tracing and debugging methods for functional languages. We had six talks and additonal discussions on various topic. We only had very few brief exercises of applying tracing tools to various programs because of the limited time.
We decided to produce a new release of Hat soon, preferably by the beginning of 2007. We also intend to have another Hat Day probably around late spring / summer 2007.
Participants: Neil Mitchell, Colin Runciman and Malcolm Wallace from the University of York, Henrik Nilsson from the University of Nottingham, Olaf Chitil, Thomas Davie and Yong Luo from the University of Kent. Also Stefan Kahrs and Nik Sultana from the University of Kent.
Abstracts of Talks
Windows and WIMP
Neil Mitchell, University of York
A Windows port of Hat has been developed and tested since the last Hat
Day. This talk covers some of the issues that were encountered, how these
issues were overcome and which obstacles remain for the future.
In addition to the standard console applications available with Hat,
progress has been made towards a graphical user interface. This HatGui
tool is written in Haskell in a cross-platform manner, is already in the
source tree for Hat, and work continues on it.
Thomas Davie, University of Kent
Structure & Properties of the Augmented Redex Trail
Olaf Chitil, University of Kent
The tracer Hat records in a detailed trace the computation of a program written in the lazy functional language Haskell. The trace can then be viewed in various ways to support program comprehension and debugging. The trace was named the augmented redex trail
An ART explicitly represents many details of a computation of a functional program. An ART is a graph so that it can share subexpressions. Sharing is the key both to a space efficient trace structure without redundancies and closeness to the implementations of functional languages.
Our model of the ART captures its essential properties and allows formal reasoning.
We abstract from the details of how Hat generates an ART by defining our model of the ART through direct graph rewriting on the ART. The one essential difference to standard graph rewriting of functional language implementations is that ART rewriting does not overwrite a redex with its reduct, but adds the reduct to the graph, keeping the reduct and thus the computation history. The ART only grows and old parts are never modified.
A canonical naming scheme for graph nodes avoids unnecessary distinctions between isomorphic graphs, is independent of the evaluation order and encodes useful information about the structure of the graph (Colin suggested using the letters f,a,r instead of l,r,t in the node names).
Although the trace is a graph whose structure is independent of any rewriting strategy, we define the trace inductively, thus giving us a powerful method for proving its properties.
- Structure and Properties of Traces for Functional Programs. Olaf Chitil and Yong Luo. 3rd International Workshop on Term Graph Rewriting, Termgraph 2006, to appear in ENTCS, 2006.
Correctness of Algorithmic Debugging
Yong Luo, University of Kent
In non-strict functional programming languages such as Haskell, it happens
often that some parts of a program are not evaluated because their values
are not demanded. In practice, those unevaluated parts are often replaced by
a placeholder (e.g. _) in order to keep the trace size smaller. In the
process of algorithmic debugging, one needs to answer several questions in
order to locate a program fault. Replacing unevaluated parts makes these
questions shorter and semantically clearer. We present a
formal model of tracing in which unevaluated parts are replaced by the
symbol _. The most important property, the correctness of algorithmic
debugging, is proved.
Malcolm Wallace, University of York
W-Hat is the working name for a generalised query language over Hat
traces. We start by defining simple trace operators that, given a trace
node, can navigate around to other nodes, and extract labelled
information. We build on this in steps: first, by introducing a
comprehension notation that enables one to select certain nodes from the
trace as starting points for the navigational operations. This leads to
the need for certain meta-operations over the trace, such as various
forms of equivalence relation: equality of labels, node equality,
structural equality, equality of results. Other kinds of query-level
operation include "as long as possible", and simple combining forms for
the results of tests.
It turns out that expressing even simple queries in this little
operational language is tedious, so we define a pattern-matching layer
as a means to simplify the user's task, which translates in the obvious
way to to an underlying query.
With this apparatus, many of the existing viewing tools (hat-observe,
hat-stack, hat-trail, hat-detect) can now be easily re-expressed as very
small programs utilising W-Hat. However, rather than merely replicating
the existing tools, we want to demonstrate new levels of expressiveness.
One obvious idea is to permit any arbitrary Haskell computation to be
written over the values drawn from the trace. This requires a
representation change - trace values must become ordinary Haskell values
(but one must also account for undefined portions of structures). It is
also possible that after computing over such values, one may wish to
regain their traced nature, to once again navigate explicitly through
Outstanding problems include: whether it is possible to determine an
optimal order for traversing the trace, based on the exact nature of a
query; and whether the dropping of trace structures to ordinary data
structures is sufficient, or if instead the computation over structures
must be lifted to deal with traced data.
SmallCheck and Hpc in relation to Hat
Colin Runciman, University of York
SmallCheck is a library for lightweight testing in Haskell, similar
in spirit to QuickCheck but testing properties for all small values
instead of for some random values. As counter-examples reported by
QuickCheck are minimal they are ideal candidates for investigation by
tracing. Question: can we construct 'dual' executables that run
untraced property tests until a counter-example is found, then
immediately switch to traced execution for a repeated computation of the
failing test only?
Hpc is a tool-kit for recording and reporting Haskell program
coverage. Like Hat, it is based on a source-to-source transformation,
re-using infrastructure such as the hat-trans parser and
pretty-printer. Also like Hat, Hpc involves the run-time production of
an auxiliary record of computation but this record is deliberately very
simple -- just an array of binary switches. The interpretation of
switch values is communicated between transformation-time and
viewing-time by index-files for programs and modules. Question: have we
missed opportunities to improve the performance of Hat by generating
index files -- either at transformation time or between run-time and