"Spiking Your Caches",
Kevin Hammond, Geoffrey L. Burn and Denis B. Howe
Abstract
Despite recent advances, predicting the performance of functional programs on real machines remains something of a black art. This paper reports on one particularly unexpected set of results where small variations in the dynamic heap settings occasionally gave rise to significant differences in CPU performance. These performance spikes can be traced to the direct-mapped cache of the machine being benchmarked, the widely-used Sun Sparcstation 1.
"Lazy Depth-First Search and Linear Graph
Algorithms in Haskell",
David J. King and John Launchbury
[Extended version of the paper in GFP '93]
Abstract
Depth-first search is the key to a wide variety of graph algorithms. In this paper we explore the implementation of depth first search in a lazy functional language. For the first time in such languages we obtain a linear-time implementation. But we go further. Unlike traditional imperative presentations, algorithms are constructed from individual components, which may be reused to create new algorithms. Furthermore, the style of program is quite amenable to formal proof, which we exemplify through a calculational-style proof of a strongly-connected components algorithm.
"Lazy Functional State Threads",
John Launchbury and Simon L. Peyton Jones
Abstract
Some algorithms make critical internal use of updatable state, even though their external specification is purely functional. Based on earlier work on monads, we present a way of securely encapsulating stateful computations that manipulate multiple, named, mutable objects, in the context of a non-strict, purely-functional language.
The security of the encapsulation is assured by the type system, using parametricity. Intriguingly, this parametricity requires the provision of a (single) constant with a rank-2 polymorphic type.
[A shorter version of this paper appears in the Proceedings of the ACM Conference on Programming Languages Design and Implementation (PLDI), Orlando, June 1994.]
"Type Classes in Haskell",
Cordelia V. Hall, Kevin Hammond,
Simon L. Peyton Jones and Philip L. Wadler
[Extended version of the paper in ESOP '94]
Abstract
This paper defines a set of type inference rules for resolving overloading introduced by type classes. Programs including type classes are transformed into ones which may be typed by the Hindley-Milner inference rules. In contrast to other work on type classes, the rules presented here relate directly to user programs. An innovative aspect of this work is the use of second-order lambda calculus to record type information in the program.
"PERs from Projections for Binding-Time Analysis",
Kei Davis
[Proc. PEPM '94]
Abstract
Launchbury has shown that first-order projection-based binding-time analysis is genuinely useful in partial evaluation. There have been three notable generalisations of his analysis technique to higher order. The first, due to Mogensen, lacked a formal basis. The second, Hunt and Sands', used structures strictly more general that projections, namely partial equivalence relations (PERs). The third, ours, involved a complex construction that gave rise to impractically large abstract domains. This paper presents a technique free of these shortcomings: it is simple, entirely projection-based, satisfies a formal correctness condition, and gives rise to reasonably small abstract domains. Though the technique is cast in terms of projections, there is also an interpretation in terms of PERs. The principal limitation of the technique is the restriction to monomorphic typing.
"A Typed Operational Semantics based on
Grammatical Characterisation of an Abstract
Machine",
Robin Popplestone
Abstract
In computation, we often want to represent finite sequences of objects. Classically, a set of finite sequences of tokens drawn from an alphabet is a language, and may be characterised by a grammar. It would seem natural therefore to use grammars as a richer way of specifying types, simply by deciding that tokens can be the objects from which a type is built. For example, List ({Int*String}) is the type of all lists in which short integers alternate with strings, using {a} for the Kleene-closure of a.
However, one's enthusiasm for this approach might be tempered by the realisatuon that some questions about some grammars are not effective- ly computable. A crucial capability required for this work is the ability to divide one grammar exactly by another. Exact division is an extension of the concept of division found in Hopcroft and Ullman and characterises, at the type-level of abstraction, the acquisition of arguments by a function.
This approach is valuable for any language or system in which stacking operations are explicit, including the Forth, POP-11 and PostScript lang- uages, and the Poplog multi-language environment. It has been applied experimentally to the development of a type-checker for the POP-11 language.
"Specifying Types by Grammars: A Polymorphic
Static Type Checker Operating at a Stack
Machine Level",
Robin Popplestone
Abstract
It is important for computer languages to represent sequences of entities. A set of sequences is a formal language, commonly specified by one of the various kinds of grammar known to theorists. Thus it is natural to approach the problem of specifying which sequences can occur in given circumstances in a program (for example as the value of a variable) by defining the concept of sequence type using grammars.
This report describes an experimental type-checker for the POP-11 language, which, being an open-stack language like Forth or PostScript, has acted as a forcing-frame for the grammatical approach. Functions are regarded as parsing the stack for their arguments and generating their results. Both arguments and results belong to languages specified by a grammar.
Declarations are made quite independent of the main program text, using a single macro "declare". The types of most procedures have to be declared, but that of their local values is inferred.
Parametric polymorphism and overloading are supported. For example, the checker will typecheck a definition of "applist", overloaded with two signatures which encompass many of the uses of that versatile procedure.
"Abstract Interpretation of Polymorphic
Higher-Order Functions",
Gebreselassie Baraki,
[Thesis submitted for the degree of PhD]
Partial Abstract
This thesis describes several abstract interpret- ations of polymorphic functions. In all the interpretations, information about any instance of a polymorphic function is obtained from the smallest, thus avoiding the computation of the instance directly. This is useful in the case of recursive functions, because it avoids the expensive computation of finding fixed points of functionals corresponding to complex instances.
"Using Overloading to Express Distinctions
Between Evaluators",
Cordelia V. Hall
[To appear in Information Processing Letters]
Abstract
Evaluators, also called ``interpreters'', play a variety of roles in the study of programming languages. Given this, it's surprising that we don't have a better framework for developing evaluators and specifying their relationship to each other. This paper shows that type classes in Haskell provide an excellent framework for exploring relationships between evaluators, using abstract interpretation as a motivating example.
"Between Functions and Relations
in Calculating Programs"
Graham M. Hutton
[Thesis submitted for the degree of PhD]
Abstract
This thesis is about the calculational approach to programming, in which one derives programs from specifications. One such calculational paradigm is Ruby, the relational calculus developed by Jones and Sheeran for describing and designing circuits. We identify two shortcomings with derivations made using Ruby. The first is that the notion of a program being an implementation of a specification has never been made precise. The second is to do with types. Fundamental to the use of type information in deriving programs is the idea of having types as special kinds of programs. InRuby, types are partial equivalence relations (pers). Unfortunately, manipulating some formulae involving types has proved difficult within Ruby. In particular, the preconditions of the `induction' laws that are much used within program derivation often work out to be assertions about types; such assertions have typically been verified either by informal arguments or by using predicate calculus, rather than by applying algebraic laws from Ruby.
In this thesis we address both of the shortcomings noted above. We define what it means for a Ruby program to be an implementation, by introducing the notion of a causal relation, and the network denoted by a Ruby program. A relation is causal if it is functional in some structural way, but not necessarily from domain to range; a network captures the connectivity between the primitive relations in a program. Moreover, we present an interpreter for Ruby programs that are implementations. Our technique for verifying an assertion about types is to first express it using operators that give the best left and right types for a relation, and then verify this assertion by using algebraic properties of these operators.
"Generation garbage collection for Haskell"
Patrick M. Sansom and Simon L. Peyton Jones
[Extended version of paper in FPCA '93]
Abstract
This paper examines the use of generational garbage collection techniques for a lazy implementation of a non-strict functional language. Detailed measurements which demonstrate that a generational garbage collector can substantially out-perform non-generational collectors, despite the frequency of write operations in the underlying implementation, are presented.
Our measurements are taken from a state-of-the-art compiled implementation for Haskell, running substantial benchmark programs. We make measurements of dynamic properties (such as object lifetimes) which affect generational collectors, study their interaction with a simple generational scheme, make direct performance comparisons with simpler collectors, and quantify the interaction with a paging system.
The generational collector is demonstrably superior. At least for our benchmarks, it reduces the net storage management overhead, and it allows larger programs to be run on a given machine before thrashing ensues.
[A summary version of this report is published in the Proceedings of the ACM conference on Functional Programming Languages and Computer Architecture, Copenhagen, June 1993. This technical report contains the complete set of performance results for all of the benchmark programs.]
"Processing Transactions on GRIP",
Gert Akerholt, Kevin Hammond, Simon Peyton Jones
and Phil Trinder.
Abstract
The GRIP architecture allows efficient execution of functional programs on a multi-processor built from standard hardware components. State-of-the-art compilation techniques are combined with sophisticated runtime resource-control to give good parallel performance. This paper reports the results of running GRIP on an application which is apparently unsuited to the basic functional model: a database transaction manager incorporating updates as well as lookup transactions. The results obtained show good relative speedups for GRIP, with real performance advantages over the same application executing on sequential machines.
"Imperative Functional Programming",
Simon Peyton Jones and Philip Wadler.
Abstract
We present a new model, based on monads, for performing input/output in a non-strict, purely functional language. It is composable, extensible, efficient, requires no extensions to the type system, and extends smoothly to incorporate mixed-language working and in-place array updates.
"Higher-Order Binding-Time Analysis",
Kei Davis
[Proc. PEPM '94]
Abstract
The partial evaluation process requires a binding-time analysis. Binding-time analysis seeks to determine which parts of a program's result is determined when some part of the input is known. Domain projections provide a very general way to encode a description of which parts of a data structure are static (known), and which are dynamic (not static). For first-order functional languages Launchbury has developed an abstract interpretation technique for binding-time analysis in which the basic abstract value is a projection. Unfortunately this technique does not generalise easily to higher-order languages. This paper develops such a generalisation: a projection-based abstract interpretation suitable for higher-order binding-time analysis.
The principal limitation of our technique is the restriction to monomorphic typing.
"A Futurebus interface from off-the-shelf parts",
Simon Peyton Jones and Mark Hardie.
Abstract
As part of the GRIP project, we have designed a Futurebus interface using off-the-shelf parts. We describe our implementation, which is unusual in its use of fully asynchronous finite state machines. Based on this experience, we draw some lessons for designers using Futurebus.
Last changed: $Date: 1996/05/13 10:11:01 $