title: Lessons from the Design of a Standard ML Library

abstract: Abstract We describe the Edinburgh SML Library and draw lessons from its development. These lessons are of two kinds. The first concerns how to use SML to write a library, and shows some of the design choices that have to be considered. Most of the paper concerns this topic. The second kind of lesson concerns ways in which the language hinders the construction of a library. We suggest some changes to the language as a result of this experience, the most important being the addition of higher-order functors. We also suggest that language designers should consider the needs of libraries early on in the design of a language.


venue: jfp

title: Functional Pearls: The Last Tail


title: Efficient Analysis for Realistic Off-Line Partial Evaluation

authors:
Anders Bondorf
Jesper Jørgensen

abstract: Abstract Based on Henglein's efficient binding-time analysis for the lambda calculus (with constants and ‘fix’) (Henglein, 1991), we develop three efficient analyses for use in the preprocessing phase of Similix, a self-applicable partial evaluator for a higher-order subset of Scheme. The analyses developed in this paper are almost-linear in the size of the analysed program. (1) A flow analysis determines possible value flow between lambda-abstractions and function applications and between constructor applications and selector/predicate applications. The flow analysis is not particularly biased towards partial evaluation; the analysis corresponds to the closure analysis of Bondorf (1991b). (2) A (monovariant) binding-time analysis distinguishes static from dynamic values; the analysis treats both higher-order functions and partially static data structures. (3) A new is-used analysis , not present in Bondorf (1991b), finds a non-minimal binding-time annotation which is ‘safe’ in a certain way: a first-order value may only become static if its result is ‘needed’ during specialization; this ‘poor man's generalization’ (Holst, 1988) increases termination of specialization. The three analyses are performed sequentially in the above mentioned order since each depends on results from the previous analyses. The input to all three analyses are constraint sets generated from the program being analysed. The constraints are solved efficiently by a normalizing union/find-based algorithm in almost-linear time. Whenever possible, the constraint sets are partitioned into subsets which are solved in a specific order; this simplifies constraint normalization. The framework elegantly allows expressing both forwards and backwards components of analyses. In particular, the new is-used analysis is of backwards nature. The three constraint normalization algorithms are proved correct (soundness, completeness, termination, existence of a best solution). The analyses have been implemented and integrated in the Similix system. The new analyses are indeed much more efficient than those of Bondorf (1991b); the almost-linear complexity of the new analyses is confirmed by the implementation.


title: Pattern Matching with Abstract Data Types

authors:
F. Warren Burton
Robert D. Cameron

abstract: Abstract Pattern matching in modern functional programming languages is tied to the representation of data. Unfortunately, this is incompatible with the philosophy of abstract data types. Two proposals have been made to generalize pattern matching to a broader class of types. The laws mechanism of Miranda allows pattern matching with non-free algebraic data types. More recently, Wadler proposed the concept of views as a more general solution, making it possible to define arbitrary mappings between a physical implementation and a view supporting pattern matching. Originally, it was intended to include views in the new standard lazy functional programming language Haskell. Laws and views each offer important advantages, particularly with respect to data abstraction. However, if not used with great care, they also introduce serious problems in equational reasoning. As a result, laws have been removed from Miranda and views were not included in the final version of Haskell. We propose a third approach which unifies the laws and views mechanisms while avoiding their problems. Philosophically, we view pattern matching as a bundling of case recognition and component selection functions instead of a method for inverting data construction. This can be achieved by removing the implied equivalence between data constructors and pattern constructors. In practice, we allow automatic mapping into a view but not out of the view. We show that equational reasoning can still be used with the resulting system. In fact, equational reasoning is easier, since there are fewer hidden traps.


title: Deciding Type Isomorphisms in a Type-Assignment Framework

abstract: Abstract This paper provides a formal treatment of isomorphic types for languages equipped with an ML style polymorphic type inference mechanism. The results obtained make less justified the commonplace feeling that (the core of) ML is a subset of second order λ-calculus: we can provide an isomorphism of types that holds in the core ML language, but not in second order λ-calculus. This new isomorphism allows to provide a complete (and decidable) axiomatization of all the types isomorphic in ML style languages, a relevant issue for the type as specifications paradigm in library searches. This work is a very extended version of Di Cosmo (1992): we provide both a thorough theoretical treatment of the topic and describe a practical implementation of a library search system so that the paper can be used as a reference both by those interested in the formal theory of ML style languages, and by those simply concerned with implementation issues. The new isomorphism can also be used to extend the usual ML type-inference algorithm, as suggested by Di Cosmo (1992). Building on that proposal, we introduce a better type-inference algorithm that behaves well in the presence of non-functional primitives like references and exceptions. The algorithm described here has been implemented easily as a variation to the Caml-Light 0.4 system.


title: Extended Natural Semantics

abstract: Abstract We extend the definition of natural semantics to include simply typed λ-terms, instead of first-order terms, for representing programs, and to include inference rules for the introduction and discharge of hypotheses and eigenvariables. This extension, which we call extended natural semantics , affords a higher-level notion of abstract syntax for representing programs and suitable mechanisms for manipulating this syntax. We present several examples of semantic specifications for a simple functional programming language and demonstrate how we achieve simple and elegant manipulations of bound variables in functional programs. All the examples have been implemented and tested in λProlog, a higher-order logic programming language that supports all of the features of extended natural semantics.


title: Typing First-Class Continuations in ML

authors:
Robert Harper
Bruce F. Duba
David B. MacQueen

abstract: Abstract An extension of ML with continuation primitives similar to those found in Scheme is considered. A number of alternative type systems are discussed, and several programming examples are given. A continuation-based operational semantics is defined for a small, purely functional language, and the soundness of the Damas–Milner polymorphic type assignment system with respect to this semantics is proved. The full Damas–Milner type system is shown to be unsound in the presence of first-class continuations. Restrictions on polymorphism similar to those introduced in connection with reference types are shown to suffice for soundness.


title: The Use of Functional Languages in Teaching Computer Science

abstract: Abstract This survey presents information concerning the use of functional languages (both strict and non-strict) for teaching in higher education. It lists the languages used by over 70 different institutions, the years in which the courses are given, and the recommended textbooks.


title: Improving Intervals

authors:
W. Ken Jackson
F. Warren Burton

abstract: Abstract We show how improving values (Burton, 1991) can be extended to handle both upper and lower bounds. The result is a new data type, called improving intervals . We give a simple implementation of improving intervals that uses a list of successively tighter bounds to represent a value. A program using improving intervals can be evaluated as a parallel program using speculative evaluation. The utility of improving intervals is demonstrated through two programs: parallel alpha-beta and parallel branch-and-bound


title: Teaching Functional Programming to First-Year Students

authors:
Stef Joosten
Klaas van den Berg
Gerrit van Der Hoeven

abstract: Abstract In the period 1986–1991, experiments have been carried out with an introductory course in computer programming, based on functional programming. Due to thorough educational design and evaluation, a successful course has been developed. This has led to a revision of the computer programming education in the first year of the computer science curriculum at the University of Twente. This article describes the approach, the aim of the computer programming course, the outline and subject matter of the course, and the evaluation. Educational research has been done to assess the quality of the course.


title: Using Miranda as a First Programming Language

authors:
Tim Lambert
Peter Lindsay
Ken Robinson

abstract: Abstract The functional programming language Miranda has been used as a first programming language at the University of NSW since the beginning of 1989, when a new computer engineering course and a revised computer science course were introduced. This paper explains the reasons for choosing the language, and describes the subject in which Miranda is introduced. Examples of the presentation of the material, and of exercises and assignment used in the course, are given. Finally, an assessment of the experience is given.


title: Dynamics in ML

authors:
Xavier Leroy
Michel Mauny

abstract: Abstract Objects with dynamic types allow the integration of operations that essentially require runtime type-checking into statically-typed languages. This paper presents two extensions of the ML language with dynamics, based on our work on the CAML implementation of ML, and discusses their usefulness. The main novelty of this work is the combination of dynamics with polymorphism.


title: Functional Programming for Business Students

abstract: Abstract A functional language, Miranda, is being used on an introductory programming course for business students. This paper describes the rationale for such a course and choice of language. An application in the area of operations management, which is used in teaching, is given as an example of the benefits of using a functional language in this area. The reaction of the students and staff to this (for them) new paradigm of programming is described. Some conclusions are drawn for computing education for non-specialists.


title: Partially Strict Non-Recursive Data Types

authors:
Eric Nöcker
Sjaak Smetsers

abstract: Abstract Values belonging to lazy data types have the advantage that sub-components can be accessed without evaluating the values as a whole: unneeded components remain unevaluated. A disadvantage is that often a large amount of space and time is required to handle lazy data types properly. Many special constructor cells are needed to ‘glue’ the individual parts of a composite object together and to store it in the heap. We present a way of representing data in functional languages which makes these special constructor cells superfluous. In some cases, no heap at all is needed to store this data. To make this possible, we introduce a new kind of data type: ( partially) strict non-recursive data types . The main advantage of these types is that an efficient call-by-value mechanism can be used to pass arguments. A restrictive subclass of (partially) strict non-recursive data types, partially strict tuples , is treated more comprehensively. We also give examples of important classes of applications. In particular, we show how partially strict tuples can be used to define very efficient input and output primitives. Measurements of applications written in Concurrent Clean which exploit partially strict tuples have shown that speedups of 2 to 3 times are reasonable. Moreover, much less heap space is required when partially strict tuples are used.


title: Correctness of Binding-Time Analysis

abstract: Abstract A binding-time analysis is correct if it always produces consistent binding-time information. Consistency prevents partial evaluators from ‘going wrong’. A sufficient and decidable condition for consistency, called well-annotatedness, was first presented by Gomard and Jones. In this paper we prove that a weaker condition implies consistency. Our condition is decidable, subsumes the one of Gomard and Jones, and was first studied by Schwartzbach and the present author. Our result implies the correctness of the binding-time analysis of Mogensen, and it indicates the correctness of the core of the binding-time analyses of Bondorf and Consel. We also prove that all partial evaluators will on termination have eliminated all ‘eliminable’-marked parts of an input which satisfies our condition. This generalizes a result of Gomard. Our development is for the pure λ-calculus with explicit binding-time annotations.


title: Terminating Comprehensions

abstract: Abstract List terminators are discussed as a new form of qualifier in list comprehensions for early termination of a list. The semantics of list terminators is expressed in terms of an optimal translation of list comprehensions (cf. Wadler, 1987) because it makes direct use of a continuation list.


title: On the Specialization of Online Program Specializers

authors:
Erik Ruf
Daniel Weise

abstract: Abstract A common technique for improving the speed of program specialization is to specialize the program specializer itself on the program to be specialized, creating a custom program generator . Much research has been devoted to the problem of generating efficient program generators, which do not perform reductions at program generation time which could instead have been performed when the program generator was constructed. The conventional wisdom holds that only program specializers using binding-time approximations can be specialized into such efficient program generators. This paper argues that this is not the case, and demonstrates that the specialization of a nontrivial online program specializer similar to the original ‘naive MIX’ can indeed yield an efficient program generator. The key to our argument is that, while the use of binding-time information at program generator generation time is necessary for the construction of an efficient custom specializer, the use of explicit binding-time approximation techniques is not. This allows us to distinguish the problem at hand (i.e. the use of binding-time information during program generator generation) from particular solutions to that problem (i.e. offline specialization). We show that, given a careful choice of specializer data structures, and sufficiently powerful specialization techniques, binding-time information can be inferred and utilized without explicit approximations. This allows the construction of efficient, optimizing program generators from online program specializers.


title: An Incremental, Exploratory and Transformational Environment for the Lazy Functional Programming

authors:
Colin Runciman
Ian Toyn
Mike Firth

abstract: 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.


title: Heap Profiling of Lazy Functional Programs

authors:
Colin Runciman
David Wakeling

abstract: 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.


title: Functional Programming in Education - Introduction

authors:
Simon J. Thompson
Philip Wadler


title: Program Transformation with Metasystem Transitions

abstract: Abstract A new program transformation method is presented. It is a further refinement of supercompilation where the supercompiler is not applied directly to the function to be transformed, but to a metafunction, namely an interpreter which computes this function using its definition and an abstract (i.e. including variables) input. It is shown that with this method such tranformations become possible which the direct application of the supercompiler cannot perform. Examples include the merging of iterative loops, function inversion, and transformation of deterministic into non-deterministic algorithms, and vice-versa .


title: Specifying the Correctness of Binding-Time Analysis

abstract: Abstract Mogensen has exhibited a very compact partial evaluator for the pure lambda calculus, using binding-time analysis followed by specialization. We give a correctness criterion for this partial evaluator and prove its correctness relative to this specification. We show that the conventional properties of partial evaluators, such as the Futamura projections, are consequences of this specification. By considering both a flow analysis and the transformation it justifies together, this proof suggests a framework for incorporating flow analyses into verified compilers.


title: Baby Modula-3 and a Theory of Objects

abstract: Abstract Baby Modula-3 is a small, functional, object-oriented programming language. It is intended as a vehicle for explaining the core of Modula-3 from a biased perspective: Baby Modula-3 includes the main features of Modula-3 related to objects, but not much else. To the theoretician, Baby Modula-3 provides a tractable, concrete example of an object-oriented language, and we use it to study the formal semantics of objects. Baby Modula-3 is defined with a structured operational semantics and with a set of static type rules. A denotational semantics guarantees the soundness of this definition.


title: A Functional Animation Starter-Lit

abstract: Abstract A functional approach presents a fresh perspective on the problem of animation. We present an implementation of a functional animation system written in Haskell, and illustrate how it may be used to create simple and colourful animations.


title: On Generating unique Names

authors:
Lennart Augustsson
Mikael Rittri
Dan Synek

abstract: And Joktan begat Almodad, and Sheleph, and Hazarmaveth, and Jerah, and Handoram, and Uzal, and Diklah, and Obal, and Abimael, and Sheba, and Ophir, and Havilah, and Jobab: all these were the sons of Joktan. — Genesis 10:26–29


title: A Paradigmatic Object-Oriented Programming Language: Design, Static Typing and Semantics

abstract: Abstract To illuminate the fundamental concepts involved in object-oriented programming languages, we describe the design of TOOPL, a paradigmatic, statically-typed, functional, object-oriented programming language which supports classes, objects, methods, hidden instance variables, subtypes and inheritance. It has proven to be quite difficult to design such a language which has a secure type system. A particular problem with statically type checking object-oriented languages is designing typechecking rules which ensure that methods provided in a superclass will continue to be type correct when inherited in a subclass. The type-checking rules for TOOPL have this feature, enabling library suppliers to provide only the interfaces of classes with actual executable code, while still allowing users to safely create subclasses. To achieve greater expressibility while retaining type-safety, we choose to separate the inheritance and subtyping hierarchy in the language. The design of TOOPL has been guided by an analysis of the semantics of the language, which is given in terms of a model of the F-bounded second-order lambda calculus with fixed points at both the element and type level. This semantics supports the language design by providing a means to prove that the type-checking rules are sound, thus guaranteeing that the language is type-safe. While the semantics of our language is rather complex, involving fixed points at both the element and type level, we believe that this reflects the inherent complexity of the basic features of object-oriented programming languages. Particularly complex features include the implicit recursion inherent in the use of the keyword, self , to refer to the current object, and its corresponding type, MyType . The notions of subclass and inheritance introduce the greatest semantic complexities, whereas the notion of subtype is more straightforward to deal with. Our semantic investigations lead us to recommend caution in the use of inheritance, since small changes to method definitions in subclasses can result in major changes to the meanings of the other methods of the class.


title: Worst Case Scheduling for Parallel Functional Programs

authors:
F. Warren Burton
Victor J. Rayward-Smith

abstract: Abstract Many of the details that a programmer must manage when programming in a procedural language are handled by the implementation in a functional language. In a parallel functional language, we would expect the assignment of processes to processors and the scheduling of processes to be handled by the implementation. The partitioning of a program into processes may be handled by the implementation as well. We will assume that a parallel functional program may create processes dynamically, and that processes may synchronize in an arbitrary manner. It does not matter whether processes are defined in the source program or generated by the implementation. On parallel systems where each processor has some local memory, it is common practice not to move processes once they have started to execute. We will show that if each process must be executed on a single processor, then no fully automatic scheduling strategy can ensure good performance. We also will show that if all processes are sequential processes (i.e. do not contain internal parallelism), and if a process may be moved whenever it resumes execution following synchronization with another process, then good performance can be assured, at least in theory.


title: Safe Fusion of Functional Expressions II: Further Improvements

abstract: Abstract Large functional programs are often constructed by decomposing each big task into smaller tasks which can be performed by simpler functions. This hierarchical style of developing programs has been found to improve programmers' productivity because smaller functions are easier to construct and reuse. However, programs written in this way tend to be less efficient. Unnecessary intermediate data structures may be created. More function invocations may be required. To reduce such performance penalties, Phil Wadler proposed a transformation algorithm, called deforestation , which could automatically fuse certain composed expressions together to eliminate intermediate tree-like data structures. However, his technique is currently safe (terminates with no loss of efficiency) for only a subset of first-order expressions. This paper will generalise the deforestation technique to make it safe for all first-order and higher-order functional programs. Our generalisation is explained using a model for safe fusion which views each function as a producer and its parameters as consumers. Through this model, syntactic program properties are proposed to classify producers and consumers as either safe or unsafe. This classification is used to identify sub-terms that can be safely fused/eliminated. We present the generalised transformation algorithm, illustrate it with examples and provide a termination proof for the transformation algorithm of first-order programs. This paper also contains a suite of additional techniques to further improve the basic safe fusion method. These improvements could be viewed as enhancements to compensate for some inadequacies of the syntactic analyses used.


title: A - Translation and Looping Combinators in Pure Type Systems

authors:
Thierry Coquand
Hugo Herbelin

abstract: Abstract We present here a generalization of A-translation to a class of pure type systems. We apply this translation to give a direct proof of the existence of a looping combinator in a large class of inconsistent type systems, a class which includes type systems with a type of all types. This is the first non-automated solution to this problem.


title: Yet Yet a Counterexample for lambda + SP

authors:
Pierre-Louis Curien
Thérèse Hardin

abstract: In 1979, Klop (1980), answering a question raised by Mann in 1972, showed that the extension of λ-calculus with subjective pairing is not confluent. We refer to Klop (1980) and Barendregt (1981, revised 1984) for a perspective. The term presented by Klop to provide a counterexample is fairly simple, but the proof of non-confluence, although intuitively quite simple, involves some technical properties. Among others, a suitable standardization result on derivations in the extended system is needed in the proof. Klop's proof was revisited by Bunder (1985), who seemingly used less technical apparatus than Klop, starting with the same term as Klop. Although Bunder's proof does not explicitly use a standardization result, his proof proceeds internally with some rearrangements of derivations, so that it is fair to say that some standardization technique is present in Bunder (1985).


title: On the Generation of Specializers

abstract: Abstract Self-applicable specializers have been used successfully to automate the generation of compilers. Specializers are often rather sophisticated, for which reason one would like to adapt and transform them with the aid of the computer. But how to automate this process? The answer to this question is given by three specializer projections . While the Futamura projections define the generation of compilers from interpreters, the specializer projections define the generation of specializers from interpreters. We discuss the potential applications of the specializer projections, and argue that their realization is a real touchstone for the effectiveness of the specialization principle. In particular, we discuss generic specializers, bootstrapping of subject languages and the generation of optimizing specializers from interpretive specifications. The Futamura projections are regarded as a special case of the specializer projections. Recent results confirm that the specializer projections can be performed in practice using partial evaluators.


title: The Complexity of Type Inference for Higher-Order Typed lambda Calculi

authors:
Fritz Henglein
Harry G. Mairson

abstract: Abstract We analyse the computational complexity of type inference for untyped λ-terms in the second-order polymorphic typed λ-calculus ( F 2 ) invented by Girard and Reynolds, as well as higher-order extensions F 3 , F 4 , …, F ω proposed by Girard. We prove that recognising the F 2 -typable terms requires exponential time, and for F ω the problem is non-elementary. We show as well a sequence of lower bounds on recognising the F k -typable terms, where the bound for F k +1 is exponentially larger than that for F k . The lower bounds are based on generic simulation of Turing Machines, where computation is simulated at the expression and type level simultaneously. Non-accepting computations are mapped to non-normalising reduction sequences, and hence non-typable terms. The accepting computations are mapped to typable terms, where higher-order types encode reduction sequences, and first-order types encode the entire computation as a circuit, based on a unification simulation of Boolean logic. A primary technical tool in this reduction is the composition of polymorphic functions having different domains and ranges. These results are the first nontrivial lower bounds on type inference for the Girard/Reynolds system as well as its higher-order extensions. We hope that the analysis provides important combinatorial insights which will prove useful in the ultimate resolution of the complexity of the type inference problem.


title: Residual Theory in lambda-Calculus: A Formal Development

abstract: Abstract We present the complete development, in Gallina, of the residual theory of β-reduction in pure λ-calculus. The main result is the Prism Theorem, and its corollary Lévy's Cube Lemma, a strong form of the parallel-moves lemma, itself a key step towards the confluence theorem and its usual corollaries (Church-Rosser, uniqueness of normal forms). Gallina is the specification language of the Coq Proof Assistant (Dowek et al. , 1991; Huet 1992 b ). It is a specific concrete syntax for its abstract framework, the Calculus of Inductive Constructions (Paulin-Mohring, 1993). It may be thought of as a smooth mixture of higher-order predicate calculus with recursive definitions, inductively defined data types and inductive predicate definitions reminiscent of logic programming. The development presented here was fully checked in the current distribution version Coq V5.8. We just state the lemmas in the order in which they are proved, omitting the proof justifications. The full transcript is available as a standard library in the distribution of Coq.


title: Book Review: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic by Mike Gordon and Tom Melham (eds.), Cambridge University Press, 1993, ISBN 0-521-44189-7


title: An Overview of the Flagship System

abstract: Abstract The Flagship Project 1 was a research collaboration between the University of Manchester, Imperial College London and International Computers Ltd. The project was unusual in that it aimed to produce a complete computing system based on a declarative programming style. Three areas of a declarative system were addressed: (1) programming languages and programming environments; (2) the machine architecture and computational models; and (3) the software environment. This overview paper discusses each of these areas, the intention being to present the project as a coherent whole.


title: On the Equivalence Between CMC and TIM

authors:
Rafael Dueire Lins
Simon J. Thompson
Simon L. Peyton Jones

abstract: Abstract In this paper we present an equivalence between TIM, a machine developed to implement non-strict functional programming languages, and the set of Categorical Multi-Combinators, a rewriting system developed with similar aims. These two models of computation at first appear to be quite different, but we show a direct equivalence between them, thereby adding some new structure to the ‘design-space’ of abstract machines for non-strict languages.


title: Total Unfolding: Theory and Applications

abstract: Abstract Unfolding is a common technique in program transformations. Here, we present a computation model where unfolding is a simple generalisation of the usual concept of evaluation. The model is a variant of the well-known full substitution evaluation rule for recursive programs. The evaluation mechanism involved is symbolic substitution of function definitions followed by simplification. Simplification is expressed as a confluent rewrite strategy which uses three kinds of reductions: β-reduction, non-erasing reduction, and erasing reduction. Non-erasing reductions include simplification of constant subexpressions. Erasing reductions formalize the behaviour of nonstrict operations. In this computation model, we prove a termination theorem of symbolic unfolding relative to more instantiated calls. A possible application of the model is a technique called total unfolding , where a partially instantiated function call is unfolded until no more calls exist. Under certain conditions the result will be a first order term: such terms correspond to basic blocks in imperative programs and can be efficiently implemented by scheduling techniques. Possible applications are hardware synthesis, and code generation for parallel machines.


title: Lilac: A Functional Programming Language Based on Linear Logic

abstract: Abstract We take Abramsky's term assignment for Intuitionistic Linear Logic (the linear term calculus) as the basis of a functional programming language. This is a language where the programmer must embed explicitly the resource and control information of an algorithm. We give a type reconstruction algorithm for our language in the style of Milner's W algorithm, together with a description of the implementation and examples of use.


title: Algorithmic Debugging for Lazy Functional Languages

authors:
Henrik Nilsson
Peter Fritzson

abstract: Abstract Lazy functional languages have non-strict semantics and are purely declarative, i.e. they support the notion of referential transparency and are devoid of side-effects. Traditional debugging techniques are, however, not suited for lazy functional languages, since computations generally do not take place in the order one might expect. Since algorithmic debugging allows the user to concentrate on the declarative aspects of program semantics, and will semi-automatically find functions containing bugs, we propose to use this technique for debugging lazy functional programs. Because of the non-strict semantics of lazy functional languages, arguments to functions are in general partially evaluated expressions. The user is, however, usually more concerned with the values that these expressions represent. We address this problem by providing the user with a strictified view of the execution trace whenever possible. In this paper, we present an algorithmic debugger for a lazy functional language based on strictification and some experience in using it. A number of problems with the current implementation of the debugger (e.g. too large trace size and too many questions asked) are also discussed and some techniques for overcoming these problems, at least partially, are suggested. The key techniques are immediate strictification and piecemeal tracing .


title: Simple Type-Theoretic Foundations for Object-Oriented Programming

authors:
Benjamin C. Pierce
David N. Turner

abstract: Abstract We develop a formal, type-theoretic account of the basic mechanisms of object-oriented programming: encapsulation, message passing, subtyping and inheritance. By modelling object encapsulation in terms of existential types instead of the recursive records used in other recent studies, we obtain a substantial simplification both in the model of objects and in the underlying typed λ-calculus.


title: Principal Signatures for Higher-Order Program Modules

abstract: Abstract In this paper we present a language for programming with higher-order modules. The language HML is based on Standard ML in that it provides structures, signatures and functors. In HML, functors can be declared inside structures and specified inside signatures; this is not possible in Standard ML. We present an operational semantics for the static semantics of HML signature expressions, with particular emphasis on the handling of sharing. As a justification for the semantics, we prove a theorem about the existence of principal signatures. This result is closely related to the existence of principal type schemes for functional programming languages with polymorphism.


title: How Powerful are Folding/Unfolding Transformations?

abstract: Abstract This paper discusses the transformation power of Burstall and Darlington's folding/unfolding system, i.e. what kind of programs can be derived from a given one. A necessary condition of derivability is proved. The notion of inherent complexity of recursive functions in introduced. A bound on efficiency gain by folding/unfolding transformations is obtained for all reasonable computation models. The well-known partial correctness and incompleteness of the system are corollaries of the result. Examples of underivability are given, e.g. binary searching cannot be derived from linear searching, merge sorting cannot be derived from insert sorting.


title: Dynamic Typing in Polymorphic Languages

authors:
Martín Abadi
Luca Cardelli
Benjamin C. Pierce
Didier Rémy

abstract: Abstract There are situations in programming where some dynamic typing is needed, even in the presence of advanced static type systems. We investigate the interplay of dynamic types with other advanced type constructions, discussing their integration into languages with explicit polymorphism (in the style of system F ), implicit polymorphism (in the style of ML), abstract data types, and subtyping.


title: The Ins and Outs of Clean I/O

authors:
Peter Achten
Marinus J. Plasmeijer

abstract: Abstract Functional programming languages have banned assignment because of its undesirable properties. The reward of this rigorous decision is that functional programming languages are side-effect free. There is another side to the coin: because assignment plays a crucial role in Input/Output (I/O), functional languages have a hard time dealing with I/O. Functional programming languages have therefore often been stigmatised as inferior to imperative programming languages because they cannot deal with I/O very well . In this paper, we show that I/O can be incorporated in a functional programming language without loss of any of the generally accepted advantages of functional programming languages. This discussion is supported by an extensive account of the I/O system offered by the lazy, purely functional programming language Clean. Two aspects that are paramount in its I/O system make the approach novel with respect to other approaches. These aspects are the technique of explicit multiple environment passing , and the Event I/O framework to program Graphical User I/O in a highly structured and high-level way. Clean file I/O is as powerful and flexible as it is in common imperative languages (one can read, write, and seek directly in a file). Clean Event I/O provides programmers with a high-level framework to specify complex Graphical User I/O. It has been used to write applications such as a window-based text editor, an object based drawing program, a relational database, and a spreadsheet program. These graphical interactive programs are completely machine independent, but still obey the look-and-feel of the concrete window environment being used. The specifications are completely functional and make extensive use of uniqueness typing, higher-order functions, and algebraic data types. Efficient implementations are present on the Macintosh, Sun (X Windows under Open Look) and PC (OS/2).


title: Strong Normalisation for the Linear Term Calculus

abstract: Abstract We prove a strong normalisation result for the linear term calculus of Benton, Bierman, Hyland and de Paiva. Rather than prove the result from first principles, we give a translation of linear terms into terms in the second-order polymorphic lambda calculus (λ2) which allows the result to be proved by appealing to the well-known strong normalisation property of λ2. An interesting feature of the translation is that it makes use of the λ2 coding of a coinductive datatype as the translation of the !-types (exponentials) of the linear calculus.


title: Lexical Profiling: Theory and Practice

authors:
Chris D. Clack
Stuart Clayman
David Parrott

abstract: Abstract This paper addresses the issue of analysing the run-time behaviour of lazy, higher-order functional programs. We examine the difference between the way that functional programmers and functional language implementors view program behaviour. Existing profiling techniques are discussed and a new technique is proposed which produces results that are straightforward for programmers to assimilate. The new technique, which we call lexical profiling , collects information about the run-time behaviour of functional programs, and reports the results with respect to the original source code rather than simply listing the actions performed at run-time. Lexical profiling complements implementation-specific profiling and is important because it provides a view of program activity which is largely independent of the underlying evaluation mechanism. Using the lexical profiler, programmers may easily relate results back to the source program. We give a full implementation of the lexical profiling technique for a sequential, interpretive graph reduction engine, and extensions for compiled and parallel graph reduction are discussed.


title: On-Line & Off-Line Partial Evaluation: Semantic Specifications and Correctness Proofs

authors:
Charles Consel
Siau-Cheng Khoo

abstract: Abstract This paper presents semantic specifications and correctness proofs for both on-line and offline partial evaluation of strict first-order functional programs. To do so, our strategy consists of defining a core semantics as a basis for the specification of three non-standard evaluations: instrumented evaluation, on-line and off-line partial evaluation. We then use the technique of logical relations to prove the correctness of both on-line and off-line partial evaluation semantics. The contributions of this work are as follows: 1. We provide a uniform framework to defining and proving correct both on-line and off-line partial evaluation. 2. This work required a formal specification of on-line partial evaluation with polyvariant specialization. We define criteria for its correctness with respect to an instrumented standard semantics. As a by-product, on-line partial evaluation appears to be based on a fixpoint iteration process, just like binding-time analysis. 3. We show that binding-time analysis, the preprocessing phase of off-line partial evaluation, is an abstraction of on-line partial evaluation. Therefore, its correctness can be proved with respect to on-line partial evaluation, instead of with respect to the standard semantics, as is customarily done. 4. Based on the binding-time analysis, we formally derive the specialization semantics for off-line partial evaluation. This strategy ensures the correctness of the resulting semantics.


title: A Polymorphic Library for Constructive Solid Geometry

authors:
John R. Davy
Peter M. Dew

abstract: Abstract Solid modelling using constructive solid geometry (CSG) includes many examples of stylised divide-and-conquer algorithms. We identify the sources of these recurrent patterns and describe a Geometric Evaluation Library (GEL) which captures them as higher-order functions. This library then becomes the basis of developing CSG applications quickly and concisely. GEL is currently implemented as a set of separately compiled modules in the pure functional language Hope+. We evaluate our work in terms of performance and general applicability. We also assess the benefits of the functional paradigm in this domain and the merits of programming with a set of higher-order functions.


title: Untyped Strictness Analysis

authors:
Christine Ernoult
Alan Mycroft

abstract: Abstract We re-express Hudak and Young's higher-order strictness analysis for the untyped λ-calculus in a conceptually simpler and more semantically-based manner. We show our analysis to be a sound abstraction of Hudak and Young's which is also complete in a sense we make precise.


title: Comparing Id and Haskell in a Monte Carlo Photon Transport Code

authors:
Jeffrey Hammes
Olaf M. Lubeck
A. P. Wim Böhm

abstract: Abstract In this paper we present functional Id and Haskell versions of a large Monte Carlo radiation transport code, and compare the two languages with respect to their expressiveness. Monte Carlo transport simulation exercises such abilities as parsing, input/output, recursive data structures and traditional number crunching, which makes it a good test problem for languages and compilers. Using some code examples, we compare the programming styles encouraged by the two languages. In particular, we discuss the effect of laziness on programming style. We point out that resource management problems currently prevent running realistically large problem sizes in the functional versions of the code.


title: Special Issue on State-of-the-Art Applications of Pure Functional Programming Languages

authors:
Pieter H. Hartel
Marinus J. Plasmeijer

abstract: Can functional programs be used to build real applications?The mere fact that this question is being asked is encouraging.Functional programming is all too often perceived as an exotic, mostly theoretical activity that has no bearing on reality.1994 saw two events specifically devoted to answering this question.The first was the Dagstuhl workshop on 'Functional programming in the real world', and the second the creation of this special issue.During the Dagstuhl workshop some 30 applications were presented.The call for papers for this special issue attracted 21 submissions.The sheer number of people working on applications indicates that solving real problems using functional languages is now becoming a serious proposition.The contributions in this issue address several diverse application areas: nuclear physics, databases query processing, parallel vision, building a spread sheet, solid modelling and molecular biology.Several other areas such as operational research and engineering design were represented in the papers that could not be included in this issue.A number of papers were also submitted targeting typical computer science applications, such as building parsers, programming environments, and executable specifications.The six papers that make up this issue have been selected purely on the basis of the formal refereeing process.Three of the papers describe prototypes of real systems.These are the database query processing, parallel vision and molecular biology systems.The production systems, which have been developed on the basis of these prototypes are used 'in anger'.The production systems have been implemented respectively as a shell script, a parallel Occam 2 program and as a C++ program.The prototypes are either incomplete, or too slow or space hungry to be used as a real application.The other three papers describe kernel applications, that were built to gain understanding of the problem domain.These are the nuclear physics, spreadsheet and solid modelling programs.These kernel applications are not used as real applications because they are not sufficiently complete to do the job properly.


title: A Unifying Type-Theoretic Framework for Objects

authors:
Martin Hofmann
Benjamin C. Pierce

abstract: Abstract We give a direct type-theoretic characterization of the basic mechanisms of object-oriented programming, including objects, methods, message passing, and subtyping, by introducing an explicit constructor for object types and suitable introduction, elimination, and equality rules. The resulting abstract framework provides a basis for justifying and comparing previous encodings of objects based on recursive record types (Cardelli, 1984; Cardelli, 1992; Bruce, 1994; Cook et al. , 1990; Mitchell, 1990a) and encodings based on existential types (Pierce & Turner, 1994).


title: Implementing a Functional Spreadsheet in Clean

authors:
Walter A. C. A. J. de Hoon
Luc M. W. J. Rutten
Marko C. J. D. van Eekelen

abstract: Abstract It has been claimed that recent developments in the research on the efficiency of code generation and on graphical input/output interfacing have made it possible to use a functional language to write efficient programs that can compete with industrial applications written in a traditional imperative language. As one of the early steps in verifying this claim, this paper describes a first attempt to implement a spreadsheet in a lazy, purely functional language. An interesting aspect of the design is that the language with which the user specifies the relations between the cells of the spreadsheet is itself a lazy, purely functional and higher order language as well, and not some special dedicated spreadsheet language. Another interesting aspect of the design is that the spreadsheet incorporates symbolic reduction and normalisation of symbolic expressions (including equations). This introduces the possibility of asking the system to prove equality of symbolic cell expressions: a property which can greatly enhance the reliability of a particular user-defined spreadsheet. The resulting application is by no means a fully mature product. It is not intended as a competitor to commercially available spreadsheets. However, with its higher order lazy functional language and its symbolic capabilities it may serve as an interesting candidate to fill the gap between calculators with purely functional expressions and full-featured spreadsheets with dedicated non-functional spreadsheet languages. This paper describes the global design and important implementation issues in the development of the application. The experience gained and lessons learnt during this project are discussed. Performance and use of the resulting application are compared with related work.


title: The Virtues of Eta-Expansion

authors:
C. Barry Jay
Neil Ghani

abstract: Abstract Interpreting η-conversion as an expansion rule in the simply-typed λ-calculus maintains the confluence of reduction in a richer type structure. This use of expansions is supported by categorical models of reduction, where β-contraction, as the local counit, and η-expansion, as the local unit, are linked by local triangle laws. The latter form reduction loops, but strong normalization (to the long βη-normal forms) can be recovered by ‘cutting’ the loops.


title: A System of Constructor Classes: Overloading and Implicit Higher-Order Polymorphism

abstract: Abstract This paper describes a flexible type system that combines overloading and higher-order polymorphism in an implicitly typed language using a system of constructor classes —a natural generalization of type classes in Haskell. We present a range of examples to demonstrate the usefulness of such a system. In particular, we show how constructor classes can be used to support the use of monads in a functional language. The underlying type system permits higher-order polymorphism but retains many of the attractive features that have made Hindley/Milner type systems so popular. In particular, there is an effective algorithm that can be used to calculate principal types without the need for explicit type or kind annotations. A prototype implementation has been developed providing, amongst other things, the first concrete implementation of monad comprehensions known to us at the time of writing.


title: Refining Reduction in the Lambda Calculus

authors:
Fairouz Kamareddine
Rob Nederpelt

abstract: Abstract We introduce a λ-calculus notation which enables us to detect in a term, more β-redexes than in the usual notation. On this basis, we define an extended β-reduction which is yet a subrelation of conversion. The Church Rosser property holds for this extended reduction. Moreover, we show that we can transform generalised redexes into usual ones by a process called ‘term reshuffling’.


title: Semantics Directed Program Execution Monitoring

authors:
Amir Kishon
Paul Hudak

abstract: Abstract Monitoring semantics is a formal model of program execution which captures ‘monitoring activity’ as found in profilers, tracers, debuggers, etc. Beyond its theoretical interest, this formalism provides a new methodology for implementing a large family of source-level monitoring activities for sequential deterministic programming languages. In this article we explore the use of monitoring semantics in the specification and implementation of a variety of monitors: profilers, tracers, collecting interpreters, and, most importantly, interactive source-level debuggers. Although we consider such monitors only for (both strict and non-strict) functional languages, the methodology extends easily to imperative languages, since it begins with a continuation semantics specification. In addition, using standard partial evaluation techniques as an optimization strategy, we show that the methodology forms a practical basis for building real monitors. Our system can be optimized at two levels of specialization: specializing the interpreter with respect to a monitor specification automatically yields an instrumented interpreter; further specializing this instrumented interpreter with respect to a source program yields an instrumented program, i.e. one in which the extra code to perform monitoring has been automatically embedded into the program.


title: Prototyping a Parallel Vision System in Standard ML

authors:
Greg Michaelson
Norman Scaife

abstract: Abstract The construction of a parallel vision system from Standard ML prototypes is presented. The system recognises 3D objects from 2D scenes through edge detection, grouping of edges into straight lines and line junction based model matching. Functional prototyping for parallelism is illustrated through the development of the straight line detection component. The assemblage of the whole system from prototyped components is then considered and its performance discussed.


title: Type Reconstruction for Type Classes

authors:
Tobias Nipkow
Christian Prehofer

abstract: Abstract We study the type inference problem for a system with type classes as in the functional programming language Haskell. Type classes are an extension of ML-style polymorphism with overloading. We generalize Milner's work on polymorphism by introducing a separate context constraining the type variables in a typing judgement. This leads to simple type inference systems and algorithms which closely resemble those for ML. In particular, we present a new unification algorithm which is an extension of syntactic unification with constraint solving. The existence of principal types follows from an analysis of this unification algorithm.


title: Simple and Efficient Purely Functional Queues and Deques

abstract: Abstract We present purely functional implementations of queues and double-ended queues (deques) requiring only O (1) time per operation in the worst case. Our algorithms are considerably simpler than previous designs with the same bounds. The inspiration for our approach is the incremental behaviour of certain functions on lazy lists.


title: A Debugger for Standard ML

authors:
Andrew P. Tolmach
Andrew W. Appel

abstract: Abstract We have built a portable, instrumentation-based, replay debugger for the Standard ML of New Jersey compiler. Traditional ‘source-level’ debuggers for compiled languages actually operate at machine level, which makes them complex, difficult to port, and intolerant of compiler optimization. For secure languages like ML, however, debugging support can be provided without reference to the underlying machine, by adding instrumentation to program source code before compilation. Because instrumented code is (almost) ordinary source, it can be processed by the ordinary compiler. Our debugger is thus independent from the underlying hardware and runtime system, and from the optimization strategies used by the compiler. The debugger also provides reverse execution, both as a user feature and an internal mechanism. Reverse execution is implemented using a checkpoint and replay system; checkpoints are represented primarily by first-class continuations.


title: Defining Data Structures via Böhm-Out

abstract: Abstract We show that any recursively enumerable subset of a data structure can be regarded as the solution set to a Böhm-out problem.


title: Exploring the Conformations of Nucleic Acids

authors:
Marcel Turcotte
Guy Lapalme
François Major

abstract: Abstract This paper presents an application of functional programming in the field of molecular biology: exploring the conformations of nucleic acids. The Nucleic Acid three-dimensional structure determination problem (NA3D) and a constraint satisfaction algorithm are formally described. Prototyping and experimental development using the Miranda functional programming language, over the last four years, are discussed. A Prolog implementation has been developed to evaluate software engineering and performance criteria between functional and logic programming. A C++ implementation has been developed for distribution purpose and to solve large practical problems. This system, called MC-SYM for ‘Macromolecular Conformation by SYMbolic generation’, is used in more than 50 laboratories, including academic and government research centres and pharmaceutical companies.


title: Communication Lifting: Fixed Point Computation for Parallelism

authors:
Willem G. Vree
Pieter H. Hartel

abstract: Abstract Communication lifting is a program transformation that can be applied to a synchronous process network to restructure the network. This restructuring in theory improves sequential and parallel performance. The transformation has been formally specified and proved correct and it has been implemented as an automatic program transformation tool. This tool has been applied to a small set of programs consisting of synchronous process networks. For these networks communication lifting generates parallel programs that do not require locking. Measurements indicate performance gains in practice both with sequential and parallel evaluation. Communication lifting is a worthwhile optimization to be included in a compiler for a lazy functional language.


title: Funser: A Functional Server for Textual Information Retrieval

authors:
Donald A. Ziff
Stephen P. Spackman
Keith Waclena

abstract: Abstract This paper describes a data-intensive application written in a lazy functional language: a server for textual information retrieval. The design illustrates the importance of interoperability, the capability of interacting with code written in other programming languages. Lazy functional programming is shown to be a powerful and elegant means of accomplishing several desirable concrete goals: delivering initial results promptly, using space economically, and avoiding unnecessary I/O. Performance results, however, are mixed.


title: Empirical and Analytic Study of Stack Versus Heap Cost for Languages with Closures

authors:
Andrew W. Appel
Zhong Shao

abstract: Abstract We present a comprehensive analysis of all the components of creation, access and disposal of heap-allocated and stack-allocated activation records. Among our results are: •Although stack frames are known to have a better cache read-miss rate than heap frames, our simple analytical model (backed up by simulation results) shows that the difference is too trivial to matter. •The cache write-miss rate of heap frames is very high; we show that a variety of miss-handling strategies (exemplified by specific modern machines) can give good performance, but not all can. •Stacks restrict the flexibility of closure representations (for higher-order functions) in important (and costly) ways. •The extra load placed on the garbage collector by heap-allocated frames is small. •The demands of modern programming languages make stacks complicated to implement efficiently and correctly. Overall, the execution cost of stack-allocated and heap-allocated frames is similar; but heap frames are simpler to implement and allow very efficient first-class continuations.


title: The Bologna Optimal Higher-Order Machine

authors:
Andrea Asperti
Cecilia Giovanetti
Andrea Naletto

abstract: Abstract The Bologna Optimal Higher-order Machine (BOHM) is a prototype implementation of the core of a functional language based on (a variant of) Lamping's optimal graph reduction technique (Lamping, 1990; Gonthier et al. , 1992a; Asperti, 1994). The source language is a sugared λ-calculus enriched with booleans, integers, lists and basic operations on these data types (following the guidelines of Interaction Systems – Asperti and Laneve (1993b, 1994), Laneve (1993)). In this paper, we shall describe BOHM's general architecture (comprising the garbage collector), and give a large set of benchmarks and experimental results.


title: Proof-Irrelevance out of Exluded-Middle and Choice in the Calculus of Constructions

authors:
Franco Barbanera
Stefano Berardi

abstract: Abstract We present a short and direct syntactic proof of the fact that adding the axiom of choice and the principle of excluded-middle to Coquand–Huet's Calculus of Constructions gives proof-irrelevance.


title: lambda-nu, A Calculus of Explicit Substitutions which Preserves Strong Normalisation

authors:
Zine-El-Abidine Benaissa
Daniel Briaud
Pierre Lescanne
Jocelyne Rouyer-Degli

abstract: Abstract Explicit substitutions were proposed by Abadi, Cardelli, Curien, Hardin and Lévy to internalise substitutions into λ-calculus and to propose a mechanism for computing on substitutions. λν is another view of the same concept which aims to explain the process of substitution and to decompose it in small steps. It favours simplicity and preservation of strong normalisation. This way, another important property is missed, namely confluence on open terms. In spirit, λν is closely related to another calculus of explicit substitutions proposed by de Bruijn and called C λξΦ. In this paper, we introduce λν, we present C λξΦ in the same framework as λν and we compare both calculi. Moreover, we prove properties of λν; namely λν correctly implements β reduction, λν is confluent on closed terms, i.e. on terms of classical λ-calculus and on all terms that are derived from those terms, and finally λν preserves strong normalisation in the following sense: strongly β normalising terms are strongly λν normalising.


title: A Simple Proof of the Undecidability of Inhabitation in lambdaP

authors:
Marc Bezem
Jan Springintveld

abstract: Capsule ReviewIt had been known that the simplest system with dependent types, XP, is undecidable, in that sense that the set {(A,D\3pr\-XP p:A} is non-computable.The proof runs as follows.First, there is an obvious embedding of predicate logic into XP.This is the principle idea of one of the basic members of the AUTOMATH family, AUT-QE, and also later of Edinburgh LF.It can be shown that this embedding is conservative (Berardi; Barendsen and Geuvers).This is not completely obvious, since XP has functions of arbitrarily high type at its disposal.Now it follows from Godel's technique (proving the incompleteness theorems) that arithmetic and even a finitely axiomatizable part of it (Robinson's arithmetic) is essentially undecidable.Therefore XP is also undecidable.This is quite a long path to the result -admittedly quite beautiful, passing along classical details like the Chinese remainder theorem -but almost too much.Fortunately, the authors of this paper have given a very direct argument showing the same result, by a surprisingly straightforward encoding of a register machine.An inhabitation problem in a given Pure Type System (PTS) XS is a pair (F, B) such that, for some sort s, F \-^s B : s.A solution for (F, B) is a term A such that F \~xs A : B. In this note we prove that in the PTS kP it is undecidable whether an inhabitation problem has a solution.This result also follows from Lob's results on embeddings of predicate logic in fragments of intuitionistic logic (Lob, 1976, p. 1, 1. 10) plus the fact that XP is sound and complete with respect to minimal predicate logic (see Geuvers (1993)).The merit of our proof is that it is short, simple and intuitive.Sometimes, inhabitation problems are defined with F the empty context.In IP, however, this makes little sense: the only statement valid in the empty context is * : D. After the proof of our result, we discuss related results concerning the other systems of the ^-cube.For a general introduction to PTSs the reader is referred to Barendregt (1992).


title: Generic Functional Programming with Types and Relations

authors:
Richard S. Bird
Oege de Moor
Paul F. Hoogendijk

abstract: Abstract A generic functional program is one which is parameterised by datatype. By installing specific choices, for example lists or trees, different programs are obtained that are, nevertheless, abstractly the same. The purpose of this paper is to explore the possibility of deriving generic programs. Part of the theory of lists that deals with segments is recast as a theory about ‘segments’ in a wide class of datatypes, and then used to pose and solve a generic version of a well-known problem.


title: Generating Action Compilers by Partial Evaluation

authors:
Anders Bondorf
Jens Palsberg

abstract: Abstract Compiler generation based on Mosses' action semantics has been studied by Brown, Moura, and Watt, and also by the second author. The core of each of their systems is a handwritten action compiler, producing either C or machine code. We have obtained an action compiler in a much simpler way: by partial evaluation of an action interpreter. Even though our compiler produces Scheme code, the code runs as fast as that produced by the previous action compilers.


title: Optimal Purely Functional Priority Queues

authors:
Gerth Stølting Brodal
Chris Okasaki

abstract: Abstract Brodal recently introduced the first implementation of imperative priority queues to support findMin, insert and meld in O (1) worst-case time, and deleteMin in O (log n ) worst-case time. These bounds are asymptotically optimal among all comparison-based priority queues. In this paper, we adapt Brodal's data structure to a purely functional setting. In doing so, we both simplify the data structure and clarify its relationship to the binomial queues of Vuillemin, which support all four operations in O (log n ) time. Specifically, we derive our implementation from binomial queues in three steps: first, we reduce the running time of insert to O (1) by eliminating the possibility of cascading links; second, we reduce the running time of findMin to O (1) by adding a global root to hold the minimum element; and finally, we reduce the running time of meld to O (1) by allowing priority queues to contain other priority queues. Each of these steps is expressed using ML-style functors. The last transformation, known as data-structural bootstrapping, is an interesting application of higher-order functors and recursive structures.


title: Proving the Correctness of Compiler Optimisations Based on a Global Analysis: A Study of Strictness Analysis

authors:
Geoffrey Livingston Burn
Daniel Le Métayer

abstract: Abstract A substantial amount of work has been devoted to the proof of correctness of various program analyses but much less attention has been paid to the correctness of compiler optimisations based on these analyses. In this paper we tackle the problem in the context of strictness analysis for lazy functional languages. We show that compiler optimisations based on strictness analysis can be expressed formally in the functional framework using continuations. This formal presentation has two benefits: it allows us to give a rigorous correctness proof of the optimised compiler; and it exposes the various optimisations made possible by a strictness analysis.


title: Some Lattice-Based Scientific Problems, Expressed in Haskell

authors:
D. B. Carpenter
Hugh Glaser

abstract: Abstract The paper explores the application of a lazy functional language, Haskell, to a series of grid-based scientific problems—solution of the Poisson equation, and Monte Carlo simulation of two theoretical models from statistical and particle physics. The implementations introduce certain abstractions of grid topology, making extensive use of the polymorphic features of Haskell. Updating is expressed naturally through use of infinite lists, exploiting the laziness of the language. Evolution of systems is represented by arrays of interacting streams.


title: Reference Counting as a Computational Interpretation of Linear Logic

authors:
Jawahar Chirimar
Carl A. Gunter
Jon G. Riecke

abstract: Abstract We develop an operational model for a language based on linear logic. Our semantics is ‘low-level’ enough to express sharing and copying while still being ‘high-level’ enough to abstract away from details of memory layout, and thus can be used to test potential applications of linear logic for analysis of programs. In particular, we demonstrate a precise relationship between type correctness for the linear-logic-based language and the correctness of a reference-counting interpretation of the primitives, and formulate and prove a result describing the possible run-time reference counts of values of linear type.


title: Formal Basis for the Refinement of Rule Based Transition Systems

abstract: Abstract This paper makes a contribution to the refinement of systems which involve search by proposing a simple non-deterministic model for rule based transition systems and using this to define a meaning for rule based refinement which allows each stage of the software development path to be verified with respect to the previous stage. The proposal allows a system which involves search to be specified in terms of all the possible outcomes. Each stage of refinement will introduce complexity to the rules and therefore develop the search space in ever more sophisticated ways. At each stage of the refinement it will be possible to be precise about which collections of outcomes have been deleted, thereby achieving a verified (prototype) implementation.


title: A Confluent Reduction for the lambda-Calculus with Surjective Pairing and Terminal Object

authors:
Pierre-Louis Curien
Roberto Di Cosmo

abstract: Abstract We exhibit confluent and effectively weakly normalizing (thus decidable) rewriting systems for the full equational theory underlying cartesian closed categories, and for polymorphic extensions of it. The λ-calculus extended with surjective pairing has been well-studied in the last two decades. It is not confluent in the untyped case, and confluent in the typed case. But to the best of our knowledge the present work is the first treatment of the lambda calculus extended with surjective pairing and terminal object via a confluent rewriting system, and is the first solution to the decidability problem of the full equational theory of Cartesian Closed Categories extended with polymorphic types . Our approach yields conservativity results as well. In separate papers we apply our results to the study of provable type isomorphisms, and to the decidability of equality in a typed λ-calculus with subtyping.


title: π-Red+ An Interactive Compiling Graph Reduction System for an Applied λ-Calculus

authors:
Dietmar Gärtner
Werner E. Kluge

abstract: Abstract This paper describes a compiling graph reduction system which realizes the reduction semantics of a fully-fledged applied λ-calculus. High-level functional programs are conceptually executed as sequences of program transformations governed by full β-reductions. They may be carried out step-by-step, and intermediate programs may be displayed in high-level notation, rendering the system suitable for interactive program design, high-level debugging, and also for teaching basic programming language concepts and language interpretation. Run-time efficiency for production runs is achieved by means of an abstract stack machine ASM which serves as an intermediate level of code generation. It employs multiple stacks for reasonably fast function calls, optimized tail-end recursions, and earliest possible releases of subgraphs that are no longer needed. The ASM involves an interpreter if and only if potential naming conflicts need to be resolved when reducing partial function applications.


title: Deriving Tidy Drawings of Trees

abstract: Abstract The tree-drawing problem is to produce a ‘tidy’ mapping from elements of a tree to points in the plane. In this paper, we derive an efficient algorithm for producing tidy drawings of trees. The specification, the starting point for the derivations, consists of a collection of intuitively appealing criteria satisfied by tidy drawings. The derivation shows constructively that these criteria completely determine the drawing. Indeed, the criteria completely determine a simple but inefficient algorithm for drawing a tree, which can be transformed into an efficient algorithm using just standard techniques and a small number of inventive steps. The algorithm consists of an upwards accumulation followed by a downwards accumulation on the tree, and is further evidence of the utility of these two higher-order tree operations.


title: The Third Homomorphism Theorem

abstract: Abstract The Third Homomorphism Theorem is a folk theorem of the constructive algorithmics community. It states that a function on lists that can be computed both from left to right and from right to left is necessarily a list homomorphism – it can be computed according to any parenthesization of the list. We formalize and prove the theorem, and use it to improve an O ( n 2 ) sorting algorithm to O ( n log n ).


title: Sparse Matrix Representations in a Functional Language

authors:
Philip W. Grant
John A. Sharp
Michael F. Webster
Xiaoming Zhang

abstract: Abstract This paper investigates several sparse matrix representation schemes and associated algorithms in Haskell for solving linear systems of equations arising from solving realistic computational fluid dynamics problems using a finite element algorithm. This work complements that of Wainwright and Sexton (1992) in that a Choleski direct solver (with an emphasis on its forward/backward substitution steps) is examined. Experimental evidence comparing time and space efficiency of these matrix representation schemes is reported, together with associated forward/backward substitution implementations. Our results are in general agreement with Wainwright and Sexton's.


title: Weak Polymorphism can be Sound

abstract: Abstract The weak polymorphic type system of Standard ML of New Jersey (SML/NJ) (MacQueen, 1992) has only been presented as part of the implementation of the SML/NJ compiler, not as a formal type system. As a result, it is not well understood. And while numerous versions of the implementation have been shown unsound, the concept has not been proved sound or unsound. We present an explanation of weak polymorphism and show that a formalization of this is sound. We also relate this to the SML/NJ implementation of weak polymorphism through a series of type systems that incorporate elements of the SML/NJ type inference algorithm.


title: Operational Interpretations of an Extension of Fomega with Control Operators

authors:
Robert Harper
Mark Lillibridge

abstract: Abstract We study the operational semantics of an extension of Girard's System F ω with two control operators: an abort operation that abandons the current control context, and a callcc operation that captures the current control context. Two classes of operational semantics are considered, each with a call-by-value and a call-by-name variant, differing in their treatment of polymorphic abstraction and instantiation. Under the standard semantics, polymorphic abstractions are values and polymorphic instantiation is a significant computation step; under the ML-like semantics evaluation proceeds beneath polymorphic abstractions and polymorphic instantiation is computationally insignificant. Compositional, type-preserving continuation-passing style (cps) transformation algorithms are given for the standard semantics, resulting in terms on which all four evaluation strategies coincide. This has as a corollary the soundness and termination of well-typed programs under the standard evaluation strategies. In contrast, such results are obtained for the call-by-value ML-like strategy only for a restricted sub-language in which constructor abstractions are limited to values. The ML-like call-by-name semantics is indistinguishable from the standard call-by-name semantics when attention is limited to complete programs.


title: Benchmarking Implementations of Functional Languages with 'Pseudoknot', a Float-Intensive Benchmark

authors:
Pieter H. Hartel
Marc Feeley
Martin Alt
Lennart Augustsson
Peter Baumann
Marcel Beemster
Emmanuel Chailloux
Christine H. Flood
Wolfgang Grieskamp
John H. G. van Groningen
Kevin Hammond
Bogumil Hausman
Melody Y. Ivory
Richard E. Jones
Jasper Kamperman
Peter Lee
Xavier Leroy
Rafael Dueire Lins
Sandra Loosemore
Niklas Röjemo
Manuel Serrano
Jean-Pierre Talpin
Jon Thackray
Stephen Thomas
Pum Walters
Pierre Weis
Peter Wentworth

abstract: Abstract Over 25 implementations of different functional languages are benchmarked using the same program, a floating-point intensive application taken from molecular biology. The principal aspects studied are compile time and execution time for the various implementations that were benchmarked. An important consideration is how the program can be modified and tuned to obtain maximal performance on each language implementation. With few exceptions, the compilers take a significant amount of time to compile this program, though most compilers were faster than the then current GNU C compiler (GCC version 2.5.8). Compilers that generate C or Lisp are often slower than those that generate native code directly: the cost of compiling the intermediate form is normally a large fraction of the total compilation time. There is no clear distinction between the runtime performance of eager and lazy implementations when appropriate annotations are used: lazy implementations have clearly come of age when it comes to implementing largely strict applications, such as the Pseudoknot program. The speed of C can be approached by some implementations, but to achieve this performance, special measures such as strictness annotations are required by non-strict implementations. The benchmark results have to be interpreted with care. Firstly, a benchmark based on a single program cannot cover a wide spectrum of ‘typical’ applications. Secondly, the compilers vary in the kind and level of optimisations offered, so the effort required to obtain an optimal version of the program is similarly varied.


title: The Resource Constrained Shortest Path Problem Implemented in a Lazy Functional Language

authors:
Pieter H. Hartel
Hugh Glaser

abstract: Abstract The resource constrained shortest path problem is an NP-hard problem for which many ingenious algorithms have been developed. These algorithms are usually implemented in Fortran or another imperative programming language. We have implemented some of the simpler algorithms in a lazy functional language. Benefits accrue in the software engineering of the implementations. Our implementations have been applied to a standard benchmark of data files, which is available from the Operational Research Library of Imperial College, London. The performance of the lazy functional implementations, even with the comparatively simple algorithms that we have used, is competitive with a reference Fortran implementation.


title: Combinators for Parsing Expressions

abstract: Abstract This paper describes a scheme for constructing parsers based on the top-down combinator approach. In particular, it describes a set of combinators for parsing expressions described by ambiguous grammars with precedence and associativity rules. The new combinators embody the mechanical grammar manipulations typically employed to remove left-recursion and hence help to avoid the possibility of a non-terminating parser. A number of approaches to the problem are described—the most elegant and efficient method is based on continuation passing. As a practical demonstration, a parser for the expression part of the C programming language is presented. The expression combinators are general, and may be constructed from any suitable set of top-down combinators. A comparison with parser generators shows that the combinator approach is most applicable for rapid development.


title: Haskore Music Notation - An Algebra of Music

authors:
Paul Hudak
Tom Makucevich
Syam Gadde
Bo Whong

abstract: Abstract We have developed a simple algebraic approach to music description and composition called Haskore . In this framework, musical objects consist of primitive notions such as notes and rests, operations to transform musical objects such as transpose and tempo-scaling, and operations to combine musical objects to form more complex ones, such as concurrent and sequential composition. When these simple notions are embedded into a functional language such as Haskell, rather complex musical relationships can be expressed clearly and succinctly. Exploiting the algebraic properties of Haskore, we have further defined a notion of literal performance (devoid of articulation) through which observationally equivalent musical objects can be determined. With this basis many useful properties can be proved, such as commutative, associative, and distributive properties of various operators. An algebra of music thus surfaces.


title: Back to Basics: Deriving Representation Changers Functionally

authors:
Graham Hutton
Erik Meijer


title: On Cubism

abstract: Abstract A number of difficulties in the formalism of Pure Type Systems (PTS) is discussed and an alternative classification system for typed calculi is proposed. In the new approach the main novelty is that one first explicitly specifies the dependencies that may occur. This is especially useful to describe constants, but it also facilitates the description of other type theoretic features like dependent sums.


title: Canonical Typing and Pi-Conversion in the Barendregt Cube

authors:
Fairouz Kamareddine
Rob Nederpelt

abstract: Abstract In this article, we extend the Barendregt Cube with ∏-conversion (which is the analogue of β-conversion, on product type level) and study its properties. We use this extension to separate the problem of whether a term is typable from the problem of what is the type of a term.


title: Drawing Trees

abstract: Abstract This article describes the application of functional programming techniques to a problem previously studied by imperative programmers, that of drawing general trees automatically. We first consider the nature of the problem and the ideas behind its solution (due to Radack), independent of programming language implementation. We then describe a Standard ML program which reflects the structure of the abstract solution much better than an imperative language implementation. We conclude with an informal discussion on the correctness of the implementation and some changes which improve the algorithm's worst-case time complexity.


title: Type Classes with Existential Types

abstract: Abstract We argue that the novel combination of type classes and existential types in a single language yields significant expressive power. We explore this combination in the context of higher-order functional languages with static typing, parametric polymorphism, algebraic data types and Hindley–Milner type inference. Adding existential types to an existing functional language that already features type classes requires only a minor syntactic extension. We first demonstrate how to provide existential quantification over type classes by extending the syntax of algebraic data type definitions, and give examples of possible uses. We then develop a type system and a type inference algorithm for the resulting language. Finally, we present a formal semantics by translation to an implicitly-typed second-order λ-calculus and show that the type system is semantically sound. Our extension has been implemented in the Chalmers Haskell B. system, and all examples from this paper have been developed using this system.


title: Representing Demand by Partial Projections

authors:
John Launchbury
Gebreselassie Baraki

abstract: Abstract The projection-based strictness analysis of Wadler and Hughes is elegant and theoretically satisfying except in one respect: the need for lifting. The domains and functions over which the analysis is performed need to be transformed, leading to a less direct correspondence between analysis and program than might be hoped for. In this paper we shall see that the projection analysis may be reformulated in terms of partial projections, so removing this infelicity. There are additional benefits of the formulation: the two forms of information captured by the projection are distinguished, and the operational significance of the range of the projection fits exactly with the theory of unboxed types.


title: Deduction for Functional Programmers

authors:
James J. Leifer
Bernard Sufrin


title: A Syntactic Theory of Type Generativity and Sharing

abstract: Abstract This paper presents a purely syntactic account of type generativity and sharing – two key mechanisms in the SML module system – and shows its equivalence with the traditional stamp-based description of these mechanisms. This syntactic description recasts the SML module system in a more abstract, type-theoretic framework.


title: Note on Algol and Conservatively Extending Functional Programming

abstract: Abstract A simple Idealized Algol is considered, based on Reynolds's ‘essence of Algol’. It is shown that observational equivalence in this language conservatively extends observational equivalence in its assignment-free functional sublanguage.


title: Predictive Parser Combinators Need four Values to Report Errors

authors:
Andrew S. Partridge
David Wright

abstract: Abstract A combinator-based parser is a parser constructed directly from a BNF grammar, using higher-order functions (combinators) to model the alternative and sequencing operations of BNF. This paper describes a method for constructing parser combinators that can be used to build efficient predictive parsers which accurately report the cause of parsing errors. The method uses parsers that return values (parse trees or error indications) decorated with one of four tags.


title: New Dimensions in Heap Profiling

authors:
Colin Runciman
Niklas Röjemo

abstract: 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.


title: A Positive Supercompiler

authors:
Morten Heine Sørensen
Robert Glück
Neil D. Jones

abstract: Abstract We introduce a positive supercompiler , a version of Turchin's supercompiler maintaining only positive information during transformation, and using folding without generalization. The positive supercompiler can also be regarded as a variant of Wadler's deforestation maintaining an increased amount of information. We compare our algorithm to deforestation and, in less detail, to partial evaluation, Turchin's supercompiler, Generalized Partial Computation (GPC), and partial deduction by classifying these transformers by the amount of information they maintain during transformation. This factor is significant, as a differentiating example reveals: positive supercompilation, Turchin's supercompiler, GPC and partial deduction can specialize a general pattern matcher with respect to a fixed pattern to obtain an efficient matcher very similar to the Knuth–Morris–Pratt algorithm. Deforestation and traditional partial evaluation achieve this effect only after a non-trivial hand rewriting of the general matcher.


title: A Foundation for Actor Computation

authors:
Gul Agha
Ian A. Mason
Scott F. Smith
Carolyn L. Talcott

abstract: We present an actor language which is an extension of a simple functional language, and provide an operational semantics for this extension. Actor configurations represent open distributed systems, by which we mean that the specification of an actor system explicitly takes into account the interface with external components. We study the composability of such systems. We define and study various notions of testing equivalence on actor expressions and configurations. The model we develop provides fairness. An important result is that the three forms of equivalence, namely, convex, must, and may equivalences, collapse to two in the presence of fairness. We further develop methods for proving laws of equivalence and provide example proofs to illustrate our methodology.


title: A Competitive Algorithm for Managing Sharing in the Distributed Execution of Functional Programs

authors:
Gad Aharoni
Amnon Barak
Amir Ronen

abstract: Execution of functional programs on distributed-memory multiprocessors gives rise to the problem of evaluating expressions that are shared between several Processing Elements (PEs). One of the main difficulties of solving this problem is that, for a given shared expression, it is not known in advance whether realizing the sharing is more cost effective than duplicating its evaluation. Realizing the sharing requires coordination between the sharing PEs to ensure that the shared expression is evaluated only once. This coordination involves relatively high communication costs, and is therefore only worthwhile when the shared expressions require much computation time to evaluate. In contrast, when the shared expression is not computation intensive, it is more cost effective to duplicate the evaluation, and thus avoid the communication overhead costs. This dilemma of deciding whether to duplicate the work or to realize the sharing stems from the unknown computation time that is required to evaluate a shared expression. This computation time is difficult to estimate due to unknown run-time evolution of loops and recursion that may be part of the expression. This paper presents an on-line (run-time) algorithm that decides which of the expressions that are shared between several PEs should be evaluated only once, and which expressions should be evaluated locally by each sharing PE. By applying competitive considerations, the algorithm manages to exploit sharing of computation-intensive expressions, while it duplicates the evaluation of expressions that require little time to compute. The algorithm accomplishes this goal even though it has no a priori knowledge of the amount of computation that is required to evaluate the shared expression. We show that this algorithm is competitive with a hypothetical optimal off-line algorithm, which does have such knowledge, and we prove that the algorithm is deadlock free. Furthermore, this algorithm does not require any programmer intervention, it has low overhead, and it is designed to run on a wide variety of distributed systems.


title: Type and Behaviour Reconstruction for Higher-Order Concurrent Programs

authors:
Torben Amtoft
Flemming Nielson
Hanne Riis Nielson

abstract: In this paper we develop a sound and complete type and behaviour inference algorithm for a fragment of CML (Standard ML with primitives for concurrency). Behaviours resemble terms of a process algebra and yield a concise representation of the communications taking place during execution; types are mostly as usual except that function ypes and ‘delayed communication types’ are labelled by behaviours expressing the communications that will take place if the function is applied or the delayed action is activated. The development of the present paper improves a previously published algorithm in achieving completeness as well as soundness; this is due to an alternative strategy for generalising over types and behaviours.


title: Shrinking lambda Expressions in Linear Time

authors:
Andrew W. Appel
Trevor Jim

abstract: Functional-language compilers often perform optimizations based on beta and delta reduction. To avoid speculative optimizations that can blow up the code size, we might wish to use only shrinking reduction rules guaranteed to make the program smaller: these include dead-variable elimination, constant folding, and a restricted beta rule that inlines only functions that are called just once. The restricted beta rule leads to a shrinking rewrite system that has not previously been studied. We show some efficient normalization algorithms that are immediately useful in optimizing compilers; and we give a confluence proof for our system, showing that the choice of normalization algorithm does not affect final code quality.


title: The Call-By-Need lambda Calculus

authors:
Zena M. Ariola
Matthias Felleisen

abstract: Plotkin (1975) showed that the lambda calculus is a good model of the evaluation process for call-by-name functional programs. Reducing programs to constants or lambda abstractions according to the leftmost-outermost strategy exactly mirrors execution on an abstract machine like Landin's SECD machine. The machine-based evaluator returns a constant or the token closure if and only if the standard reduction sequence starting at the same program will end in the same constant or in some lambda abstraction. However, the calculus does not capture the sharing of the evaluation of arguments that lazy implementations use to speed up the execution. More precisely, a lazy implementation evaluates procedure arguments only when needed and then only once. All other references to the formal procedure parameter re-use the value of the first argument evaluation. The mismatch between the operational semantics of the lambda calculus and the actual behavior of the prototypical implementation is a major obstacle for compiler writers. Unlike implementors of the leftmost-outermost strategy or of a call-by-value language, implementors of lazy systems cannot easily explain the behavior of their evaluator in terms of source level syntax. Hence, they often cannot explain why a certain syntactic transformation ‘works’ and why another doesn't. In this paper we develop an equational characterization of the most popular lazy implementation technique – traditionally called ‘call-by-need’ – and prove it correct with respect to the original lambda calculus. The theory is a strictly smaller theory than Plotkin's call-by-name lambda calculus. Immediate applications of the theory concern the correctness proofs of a number of implementation strategies, e.g. the call-by-need continuation passing transformation and the realization of sharing via assignments. Some of this material first appeared in a paper presented at the 1995 ACM Conference on the Principles of Programming Languages. The paper was a joint effort with Maraist, Odersky and Wadler, who had independently developed a different equational characterization of call-by-need. We contrast our work with that of Maraist et al. in the body of this paper where appropriate.


title: Modularity of Strong Normalization in the Algebraic-lambda-Cube

authors:
Franco Barbanera
Maribel Fernández
Herman Geuvers

abstract: In this paper we present the algebraic-λ-cube, an extension of Barendregt's λ-cube with first- and higher-order algebraic rewriting. We show that strong normalization is a modular property of all the systems in the algebraic-λ-cube, provided that the first-order rewrite rules are non-duplicating and the higher-order rules satisfy the general schema of Jouannaud and Okada. We also prove that local confluence is a modular property of all the systems in the algebraic-λ-cube, provided that the higher-order rules do not introduce critical pairs. This property and the strong normalization result imply the modularity of confluence.


title: On Merging and Selection

abstract: Given two ascending lists xs and ys of combined length greater than n, consider the computation offormula hereThe standard function merge merges two ascending sequences and (!!) denotes list indexing. With a lazy evaluator the computation takes O(n) steps; with an eager one it takes O(p+q) steps, where p=length xs and q=length ys. Now in functional programming it is more efficient to index a tree than a list, so the question arises: can we find a faster solution if xs and ys are each represented by a tree? Somewhat surprisingly the answer is yes: if xs and ys are each represented by balanced binary search trees, then the computation can be reduced to O(log p+log q) steps. This is despite the fact that there is no known method for merging two binary search trees in better than linear time. The details, presented below, depend on a subtle relationship between merging and indexing.


title: On Building Trees with Minimum Height

abstract: A common solution to the problem of handling list indexing efficiently in a functional program is to build a binary tree. The tree has the given list as frontier and is of minimum height. Each internal node of the tree stores size information (actually, the size of its left subtree) to direct the search for an element at a given position in the frontier. One application was considered in my previous pearl (Bird, 1997). There are two complementary methods for building such a tree, both of which can be implemented in linear time. One method is ‘recursive’, or top down, and works by splitting the list into two equal halves, recursively building a tree for each half, and then combining the two results. The other method is ‘iterative’, or bottom up, and works by first creating a list of singleton trees, and then repeatedly combining the trees in pairs until just one tree remains. The two methods lead to different trees, but in each case the result is a tree with smallest possible height.