Richard Bird and I recently published our book Algorithm Design with Haskell with Cambridge University Press. This book can be seen as a sequel to Richard’s introductory textbook Thinking Functionally with Haskell: as well as being a textbook on algorithm design, it serves as a more advanced book on functional programming.

Our starting assumption was that algorithm design should be taught in a constructive way. Many textbooks take the form of a catalogue of famous algorithms (such as Kruskal’s and Prim’s algorithms for minimum-cost spanning trees), and some discussion of common techniques (such as greedy algorithms). They sometimes even give proofs of correctness of these algorithms. But mostly they do not address the design process: how do you get from a fresh problem statement to an algorithmic solution?

We took a constructive algorithmics approach, as espoused particularly by the mathematics of program construction community. Instead of thinking hard, inventing a program, then verifying that it implements its specification, one can calculate the program from its specification so that it is correct by construction. As well as increasing your confidence that the answer is correct, calculational techniques are a valuable foothold when you can’t immediately see what the answer should look like. After all, we don’t usually guess then verify the solution to a long division problem—we calculate the quotient and remainder from the dividend and divisor, following a repeatable process.

Our primary purpose in writing the book was to demonstrate that functional languages are a powerful vehicle for presenting both algorithm design techniques in general, and specific algorithmic developments in particular. This is in contrast to traditional textbooks on algorithm design, which are almost universally presented in an imperative style. It is sad that, even among undergraduate CS curricula that do include FP in the first place, most pay no attention to FP after the FP course is over—we are implicitly telling students that FP is only useful for FP courses, and not for anything else.

One advantage of a functional approach is that it is at a higher level: you deal holistically with a whole data structure rather than separately with each of its elements, using algebraic datatypes and higher-order operators. Another advantage is that you can conduct equational reasoning directly with programs, rather than having to sidestep into another formalism such as predicate calculus or Hoare logic. Programs are formal entities in their own right: why reason about them when you can reason with them?

The article is in three parts. In this part, Part 0, I’ll set the scene by exploring the difference between presenting developments in a functional style from doing so in an imperative style, illustrating with very simple examples. Part 1 presents some more interesting problems. But there is a catch, which we sort out in Part 2.

Imperative program design

Consider a very simple algorithm, namely summing the elements of an array. This seems very trivial, but please bear with me: I’ll go into detail in order to make comparisons later.

Given an array for , where does the following obvious looping program come from?

The canonical answer involves Hoare Logic, loop invariants, and weakest preconditions, beautifully laid out in the short book Programming: The Derivation of Algorithms by Anne Kaldewaij.

You could surely just have written the summing program from scratch, then subsequently maybe verified its correctness using loop invariants and so on. But being able to leap to the answer for simple problems is no help when it comes to more complicated problems: you need to understand the process even for simple cases, so that you can apply the same steps in more complicated cases.

For summing an array, one initial insight is needed: that the program requires a loop. Everything else can be deduced from there. Having decided that a loop is required, one first needs to come up with a loop invariant. A standard technique for doing so is to generalize one of the constants in the postcondition to a variable; here, we generalize constant to variable , and stipulate that varies from to :

The invariant is easily established by setting and , because then the range of the summation is empty. Moreover, the invariant together with the termination condition implies the postcondition; so for partial correctness it suffices to use as the loop guard—if this loop terminates, maintaining the invariant, then clearly it does so satisfying the postcondition. This leads to:

(Demonstrating that the loop does indeed terminate entails choosing also an integer-valued variant function, bounded below and decreasing on every iteration; for this program, we could use , which is bounded below by . In the interests of brevity, we skip this aspect.)

All that remains now is to complete the loop body, which starts with the invariant and loop guard both true, and must re-establish the invariant:

Clearly we can make progress by incrementing . The weakest precondition approach involves working backwards through a program, so let’s make the last statement in the loop body; what must be true before that, in order that the invariant holds afterwards? The weakest precondition rule for assignment says that we simply have to substitute for in the postcondition of the assignment (namely the loop invariant):

(The reason for working backwards is precisely the simplicity of this rule for assignment; counterintuitively, it’s not nearly so easy working forwards.) We have to achieve this state starting with the invariant and the guard, so it is helpful to massage this condition to make the second part look more like the invariant:

Since the invariant implies that , we are led to the assignment —because then the substitution rule for assignment (that is, substituting for in the above condition) tells us that we have only to establish

which follows already from the invariant.

Putting these pieces together gives the following justification for the loop:

Seen as a tableau like this, it is straightforward to verify Hoare’s conditions: each assignment establishes its postcondition, given its precondition, and so on. But it is not so straightforward to see how the tableau was developed. It’s like looking at a building, once the scaffolding used for construction has been taken down: it isn’t obvious how the builders got the roof on.

This simple example illustrates rigorously justified imperative program development. But it is quite painful to conduct, for at least two reasons. For one thing, it is very low level: we would rather deal with whole data structures such as the array than with individual scalar elements. And for a second thing, none of the work happens in the programming language—it all happens instead in the predicate calculus. The translation back and forth is unfortunate extra effort, and it would be much more convenient to be able to reason directly in terms of program texts. Fortunately, both pain points can be addressed by switching from an imperative to a functional style, as we shall now see.

Roll your own control structures

A functional approach deals with the first difficulty using algebraic or abstract datatypes and higher-order functions. In Haskell, for example, there is a datatype of lists, as values in their own right. The function that sums a list of integers can be written using explicit recursion:

That’s already a bit more concise than the imperative loop, because there is no need for the loop counter. But this pattern of recursion over lists is a common one: a constant () for the empty list; and for a non-empty list, a binary operator () to combine the head with the result of a recursive call on the tail. So it is helpful to abstract the pattern as a higher-order function:

and instantiate it for specific instances:

which is more concise still.

The standard function happens to be provided in the standard library, but there is nothing special about it—we could have defined it ourselves if it weren’t already there. Indeed, in our book, we defined various similar higher-order functions of our own. One is to aggregate the elements of a non-empty list. There is already another standard library function

(note that there is no clause for the empty list, so this function is defined only for non-empty lists). It uses a homogeneous (typically associative) binary operator , and therefore aggregates a list of values of one type to a result of the same type . But this was too specific for our application. So we simply defined another higher-order function, (for “ for non-empty lists”):

This can aggregate a list of values of one type to a sum of a different type.

Higher-order functions are extremely powerful for this reason: they effectively give you the power to “roll your own control structures”, if the standard ones don’t suit your purposes.

In an OO approach, you would use a library of collection classes and corresponding iterators and visitors instead of algebraic datatypes and higher-order functions. Algebraic datatypes such as lists are open abstractions, which makes it easy to add new operations over them. In contrast, OO classes are typically closed abstractions: clients can’t add new operations, and must interact through the fixed public interface—but conversely, providers can more easily add new representations. It’s a deliberate trade-off, with each approach having advantages over the other. But for a book on algorithm design and not about data structures, we would rather facilitate adding new operations than new representations.

Equational reasoning with programs

The second difficulty with the imperative style is that reasoning about programs does not take place in the programming language, but in the predicate calculus instead. Recall that the first step in developing the loop for summing an array was to replace the constant by a variable —but in the postcondition, not in any program. Similarly, the crucial step in developing the loop body is the transformation

—again, reasoning that happens in propositions about the program, not in the program text. In contrast, the defining characteristic of pure FP is referential transparency. This enables program manipulation by good old-fashioned equational reasoning, directly with program texts, without needing to step out into a distinct language such as predicate calculus.

In particular, the fundamental rule for reasoning about is the fusion law, which states

This combines a post-processing phase with an aggregation (using operators and ) into a single aggregation (using different operators and ). This can be done when the premises on the right-hand side can be satisfied—specifically, given and , when we can find an such that

for all . (The second conjunct of the right-hand side is easy to satisfy, just by letting be .)

For example, let

and consider

which sums the elements of a list and then doubles the result. The post-processing can be combined with the aggregation into a single pass:

This follows from the fusion law, with , , , , and . Clearly

and crucially, for arbitrary ,

No sidestep is needed into loop invariants and so on; equational reasoning with programs suffices. If you try to do the same thing with the imperative loop, you will need to work through the development with invariants and postconditions again, and all the reasoning will again be in predicate calculus rather than with programs.

Functional programming for algorithm design

Fusion is the driving force in many algorithmic developments: many problems have a simple specification written with standard components (maps, filters, folds, etc), and an efficient implementation can be obtained simply by equational reasoning using fusion. For example, a common form of specification is

as illustrated by minimum-cost spanning tree:

The aggregation step is often some form of selection, to select an optimal result. The generation step is often some combinatorial enumeration, such as permutations, segments, partitions, subsequences, or trees; these are usually neatly expressed using standard higher-order operators such as . Then the problem is to fuse the aggregation and testing with the generation.

Next steps

In Part 1 of this article, we’ll cover a more interesting class of programs, namely greedy algorithms, which appear to lend themselves nicely to the functional approach. However, there is a fly in the ointment. Many algorithmic problems are optimization problems, which are often under-determined: for example, there are typically several different minimum-cost spanning trees of the same graph. Proper treatment of these problems entails handling of nondeterminism. We found that the most lightweight way of achieving this—so that we could remain focussed on algorithms and not get bogged down in metatheory—was to step briefly and carefully outside pure FP, with just a small handful of nondeterministic functions. That challenge, and our solution to it, is the the main novelty in the book, and the subject of Part 2 of the article.

Bio: Jeremy Gibbons is Professor of Computing at the University of Oxford, where he leads the Algebra of Programming research group and is former Deputy Head of Department. He served as Vice Chair then Past Vice Chair of ACM SIGPLAN, with a particular focus on Open Access. He is also Editor-in-Chief of the Journal of Functional Programming, SC Chair of ICFP, on the Advisory Board of PACMPL, an editor of Compositionality, and former Chair of IFIP Working Group 2.1 on Algorithmic Languages and Calculi.

Disclaimer: These posts are written by individual contributors to share their thoughts on the SIGPLAN blog for the benefit of the community. Any views or opinions represented in this blog are personal, belong solely to the blog author and do not represent those of ACM SIGPLAN or its parent organization, ACM.