The Spineless Tagless G-machine is an abstract machine designed to support non-strict higher-order functional languages. This presentation of the machine falls into three parts. Firstly, we give a general discussion of the design issues involved in implementing non-strict functional languages. Next, we present the STG language, an austere but recognizably-functional language, which as well as a denotational meaning has a well-defined operational semantics. The STG language is the ‘abstract machine code’ for the Spineless Tagless G-machine. Lastly, we discuss the mapping of the STG language onto stock hardware. The success of an abstract machine model depends largely on how efficient this mapping can be made, though this topic is often relegated to a short section. Instead, we give a detailed discussion of the design issues and the choices we have made. Our principal target is the C language, treating the C compiler as a portable assembler.

We present an on-line (run-time) algorithm that manages the granularity of parallel functional programs. The algorithm exploits useful parallelism when it exists, and ignores ineffective parallelism in programs that produce many small tasks. The idea is to balance the amount of local work with the cost of distributing the work. This is achieved by ensuring that for every parallel task spawned, an amount of work that equals the cost of the spawn is performed locally. We analyse several cases and compare the algorithm to the optimal execution. In most cases the algorithm competes well with the optimal algorithm, even though the optimal algorithm has information about the future evolution of the computation that is not available to the on-line algorithm. This is quite remarkable considering we have chosen extreme cases that have contradicting optimal executions. Moreover, we show that no other on-line algorithm can be consistently better than it. We also present experimental results that demonstrate the effectiveness of the algorithm.

We present a new static system which reconstructs the types, regions and effects of expressions in an implicitly typed functional language that supports imperative operations on reference values. Just as types structurally abstract collections of concrete values, regions represent sets of possibly aliased reference values and effects represent approximations of the imperative behaviour on regions.

We introduce a static semantics for inferring types, regions and effects, and prove that it is consistent with respect to the dynamic semantics of the language. We present a reconstruction algorithm that computes the types and effects of expressions, and assigns regions to reference values. We prove the correctness of the reconstruction algorithm with respect to the static semantics. Finally, we discuss potential applications of our system to automatic stack allocation and parallel code generation.

Some extensions of the basic formalism of stream processing functions are useful to specify complex structures such as operating systems. In this paper we give the foundations of higher order stream processing functions. These are functions which send and accept not only messages representing atomic data, but also complex elements such as functions. Some special notations are introduced for the specification and manipulation of such functions. A representation of time is outlined, which enables us to model time dependent behaviour. Finally, we demonstrate how characteristic operating system structures can be modelled by timed higher order stream processing functions.

In a functional program, a simple random number generator may generate a lazy list of random numbers. This is fine when the random numbers are consumed sequentially at a single point in the program. However, things are more complicated in a program where random numbers are used at many locations, such as in a large simulation. The programmer should not need to worry about providing separate generators with a unique seed at each point where random numbers are used. At the same time, the programmer should not need to coordinate the use of a single stream of random numbers in many parts of the program, which can be particularly difficult with lazy evaluation or parallel processing.

We discuss several techniques for distributing random numbers to various parts of a program, and some methods of allowing different program components to evaluate random numbers locally. We then propose a new approach in which a random number sequence can be split at a random point to produce a pair of random number sequences that can be used independently at different points in the computation.

The approach can also be used in distributed procedural programs, where it is desirable to avoid dealing with a single source of random numbers. The approach has the added advantage of producing repeatable results, as might be needed in debugging, for example.

In the last two decades, category theory has become one of the main tools for the denotational investigation of programming languages. Taking advantage of the algebraic nature of the categorical semantics, and of the rewriting systems it suggests, it is possible to use these denotational descriptions as a base for research into more operational aspects of programming languages.

This approach proves to be particularly interesting in the study and the definition of environment machines for functional languages. The reason is that category theory offers a simple and uniform language for handling terms and environments (substitutions), and for studying their interaction (through application).

Several examples of known machines are discussed, among which the Categorical Abstract Machine of Cousineau et al. (1987) and Krivine's machine. Moreover, as an example of the power and fruitfulness of this approach, we define two original categorical machines. The first one is a variant of the CAM implementing a λ-calculus with both call-by-value and call-by-name as parameters passing modes. The second one is a variant of Krivine's machine performing complete reduction of λ-terms.

The essential part of abstract interpretation is to build a machine-representable abstract domain expressing interesting properties about the possible states reached by a program at runtime. Many techniques have been developed which assume that one knows in advance the class of properties that are of interest. There are cases however when there are no a priori indications about the 'best' abstract properties to use. We introduce a new framework that enables non-unique representations of abstract program properties to be used, and expose a method, called dynamic partitioning, that allows the dynamic determination of interesting abstract domains using data structures built over simpler domains. Finally, we show how dynamic partitioning can be used to compute non-trivial approximations of functions over infinite domains and give an application to the computation of minimal function graphs.

The integration of functional and logic programming languages has been a topic of great interest in the last decade. Many proposals have been made, yet none is completely satisfactory especially in the context of higher order functions and lazy evaluation. This paper addresses these shortcomings via a new approach: domain theory as a common basis for functional and logic programming. Our integrated language remains essentially within the functional paradigm. The logic programming capability is provided by set abstraction (via Zermelo-Frankel set notation), using the Herbrand universe as a set abstraction generator, but for efficiency reasons our proposed evaluation procedure treats this generator's enumeration parameter as a logical variable. The language is defined in terms of (computable) domain-theoretic constructions and primitives, using the lower (or angelic) powerdomain to model the set abstraction facility. The result is a simple, elegant and purely declarative language that successfully combines the most important features of both pure functional programming and pure Horn logic programming. Referential transparency with respect to the underlying mathematical model is maintained throughout. An implicitly correct operational semantics is obtained by direct execution of the denotational semantic definition, modified suitably to permit logical variables whenever the Herbrand universe is being generated within a set abstraction. Completeness of the operational semantics requires a form of parallel evaluation, rather than the more familiar left-most rule.

In combinator parsing, the text of parsers resembles BNF notation. We present the basic method, and a number of extensions. We address the special problems presented by white-space, and parsers with separate lexical and syntactic phases. In particular, a combining form for handling the ‘offside rule’ is given. Other extensions to the basic method include an ‘into’ combining form with many useful applications, and a simple means by which combinator parsers can produce more informative error messages.

We present a simple and easy-to-understand explanation of ML type inference and parametric polymorphism within the framework of type monomorphism, as in the first order typed lambda calculus. We prove the equivalence of this system with the standard interpretation using type polymorphism, and extend the equivalence to include polymorphic fixpoints. The monomorphic interpretation gives a purely combinatorial understanding of the type inference problem, and is a classic instance of quantifier elimination, as well as an example of Gentzen-style cut elimination in the framework of the Curry-Howard propositions-as-types analogy.

MetaMorph is a software tool that supports transformation and proof for an equational non-strict functional language. It was developed as a vehicle for research into the synthesis of digital logic, but is equally suitable for reasoning about functional programs. The theorem prover may be used for verifying new reusable transforms and to assist the search for transformation sequences having a constrained goal. The paper provides an overview of all aspects of the project, and a brief discussion of its application to hardware.

This paper compares three different sparse matrix representations in Miranda for solving linear systems of equations: quadtrees, binary trees and run-length encoding. It compares the three data structures in each of two common linear system solvers, Conjugate Gradient and SOR. The test problems used in the paper arise from a simple reservoir model.

We start by giving a compact representation schema for λ-terms, and show how this leads to an exceedingly small and elegant self-interpreter. We then define the notion of a self-reducer, and show how this too can be written as a small λ-term. Both the self-interpreter and the self-reducer are proved correct. We finally give a constructive proof for the second fixed point theorem for the representation schema. All the constructions have been implemented on a computer, and experiments verify their correctness. Timings show that the self-interpreter and self-reducer are quite efficient, being about 35 and 50 times slower than direct execution using a call-by-need reductions strategy

This paper presents a simple framework for performing calculations with the elements of (finite) lattices. A particular feature of this work is the use of type classes to enable the use of overloaded function symbols within a strongly typed language. Previous applications of type classes have been in areas that are of most interest to language implementors. This paper suggests that type classes might also be useful as a general tool in the development of clear and modular programs.

The G-machine (Johnsson, 1987; Peyton Jones, 1987) is a compiled graph reduction machine for lazy functional languages. The G-machine compiler contains many optimizations to improve performance. One set of such optimizations is designed to improve the performance of tail recursive functions. Unfortunately, the abstract machine is subject to a space leak—objects are unnecessarily preserved by the garbage collector. This paper analyses why a particular form of space leak occurs in the G-machine, and presents some ideas for fixing this problem. This phenomena in other abstract machines is also examined briefly.

One can have all the advantages of functional programming – correctness, clarity, simplicity, and flexibility – without any sacrifice in performance, even for a scientifically significant computation on a supercomputer. Therefore, why use Fortran? We demonstrate parity – equality of speed and storage use – between a program generated automatically from a functional specification and a program written by hand in the procedural style. To our knowledge, this demonstration of parity is the first for a program that solves a scientifically significant problem – quasi-linear hyperbolic partial differential equations – on a scientifically interesting supercomputer – the CRAY X-MP. We use pure Lisp, including higher-order functions, to express the functional specification for the PDE solver. We designed this specification for maximal clarity and flexibility, rather than for efficiency. Nevertheless, we obtain a highly efficient program to solve the PDEs: automated program transformations put back the missing efficiency as they produce an executable Fortran program from the specification. The generated Fortran program vectorizes on the CRAY X-MP and runs about 4% faster than a handwritten Fortran program for the same problem. We describe the problem and the specification, and some of the problem-domain-specific and hardware-specific transformations that we use to obtain the high-efficiency program.

A closed λ-term E is called an enumerator if

Here ⋀0 is the set of closed λ-terms,. is the set of natural numbers and the ⌜n⌝ are the Church's numerals λfx.fnx. Such an E is called reducing if, moreover

An ingenious recursion theoretic proof by Statman will be presented, showing that every enumerator is reducing. I do not know any direct proof.

In this paper we show that it is possible to implement a symmetric set of finite-list operations efficiently; the set is symmetric in the sense that lists can be manipulated at either end. We derive the definitions of these operations from their specifications by calculation. The operations have O(1) time complexity, provided that we content ourselves with, so-called, amortized efficiency, instead of worst-case efficiency