# Hat publications

- Olaf Chitil
  A Theory of Tracing Pure Functional Programs

  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

- Koen Claessen, Colin Runciman, Olaf Chitil, John Hughes, Malcolm Wallace:
  Testing and Tracing Lazy Functional Programs using QuickCheck and Hat
  4th Summer School in Advanced Functional Programming, Oxford, August 2002, 40 pages (final version in Springer LNCS 2638, 2003).

  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)

- Olaf Chitil, Colin Runciman, Malcolm Wallace:
  Transforming Haskell for Tracing
  in International Workshop on the Implementation of Functional Languages, Madrid, Sept 2002, 17 pages, final version to appear in Springer LNCS series, 2003.

  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)

- Olaf Chitil:
  A Semantics for Tracing
  in Draft Proceedings of the 13th International Workshop on Implementation of Functional Languages, IFL 2001, Älvsjö, Sweden, 24-26 September 2001, editors Thomas Arts and Markus Mohnen, Ericsson Computer Science Laboratory, pp. 249-254.

  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)

- Thorsten Brehm:
  A Toolkit for Multi-View Tracing of Haskell Programs
  Master's Thesis, RWTH Aachen, 2001, 130 pages.
  Postscript (225 KB)

- Malcolm Wallace, Olaf Chitil, Thorsten Brehm, and Colin Runciman:
  Multiple-View Tracing for Haskell: a New Hat
  Proceedings of the Haskell Workshop 2001, Firenze, Italy. FInal version to appear in ENTCS.

  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)

- Olaf Chitil, Colin Runciman and Malcolm Wallace:
  Freja, Hat and Hood - A Comparative Evaluation of Three Systems for Tracing and Debugging Lazy Functional Programs
  Markus Mohnen and Pieter Koopman (eds): Proceedings of the 12th International Workshop on Implementation of Functional Languages, Aachen, Germany, September 4th - 7th 2000, LNCS 2011, 2001, pp. 176-193.

  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)

- Colin Runciman:
  Advanced Redex Trails: Project Proposal
  (.html)

Publications not directly about Hat, but produced as a spin-off result of the Hat project:

- Olaf Chitil:
  Compositional Explanation of Types and Algorithmic Debugging of Type Errors
  Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP'01), Firenze, Italy, 3-5 September 2001, pp. 193--204.

  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)

- Olaf Chitil:
  Pretty Printing with Lazy Dequeues
  Proceedings of the 2001 ACM SIGPLAN Haskell Workshop, Firenze, Italy, Universiteit Utrecht UU-CS-2001-23, 2 September 2001, pp. 183-201.

  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)

Hat is the successor of an earlier project and builds on its work which is described in the following publications:

- Jan Sparud and Colin Runciman:
  Tracing Lazy Functional Computations Using Redex Trails
  (PLILP'97) (.ps.gz)

- Jan Sparud and Colin Runciman:
  Complete and Partial Redex Trails of Functional Computations
  (IFL'97) (.ps.gz)

- Jan Sparud:
  Tracing and Debugging Lazy Functional Computations
  (PhD thesis, 1999) (.ps.gz)

This page last modified: 28 June 2005
York Functional Programming Group