The name has also been used for Steinitz numbers, or for numbers of the form 10 4n , both otherwise unconnected with the super-naturals described here.2 Defined in Numeric.Natural, a basic Haskell library. 3 In Haskell, symbolic data constructors, which are infix by default, must start with a colon.

This paper presents Speculate, a tool that automatically conjectures laws involving conditional equations and inequalities about Haskell functions. Speculate enumerates expressions involving a given collection of Haskell functions, testing to separate those expressions into apparent equivalence classes. Expressions in the same equivalence class are used to conjecture equations. Representative expressions of different equivalence classes are used to conjecture conditional equations and inequalities. Speculate uses lightweight equational reasoning based on term rewriting to discard redundant laws and to avoid needless testing. Several applications demonstrate the effectiveness of Speculate.

This paper presents FitSpec, a tool providing automated assistance in the task of refining sets of test properties for Haskell functions. FitSpec tests mutant variations of functions under test against a given property set, recording any surviving mutants that pass all tests. The number of surviving mutants and any smallest survivor are presented to the user. A surviving mutant indicates incompleteness of the property set, prompting the user to amend a property or to add a new one, making the property set stronger. Based on the same test results, FitSpec also provides conjectures in the form of equivalences and implications between property subsets. These conjectures help the user to identify minimal core subsets of properties and so to reduce the cost of future property-based testing.

Using static analysis techniques compilers for lazy functional languages can be used to identify parts of a program that can be legitimately evaluated in parallel and ensure that those expressions are executed concurrently with the main thread of execution. These techniques can produce improvements in the runtime performance of a program, but are limited by the static analyses’ poor prediction of runtime performance. This paper outlines the development of a system that uses iterative profile-directed improvement in addition to well-studied static analysis techniques. This allows us to achieve higher performance gains than through static analysis alone.

Systematic concurrency testing (SCT) is an approach to testing potentially nondeterministic concurrent programs. SCT avoids potentially unrepeatable results that may arise from unit testing concurrent programs. It seems to have received little attention from Haskell programmers. This paper introduces a generalisation of Haskell's concurrency abstraction in the form of typeclasses, and a library for testing concurrent programs. A number of examples are provided, some of which come from pre-existing packages.

Abstract A new version of a special-purpose processor for running lazy functional programs is presented. This processor – the Reduceron – exploits parallel memories and dynamic analyses to increase evaluation speed, and is implemented using reconfigurable hardware. Compared to a more conventional functional language implementation targeting a standard RISC processor running on the same reconfigurable hardware, the Reduceron offers a significant improvement in run-time performance.

The leading implementations of graph reduction all target conventional processors designed for low-level imperative execution. In this paper, we present a processor specially designed to perform graph-reduction. Our processor -- the Reduceron -- is implemented using off-the-shelf reconfigurable hardware. We highlight the low-level parallelism present in sequential graph reduction, and show how parallel memories and dynamic analyses are used in the Reduceron to achieve an average reduction rate of 0.55 function applications per clock-cycle.

We describe a transformation which takes a higher-order program, and produces an equivalent first-order program. Unlike Reynolds-style defunctionalisation, it does not introduce any new data types, and the results are more amenable to subsequent analysis operations. We can use our method to improve the results of existing analysis operations, including strictness analysis, pattern-match safety and termination checking. Our transformation is implemented, and works on a Core language to which Haskell programs can be reduced. Our method cannot always succeed in removing all functional values, but in practice is remarkably successful.

We describe an automated analysis of Haskell 98 programs to check statically that, despite the possible use of partial (or nonexhaustive) pattern matching, no pattern-match failure can occur. Our method is an iterative backward analysis using a novel form of pattern-constraint to represent sets of data values. The analysis is defined for a core first-order language to which Haskell 98 programs are reduced. Our analysis tool has been successfully applied to a range of programs, and our techniques seem to scale well. Throughout the paper, methods are represented much as we have implemented them in practice, again in Haskell.

This paper describes two Haskell libraries for property-based testing. Following the lead of QuickCheck, these testing libraries SmallCheck and Lazy SmallCheck also use type-based generators to obtain test-sets of finite values for which properties are checked, and report any counter-examples found. But instead of using a sample of randomly generated values they test properties for all values up to some limiting depth, progressively increasing this limit. The paper explains the design and implementation of both libraries and evaluates them in comparison with each other and with QuickCheck.

We describe the design, implementation and use of HPC, a tool-kit to record and display Haskell Program Coverage. HPC includes tools that instrument Haskell programs to record program coverage, run instrumented programs, and display information derived from coverage data in various ways.

Generic traversals over recursive data structures are often referred to as boilerplate code. The definitions of functions involving such traversals may repeat very similar patterns, but with variations for different data types and different functionality. Libraries of operations abstracting away boilerplate code typically rely on elaborate types to make operations generic. The motivating observation for this paper is that most traversals have value-specific behaviour for just one type. We present the design of a new library exploiting this assumption. Our library allows concise expression of traversals with competitive performance.

We develop a Haskell library for functional-logic programming, motivated by the implementation of Wired, a relational embedded domain-specific language for describing and analysing digital circuits at the VLSI-layout level. Compared to a previous library for logic programming by Claessen and Ljunglöf, we support residuation, easier creation of logical data types, and pattern matching. We discuss other applications of our library, including test-data generation, and various extensions, including lazy narrowing.

The pipeline model in visualization has evolved from a conceptual model of data processing into a widely used architecture for implementing visualization systems. In the process, a number of capabilities have been introduced, including streaming of data in chunks, distributed pipelines, and demand-driven processing. Visualization systems have invariably built on stateful programming technologies, and these capabilities have had to be implemented explicitly within the lower layers of a complex hierarchy of services. The good news for developers is that applications built on top of this hierarchy can access these capabilities without concern for how they are implemented. The bad news is that by freezing capabilities into low-level services expressive power and flexibility is lost. In this paper we express visualization systems in a programming language that more naturally supports this kind of processing model. Lazy functional languages support fine-grained demand-driven processing, a natural form of streaming, and pipeline-like function composition for assembling applications. The technology thus appears well suited to visualization applications. Using surface extraction algorithms as illustrative examples, and the lazy functional language Haskell, we argue the benefits of clear and concise expression combined with fine-grained, demand-driven computation. Just as visualization provides insight into data, functional abstraction provides new insight into visualization.

Every designer of a new data structure wants to know how well it performs in comparison with others. But finding, coding and testing applications as benchmarks can be tedious and time-consuming. Besides, how a benchmark uses a data structure may considerably affect its apparent efficiency, so the choice of applications may bias the results. We address these problems by developing a tool for inductive benchmarking . This tool, Auburn , can generate benchmarks across a wide distribution of uses. We precisely define ‘the use of a data structure’, upon which we build the core algorithms of Auburn: how to generate a benchmark from a description of use, and how to extract a description of use from an application. We then apply inductive classification techniques to obtain decision trees for the choice between competing data structures. We test Auburn by benchmarking several implementations of three common data structures: queues, random-access lists and heaps. These and other results show Auburn to be a useful and accurate tool, but they also reveal some limitations of the approach.

Identifying the source of space faults in functional programs is hard. The problem is compounded as space usage can vary enormously from one implementation to another. We use a term-graph rewriting model to describe evaluators with explicit space usage. Given descriptions for two evaluators E1 and E2, if E1 never has asymptotically worse space usage than E2, we can use a bisimulation-like proof method to prove it. Conversely, if E1 is leakier than E2, we characterise a class of computations that expose the difference between them.

We present two complementary approaches to writing XML document-processing applications in a functional language.In the first approach, the generic tree structure of XML documents is used as the basis for the design of a library of combinators for generic processing: selection, generation, and transformation of XML trees.The second approach is to use a type-translation framework for treating XML document type definitions (DTDs) as declarations of algebraic data types, and a derivation of the corresponding functions for reading and writing documents as typed values in Haskell.

For the programmer, storage media are usually assumed to have a minimum atomic unit of transfer of one byte. However, sometimes it is useful to have an even finer storage granularity of one bit, for instance in order to compress data.This paper describes an API in the lazy functional language Haskell for treating storage media as arbitrary-length streams of bits without byte-alignment constraints. So far as possible, storage media are treated uniformly. In particular, bit-stream memory and binary files share the same API -- a new and useful abstraction over memory management and file management. This uniformity of access leads to a novel technique for lazy random-access to files in a purely functional manner. We also describe a technique for automatically deriving compressed binary representations of user-defined data structures, whose operations provide both in-heap data compression and convenient high-level binary I/O.Of many possible applications, we illustrate the processing of Huffman-encoded image data, and a bibliographic information system which uses lazy B-trees for efficient storage management.

The popular method of enumerating the primes is the Sieve of Eratosthenes . It can be programmed very neatly in a lazy functional language, but runs rather slowly. A little-known alternative method is the Wheel Sieve , originally formulated as a fast imperative algorithm for obtaining all primes up to a given limit, assuming destructive access to a bit-array. This article describes functional variants of the wheel sieve that enumerate all primes as a lazy list.

The context for this paper is functional computation by graph reduction. Our overall aim is more efficient use of memory. The specific topic is the detection of dormant cells in the live graph --- those retained in heap memory though not actually playing a useful role in computation. We describe a profiler that can identify heap consumption by such 'useless' cells. Unlike heap profilers based on traversals of the live heap, this profiler works by examining cells postmortem. The new profiler has revealed a surprisingly large proportion of 'useless' cells, even in some programs that previously seemed space-efficient such as the boot-strapping Haskell compiler nhc.

Abstract First-generation heap profilers for lazy functional languages have proved to be effective tools for locating some kinds of space faults, but in other cases they cannot provide sufficient information to solve the problem. This paper describes the design, implementation and use of a new profiler that goes beyond the two-dimensional ‘who produces what’ view of heap cells to provide information about their more dynamic and structural attributes. Specifically, the new profiler can distinguish between cells according to their eventual lifetime , or on the basis of the closure retainers by virtue of which they remain part of the live heap. A bootstrapping Haskell compiler (nhc) hosts the implementation: among examples of the profiler's use we include self-application to nhc. Another example is the original heap-profiling case study clausify, which now consumes even less memory and is much faster.

Abstract Functional languages do not usually mesh well with embedded applications because of the need for special I/O device‐handling. By introducing a process model to a language, however, it becomes possible to express register‐level device operations and interrupts in a modular manner. This paper describes such a model, its implementation by extension to the Gofer programming system, and examples of its use. Performance results indicate that even this prototype interpretive system is adequate for small applications. The major gain of using a functional language is the ease with which abstraction can be layered over low‐level detail, improving both the readability of code and its tractability.

Abstract Most programming environments for functional languages offer a single tool used to evaluate programs – either a batch compiler or an interpreter with a read-eval-print loop. This paper presents a programming environment that supports not only evaluation, but also a range of other programming activities including transformation. The environment is designed to encourage working in an incremental and exploratory style, avoiding constraints on the order in which things must be done yet guarenteeing security. What has already been done towards the development of a program automatically persists, as does information about what has yet to be done. For instance, new laws can be introduced as conjectures and used in program transformation, but full details of proof obligations and dependencies are maintained. The paper outlines the functional language supported by the environment, and uses an extended example to illustrate program construction, execution, tracing, modification and transformation.

Abstract We describe the design, implementation and use of a new kind of profiling tool that yields valuable information about the memory use of lazy functional programs. The tool has two parts: a modified functional language implementation which generates profiling information during the execution of programs, and a separate program which converts this information to graphical form. With the aid of profile graphs, one can make alterations to a functional program which dramatically reduce its space consumption. We demonstrate this in the case of a genuine example - the first to which the tool was applied - for which the results are strikingly successful.

Abstract Polymorphic types are labels classifying both ( a ) defined components in a library and ( b ) contexts of free variables in partially written programs. It is proposed to help programmers make better use of software libraries by providing a system that, given ( b ), identifies candidates from ( a ) with matching types. Assuming at first that matching means unifying (i.e. having a common instance), efficient ways of implementing such a retrieval system are discussed and its likely effectiveness based on a quantitative study of currently available libraries is indicated. The applicative instance relation between types, which captures some intuitions about generalization/specialization is then introduced, and its use as the basis of a more flexible system is discussed.