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.

Displaying Functions

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 (ART). 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.

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.

W-Hat, Hat-Query

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 the graph.

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 viewing time?