Although detractors of functional programming sometimes claim that functional programming is too difficult or counter-intuitive for most programmers to understand and use, evidence to the contrary can be found by looking at the popularity of spreadsheets. The spreadsheet paradigm, a first-order subset of the functional programming paradigm, has found wide acceptance among both programmers and end users. Still, there are many limitations with most spreadsheet systems. In this paper, we discuss language features that eliminate several of these limitations without deviating from the first-order, declarative evaluation model. The language used to illustrate these features is a research language called Forms/3. Using Forms/3, we show that procedural abstraction, data abstraction and graphics output can be supported in the spreadsheet paradigm. We show that, with the addition of a simple model of time, animated output and GUI I/O also become viable. To demonstrate generality, we also present an animated Turing machine simulator programmed using these features. Throughout the paper, we combine our discussion of the programming language characteristics with how the language features prototyped in Forms/3 relate to what is known about human effectiveness in programming.

Launchbury and Peyton Jones came up with an ingenious idea for embedding regions of imperative programming in a pure functional language like Haskell. The key idea was based on a simple modification of Hindley-Milner's type system. Our first contribution is to propose a more natural encapsulation construct exploiting higher-order kinds, which achieves the same encapsulation effect, but avoids the ad hoc type parameter of the original proposal. The second contribution is a type safety result for encapsulation of strict state using both the original encapsulation construct and the newly introduced one. We establish this result in a more expressive context than the original proposal, namely in the context of the higher-order lambda-calculus. The third contribution is a type safety result for encapsulation of lazy state in the higher-order lambda-calculus. This result resolves an outstanding open problem on which previous proof attempts failed. In all cases, we formalize the intended implementations as simple big-step operational semantics on untyped terms, which capture interesting implementation details not captured by the reduction semantics proposed previously.

This paper is an exploration of the parallel graph reduction approach to parallel functional programming, illustrated by a particular example: pipelined, dynamically-scheduled implementation of search, updates and read-modify-write transactions on an in-store binary search tree. We use program transformation, execution-driven simulation and analytical modelling to expose the maximum potential parallelism, the minimum communication and synchronisation overheads, and to control the overall space requirement. We begin with a lazy functional program specifying a series of transactions on a binary tree, each involving several searches and updates, in a side-effect-free fashion. Transformation of the source code produces a formulation of the program with greater locality and larger grain size than can be achieved using naive parallelization methods, and we show that, with care, these tasks can be scheduled effectively. Even with a workload using random keys, significant spatial locality is found, and we evaluate a modified cache coherency protocol which avoids false sharing so that large cache lines can be used to minimise the number of messages required. As expected with a pipeline, the application should reach a steady state as soon as the first transaction is completed. However, if the network latency is too large, the rate of completion lags behind the rate at which work is admitted, and internal queues grow without bound. We determine the conditions under which this occurs, and show how it can be avoided while maximising speedup.

Algorithms can be dramatically affected by the language in which they are implemented. An algorithm that is elegant and efficient in one language may be ugly and inefficient in another. If you have ever attempted to implement an assignment-intensive algorithm in a functional programming language, you are probably more familiar with this phenomenon than you ever wanted to be! But this sword does not cut in only one direction. Functional programming languages are wonderfully suited to expressing certain kinds of algorithms in a clean, modular way, and researchers over the last five to ten years have greatly expanded the range of algorithms for which this is true.

This issue of the Journal of Functional Programming is dedicated to work presented at the Workshop on Implicit Computational Complexity in Programming Languages, affiliated with the 1998 meeting of the International Conference on Functional Programming in Baltimore.

Several machine-independent approaches to computational complexity have been developed in recent years; they establish a correspondence linking computational complexity to conceptual and structural measures of complexity of declarative programs and of formulas, proofs and models of formal theories. Examples include descriptive complexity of finite models, restrictions on induction in arithmetic and related first order theories, complexity of set-existence principles in higher order logic, and specifications in linear logic. We refer to these approaches collectively as Implicit Computational Complexity. This line of research provides a framework for a streamlined incorporation of computational complexity into areas such as formal methods in software development, programming language theory, and database theory.

A fruitful thread in implicit computational complexity is based on exploring the computational complexity consequences of introducing various syntactic control mechanisms in functional programming, including restrictions (akin to static typing) on scoping, data re-use (via linear modalities), and iteration (via ramification of data). These forms of control, separately and in combination, can certify bounds on the time and space resources used by programs. In fact, all results in this area establish that each restriction considered yields precisely a major computational complexity class. The complexity classes thus obtained range from very restricted ones, such as NC and Alternating logarithmic time, through the central classes Poly-Time and Poly-Space, to broad classes such as the Elementary and the Primitive Recursive functions.

Considerable effort has been invested in recent years to relax as much as possible the structural restrictions considered, allowing for more exible programming and proof styles, while still guaranteeing the same resource bounds. Notably, more exible control forms have been developed for certifying that functional programs execute in Poly-Time.

The 1998 workshop covered both the theoretical foundations of the field and steps toward using its results in various implemented systems, for example in controlling the computational complexity of programs extracted from constructive proofs. The five papers included in this issue nicely represent this dual concern of theory and practice. As they are going to print, we should note that the field of Implicit Computational Complexity continues to thrive: successful workshops dedicated to it were affiliated with both the LICS'99 and LICS'00 conferences. Special issues, of Information and Computation dedicated to the former, and of Theoretical Computer Science to the latter, are in preparation.

Many polyvariant program analyses have been studied in the 1990s, including k-CFA, polymorphic splitting, and the cartesian product algorithm. The idea of polyvariance is to analyze functions more than once and thereby obtain better precision for each call site. In this paper we present an equivalence theorem which relates a co-inductively-defined family of polyvariant flow analyses and a standard type system. The proof embodies a way of understanding polyvariant flow information in terms of union and intersection types, and, conversely, a way of understanding union and intersection types in terms of polyvariant flow information. We use the theorem as basis for a new flow-type system in the spirit of the λCIL-calculus of Wells, Dimock, Muller and Turbak, in which types are annotated with flow information. A flow-type system is useful as an interface between a flow-analysis algorithm and a program optimizer. Derived systematically via our equivalence theorem, our flow-type system should be a good interface to the family of polyvariant analyses that we study.

Destructive array update optimization is critical for writing scientific codes in functional languages. We present set constraints for an interprocedural update optimization that runs in polynomial time. This is a multi-pass optimization, involving interprocedural flow analyses for aliasing and liveness. We characterize and prove the soundness of these analyses using small-step operational semantics. We also prove that any sound liveness analysis induces a correct program transformation.

First-order languages based on rewrite rules share many features with functional languages, but one difference is that matching and rewriting can be made much more expressive and powerful by incorporating some built-in equational theories. To provide reasonable programming environments, compilation techniques for such languages based on rewriting have to be designed. This is the topic addressed in this paper. The proposed techniques are independent from the rewriting language, and may be useful to build a compiler for any system using rewriting modulo Associative and Commutative (AC) theories. An algorithm for many-to-one AC matching is presented, that works efficiently for a restricted class of patterns. Other patterns are transformed to fit into this class. A refined data structure, namely compact bipartite graph, allows encoding of all matching problems relative to a set of rewrite rules. A few optimisations concerning the construction of the substitution and of the reduced term are described. We also address the problem of non-determinism related to AC rewriting, and show how to handle it through the concept of strategies. We explain how an analysis of the determinism can be performed at compile time, and we illustrate the benefits of this analysis for the performance of the compiled evaluation process. Then we briefly introduce the ELAN system and its compiler, in order to give some experimental results and comparisons with other languages or rewrite engines.

From the points of view of programming pragmatics, rewriting and operational semantics, the syntactic construct used for exception handling in ML-like programming languages, and in much theoretical work on exceptions, has subtly undesirable features. We propose and discuss a more well-behaved construct.

This article describes the implementation of a debugger for lazy functional languages like Haskell. The key idea is to construct a declarative trace which hides the operational details of lazy evaluation. However, to avoid excessive memory consumption, the trace is constructed one piece at a time, as needed during a debugging session, by automatic re-execution of the program being debugged. The article gives a fairly detailed account of both the underlying ideas and of our implementation, and also presents performance figures which demonstrate the feasibility of the approach.

Triangulations of a surface are of fundamental importance in computational geometry, computer graphics, and engineering and scientific simulations. Triangulations are ordinarily represented as mutable graph structures for which both adding and traversing edges take constant time per operation. These representations of triangulations make it difficult to support persistence, including ‘multiple futures’, the ability to use a data structure in several unrelated ways in a given computation; ‘time travel’, the ability to move freely among versions of a data structure; or parallel computation, the ability to operate concurrently on a data structure without interference. We present a purely functional interface and representation of triangulated surfaces, and more generally of simplicial complexes in higher dimensions. In addition to being persistent in the strongest sense, the interface more closely matches the mathematical definition of triangulations (simplicial complexes) than do interfaces based on mutable representations. The representation, however, comes at the cost of requiring O(lg n) time for traversing or adding triangles (simplices), where n is the number of triangles in the surface. We show both analytically and experimentally that for certain important cases, this extra cost does not seriously affect end-to-end running time. Analytically, we present a new randomized algorithm for 3-dimensional Convex Hull based on our representations for which the running time matches the Ω(n lg n) lower-bound for the problem. This is achieved by using only O(n) traversals of the surface. Experimentally, we present results for both an implementation of the 3-dimensional Convex Hull and for a terrain modeling algorithm, which demonstrate that, although there is some cost to persistence, it seems to be a small constant factor.

This paper describes the Automated Complexity Analysis Prototype (ACAp) system for automated complexity analysis of functional programs synthesized with the Nuprl proof development system. We define a simple abstract cost model for NUPRL's term language based on the current call-by-name evaluator. The framework uses abstract functions and abstract lists to facilitate reasoning about primitive recursive programs with first-order functions, lazy lists and a subclass of higher-order functions. The ACAp system automatically derives upper bounds on the time complexity of NUPRL extracts relative to a given profiling semantics. Analysis proceeds by abstract interpretation of the extract, where symbolic evaluation rules extend standard evaluation to terms with free variables. Symbolic evaluation of recursive programs generates systems of multi-variable difference equations, which are solved using the MATHEMATICA computer algebra system. The use of the system is exemplified by analyzing a proof extract that computes the maximum segment sum of a list and a functional program that determines the minimum of a list via sorting. For both results, we compare call-by-name to call-by-value evaluation.

In higher-order abstract syntax, the variables and bindings of an object language are represented by variables and bindings of a meta-language. Let us consider the simply typed λ-calculus as object language and Haskell as meta-language. For concreteness, we also throw in integers and addition, but only in this section.

A fair amount has been written on the subject of reasoning about pointer algorithms. There was a peak about 1980 when everyone seemed to be tackling the formal verification of the Schorr–Waite marking algorithm, including Gries (1979, Morris (1982) and Topor (1979). Bornat (2000) writes: “The Schorr–Waite algorithm is the first mountain that any formalism for pointer aliasing should climb”. Then it went more or less quiet for a while, but in the last few years there has been a resurgence of interest, driven by new ideas in relational algebras (Möeller, 1993), in data refinement Butler (1999), in type theory (Hofmann, 2000; Walker and Morrisett, 2000), in novel kinds of assertion (Reynolds, 2000), and by the demands of mechanised reasoning (Bornat, 2000). Most approaches end up being based in the Floyd–Dijkstra–Hoare tradition with loops and invariant assertions. To be sure, when dealing with any recursively-defined linked structure some declarative notation has to be brought in to specify the problem, but no one to my knowledge has advocated a purely functional approach throughout. Mason (1988) comes close, but his Lisp expressions can be very impure. Möller (1999) also exploits an algebraic approach, and the structure of his paper has much in common with what follows.

This pearl explores the possibility of a simple functional approach to pointer manipulation algorithms.

Here are two puzzles for you to solve. First, consider the binary tree in figure 1. Take a pencil (I am assuming that this is your personal copy of JFP!) and mark some of the nodes in such a way that the sum of the values of marked nodes is as large as possible. The catch is that you cannot mark all the nodes: if you mark a node, then you are not allowed to mark its parent. Equivalently, no two marked nodes can be contiguous in the tree.

The second puzzle is similar though both the datatype and constraint are different. Consider the rose tree of figure 2 (a rose tree is a tree with arbitrary branching structure). Mark some of the nodes so that all marked nodes are now contiguous in the tree. For example, if you mark the root value 4 and the leaf value 1, then you must also mark the values 5 and −3 along the path from 4 to 1. Again the idea is to maximise the sum of the marked nodes. Of course, if all values were nonnegative, the best solution would be to mark all nodes. But they aren't and the maximum sum is obtained only by a judicious choice of marking. Answers to both puzzles are given at the end of the paper.

The Maximum Marking Problem (MMP) is the problem of marking the entries of some given data structure in such a way that a given constraint is satisfied and the sum of the values associated with marked entries is as large as possible. By the end of this pearl, you will be convinced that there is a linear-time solution for both the puzzles described above.

We propose a new style of writing graph algorithms in functional languages which is based on an alternative view of graphs as inductively defined data types. We show how this graph model can be implemented efficiently, and then we demonstrate how graph algorithms can be succinctly given by recursive function definitions based on the inductive graph view. We also regard this as a contribution to the teaching of algorithms and data structures in functional languages since we can use the functional-style graph algorithms instead of the imperative algorithms that are dominant today.

We study the effect of polynomial interpretation termination proofs of deterministic (resp. non-deterministic) algorithms defined by con uent (resp. non-con uent) rewrite systems over data structures which include strings, lists and trees, and we classify them according to the interpretations of the constructors. This leads to the definition of six function classes which turn out to be exactly the deterministic (resp. non-deterministic) polynomial time, linear exponential time and linear doubly exponential time computable functions when the class is based on con uent (resp. non-con uent) rewrite systems. We also obtain a characterisation of the linear space computable functions. Finally, we demonstrate that functions with exponential interpretation termination proofs are super-elementary.

This article describes a general framework for designing purely functional datatypes that automatically satisfy given size or structural constraints. Using the framework we develop implementations of different matrix types (for example, square matrices) and implementations of several tree types (for example, Braun trees and 2-3 trees). Consider representing square n×n matrices. The usual representation using lists of lists fails to meet the structural constraints: there is no way to ensure that the outer list and the inner lists have the same length. The main idea of our approach is to solve in a first step a related, but simpler problem, namely to generate the multiset of all square numbers. To describe this multiset we employ recursion equations involving finite multisets, multiset union, addition and multiplication lifted to multisets. In a second step we mechanically derive from these recursion equations datatype definitions that enforce the ‘squareness’ constraint. The transformation makes essential use of parameterized types.

Compare first-order functional programs with higher-order programs allowing functions as function parameters. Can the the first program class solve fewer problems than the second? The answer is no: both classes are Turing complete, meaning that they can compute all partial recursive functions. In particular, higher-order values may be first-order simulated by use of the list constructor ‘cons’ to build function closures. This paper uses complexity theory to prove some expressivity results about small programming languages that are less than Turing complete. Complexity classes of decision problems are used to characterize the expressive power of functional programming language features. An example: second-order programs are more powerful than first-order, since a function f of type [Bool]-〉Bool is computable by a cons-free first-order functional program if and only if f is in PTIME, whereas f is computable by a cons-free second-order program if and only if f is in EXPTIME. Exact characterizations are given for those problems of type [Bool]-〉Bool solvable by programs with several combinations of operations on data: presence or absence of constructors; the order of data values: 0, 1, or higher; and program control structures: general recursion, tail recursion, primitive recursion.