My mentor, colleague, and friend Richard Bird died in April 2022 after a long battle with cancer. I wrote an obituary of him for The Guardian, his favoured newspaper; this post is a hybrid of that obituary and a eulogy I delivered at his funeral.

Richard was born in 1943 in London. His parents Kay and Jack were landlords of a series of pubs in South London. Richard attended St Olave’s Grammar School, then matriculated to read mathematics at Cambridge in 1960. After graduation, he had a brief spell working in sales for International Computers and Tabulators, the mainframe computer company that eventually became ICL. He was evidently effective in this role, being as personable as he was; but it involved flying around the country in small planes, which Richard did not enjoy at all. No amount of money or approval could persuade him to stay, so he left after a year to do postgraduate study at the University of London Institute of Computer Science.

Richard met Norma Lapworth at a friend’s 21st birthday party. Norma trained as an ecologist, later becoming a teacher, education advisor, and Ofsted schools inspector. Richard and Norma married in 1967.

After a year lecturing in Vancouver 1971-1972, Richard and Norma returned to the UK for Richard to take up a lectureship at the University of Reading. He was given the time finally to complete his PhD thesis, on Computational Complexity on Register Machines, in 1973. But Reading was a rather linguistically oriented department, which did not suit Richard’s mathematical temperament. So he leapt at the opportunity to join Tony Hoare’s expanding Programming Research Group at Oxford University Computing Laboratory in 1983. He was appointed as a University Lecturer in Computation, with a non-tutorial fellowship at St Cross College, assuming responsibility as Director of the MSc in Computation. He moved to a Tutorial Fellowship at Lincoln College in 1988. Richard stayed at the PRG for the remainder of his career, being promoted to Reader in Computation in 1990 and then to Professor in 1996, serving as Director of OUCL from 1998 to 2003, and finally retiring in 2008 after 25 years.

Richard’s research area was functional programming—an approach to computer programming centred around obeying the conventions of traditional mathematics. To Richard, it was self-evident that programs are mathematical entities, and that you can manipulate them in precisely the same way as you do quadratic equations. No immediate need for consideration of the capabilities of computer hardware; no entanglement in the vagaries of specific programming languages. Just algebra, pure and simple.

His PhD thesis in the early 1970s was already concerned with program transformation: the rules by which one program is shown to be equivalent to another. He wasn’t so interested in the program you actually end up with, so much as the process by which you got there, and how you know you ended up in the right place, and what alternative directions you didn’t follow en route. Specifically, he was interested in the calculus of equivalences with which you could conduct equational reasoning on programs, just as in high-school algebra.

In 1980 he was invited to participate in IFIP Working Group 2.1 on Algorithmic Languages and Calculi. This was the group that had designed the seminal programming language Algol68, and that continues to research into notations and techniques for designing and describing algorithms today. Richard had a very fruitful collaboration in WG2.1 with Lambert Meertens from the CWI at Amsterdam, developing what came to be known as the Bird-Meertens Formalism, or Squiggol to its friends. This was a concise and somewhat cryptic algebraic program notation with a powerful accompanying corpus of theorems, supporting the equational reasoning style that Richard sought.

Richard is known and respected around the world for his elegant writing. He published about 100 scientific papers in his life—not especially prolific for a scientist, but every one of those papers was very well polished. He also wrote or co-wrote seven books, starting with Programs and Machines (1976), which featured among other constructions a machine called NoRMa, the Number-Theoretic Register Machine.

I won’t go through all seven books, much as I would like to; I will just pick out a few highlights. Richard’s second book, Introduction to Functional Programming (1988, with Phil Wadler), set out his vision for teaching functional programming. Many people love this book. Graham Hutton wrote to me to say:

Richard set the standards for elegance and clarity, and the original Bird & Wadler is my all-time favourite book. It still stands up today as one of the best programming books ever written—every page is a gem.

Richard’s next book, Algebra of Programming (1996, with Oege de Moor), was much more research-oriented, extending his Squiggol agenda from functions to relations. Tim Sears tweeted:

This book blew my mind regarding what the relationship could be between math, programming and systems. I never met Richard, but his work has had a profound impact on me.

Richard’s fifth book Pearls of Functional Algorithm Design collected and repolished some of the Functional Pearls he had published over the years. These Pearls emulated Jon Bentley’s famous Programming Pearls column in CACM in the 1980s. Bentley explained:

Just as natural pearls grow from grains of sand that have irritated oysters, these programming pearls have grown from real problems that have irritated programmers. The programs are fun, and they teach important programming techniques and fundamental design principles.

Richard established and was the founding editor of the Functional Pearls column, from the very first issue in 1991 of the Journal of Functional Programming until he retired in 2008. He characterized Functional Pearls as “polished, elegant, instructive, entertaining”. He had high standards for them: he advised reviewers to

stop reading when you get bored, or the material gets too complicated, or too much specialist knowledge is needed, or the writing is bad.

He gave a keynote lecture about Pearls in 2006, where he observed that “most of them need more time in the oyster”.

Functional Pearls are the epitome of Richard’s writing style. Erik Meijer called him “the poet laureate of functional programming”. Greg Fitzgerald tweeted that

When life got hard, I’d read his pearls to settle my mind. His proofs read like poetry.

Ed Kmett commented that Richard’s pearls book

is the only real clear exposition of how to think like a functional programmer that I’ve ever seen

I was honoured to be Richard’s co-author on his final book, Algorithm Design with Haskell, written during his illness and published in 2020. Working with him was always a joy.

Despite the global influence of his publications, Richard always saw teaching as his main duty, and research as something he did for relaxation. Andrew Ker thanked Richard for the way he had taught him as a first-year undergraduate—a way which Andrew has passed on to his own students, and which he now sees them repeating in turn. Andrew wrote:

I’ve come to see that passing on our knowledge to the next generation is the most important thing we do, even more than generating new knowledge through research. And the ideas and attitudes persist through the generations. Your influence and example extends far beyond what you know, and countless students are grateful for it.

My own favourite Richard story is a teaching one. Richard was giving a tutorial about algorithm analysis: how many steps does this program take—for example, something about processing hierarchical tree-shaped data? You’d expect a question about counting steps to have an answer in whole numbers; but in fact, the answer often involves logarithms. One student asked why this was. Richard thought for a moment, then said “logs come from trees”. The students broke out in laughter, and it took Richard a while to work out why. In fact, I think this was Richard’s own favourite Richard story too, because I know that he continued to tell it in tutorials for years afterwards.

I want to close by mentioning Richard’s openness, considerateness, and egalitarianism. The departmental secretaries always looked forward to him coming in, because he treated them with the same friendliness that he treated the most eminent of his colleagues. Several once-overawed students have written to me to express gratitude for his welcome—“no Herr Professor Doktor Doktor here, we are all colleagues”—and for helping them to find their own way.

Richard’s collaborator Lambert Meertens says:

His lectures were a joy to attend, because of their clarity and the entertaining delivery. But I’ll remember him at least as much for his kindness, his generosity, his warm interest in people’s wellbeing—expressed not only in words, but also deeds.

Cezar Ionescu remembers being apprehensive about first meeting Richard at WG2.1—you should never meet your heroes—but says he

was exactly the way I had imagined him to be: very sharp, funny, wise. We talked about opera and Shakespeare, and fought (and won!) a hard battle for tap water with the hotel staff.

My own involvement with Richard started when I applied in 1987 to do a DPhil at Oxford, on a project that turned out to have finished by the time I arrived. I rattled around the Lab for a year, not even seeing my official supervisor. But Richard invited me to join his weekly Problem Solving Club. He took me under his wing, and I have never looked back. He became my DPhil supervisor, then some years later hired me into my current position, and I am privileged to have been able to call him my colleague and my friend. I basically owe him my whole career, and I have no words sufficient to convey my gratitude to him. I will miss him greatly.

The “Sieve of Eratosthenes” is often used as a nice example of the expressive power of streams (infinite lazy lists) and list comprehensions:

That is, takes a stream of candidate primes; the head of this stream is a prime, and the remaining primes are obtained by removing all multiples of from the candidates and sieving what’s left. (It’s also a nice unfold.)

Unfortunately, as Melissa O’Neill observes, this nifty program is not the true Sieve of Eratosthenes! The problem is that for each prime , every remaining candidate is tested for divisibility. O’Neill calls this bogus common version “trial division”, and argues that the Genuine Sieve of Eratosthenes should eliminate every multiple of without reconsidering all the candidates in between. That is, only of the natural numbers are touched when eliminating multiples of 2, less than of the remaining candidates for multiples of 3, and so on. As an additional optimization, it suffices to eliminate multiples of starting with , since by that point all composite numbers with a smaller nontrivial factor will already have been eliminated.

O’Neill’s paper presents a purely functional implementation of the Genuine Sieve of Eratosthenes. The tricky bit is keeping track of all the eliminations when generating an unbounded stream of primes, since obviously you can’t eliminate all the multiples of one prime before producing the next prime. Her solution is to maintain a priority queue of iterators; indeed, the main argument of her paper is that functional programmers are often too quick to use lists, when other data structures such as priority queues might be more appropriate.

O’Neill’s paper was published as a Functional Pearl in the Journal of Functional Programming, when Richard Bird was the handling editor for Pearls. The paper includes an epilogue that presents a purely list-based implementation of the Genuine Sieve, contributed by Bird during the editing process. And the same program pops up in Bird’s textbook Thinking Functionally with Haskell (TFWH). This post is about Bird’s program.

The Genuine Sieve, using lists

Bird’s program appears in §9.2 of TFWH. It deals with lists, but these will be infinite, sorted, duplicate-free streams, and you should think of these as representing infinite sets, in this case sets of natural numbers. In particular, there will be no empty or partial lists, only properly infinite ones.

Now, the prime numbers are what you get by eliminating the composite numbers from the “plural” naturals (those greater than one), and the composite numbers are the proper multiples of the primes—so the program is cleverly cyclic:

We’ll come back in a minute to , which unions a set of sets to a set; but is the obvious implementation of list difference of sorted streams (hence, representing set difference):

and generates the multiples of starting with :

Thus, the composites are obtained by merging together the infinite stream of infinite streams . You might think that you could have defined instead , but this doesn’t work: this won’t compute the first prime without first computing some composites, and you can’t compute any composites without at least the first prime, so this definition is unproductive. Somewhat surprisingly, it suffices to “prime the pump” (so to speak) just with 2, and everything else flows freely from there.

Returning to , here is the obvious implementation of , which merges two sorted duplicate-free streams into one (hence, representing set union):

Then is basically a stream fold with . You might think you could define this simply by , but again this is unproductive. After all, you can’t merge the infinite stream of sorted streams into a single sorted stream, because there is no least element. Instead, we have to exploit the fact that we have a sorted stream of sorted streams; then the binary merge can exploit the fact that the head of the left stream is the head of the result, without even examining the right stream. So, we define:

This program is now productive, and yields the infinite sequence of prime numbers, using the genuine algorithm of Eratosthenes.

Approximation Lemma

Bird uses the cyclic program as an illustration of the Approximation Lemma. This states that for infinite lists , ,

where

Note that is undefined; the function preserves the outermost constructors of a list, but then chops off anything deeper and replaces it with (undefined). So, the lemma states that to prove two infinite lists equal, it suffices to prove equal all their finite approximations.

Then to prove that does indeed produce the prime numbers, it suffices to prove that

for all , where is the th prime (so ). Bird therefore defines

and claims that

To prove the claim, he observes that it suffices for to be well defined at least up to the first composite number greater than , because then delivers enough composite numbers to supply , which will in turn supply , and so on. It is a “non-trivial result in Number Theory” (in fact, a consequence of Bertrand’s Postulate) that ; therefore it suffices that

where is the th composite number (so ) and . Completing the proof is set as Exercise 9.I of TFWH, and Answer 9.I gives a hint about using induction to show that is the result of merging with . (Incidentally, there is a typo in TFWH: both the body of the chapter and the exercise and its solution have “” instead of “”.)

Unfortunately, the hint in Answer 9.I is simply wrong. For example, it implies that (which equals ) could be constructed from (which equals ) and (which equals ); but this means that the 6 and 8 would have to come out of nowhere. Nevertheless, the claim in Exercise 9.I is valid. What should the hint for the proof have been?

Fixing the proof

The problem is made tricky by the cyclicity. Tom Schrijvers suggested to me to break the cycle by defining

so that ; this allows us to consider in isolation from . In fact, I claim (following a suggestion generated by Geraint Jones and Guillaume Boisseau at our Algebra of Programming research group) that if where , then has a well-defined prefix consisting of all the composite numbers such that and is a multiple of some with , in ascending order, then becomes undefined. That’s not so difficult to see from the definition: contains the multiples of starting from ; all these streams get merged; but the result gets undefined (in ) once we pass the head of the last stream. In particular, has a well-defined prefix consisting of all the composites up to , then becomes undefined, as required.

However, I must say that I still find this argument unsatisfactory: I have no equational proof about the behaviour of . In fact, I believe that the Approximation Lemma is unsufficient to provide such a proof: works along the grain of , but against the grain of . I believe we want something instead like an “Approx While Lemma”, where is to as is to :

Thus, retains elements of as long as they satisfy , but becomes undefined as soon as they don’t (or when the list runs out). Then for all sorted, duplicate-free streams and unbounded streams (that is, ),

The point is that works conveniently for and and hence for too. I am now working on a proof by equational reasoning of the correctness (especially the productivity) of the Genuine Sieve of Eratosthenes…

I recently attended the Matthias Felleisen Half-Time Show, a symposium held in Boston on 3rd November in celebration of Matthias’s 60th birthday. I was honoured to be able to give a talk there; this post is a record of what I (wished I had) said.

Matthias Felleisen

Matthias is known for many contributions to the field of Programming Languages. He received the SIGPLAN Programming Languages Achievement Award in 2012, the citation for which states:

He introduced evaluation contexts as a notation for specifying operational semantics, and progress-and-preservation proofs of type safety, both of which are used in scores of research papers each year, often without citation. His other contributions include small-step operational semantics for control and state, A-normal form, delimited continuations, mixin classes and mixin modules, a fully-abstract semantics for Sequential PCF, web programming techniques, higher-order contracts with blame, and static typing for dynamic languages.

Absent from this list, perhaps because it wasn’t brought back into the collective memory until 2013, is a very early presentation of the idea of using effects and handlers for extensible language design.

However, perhaps most prominent among Matthias’s contributions to our field is a long series of projects on teaching introductory programming, from TeachScheme! through Program By Design to a latest incarnation in the form of the How to Design Programs textbook (“HtDP”), co-authored with Robby Findler, Matthew Flatt, and Shriram Krishnamurthi, and now in its second edition. The HtDP book is my focus in this post; I have access only the First Edition, but the text of the Second Edition is online. I make no apologies for using Haskell syntax in my examples, but at least that gave Matthias something to shout at!

Design Recipes

One key aspect of HtDP is the emphasis on design recipes for solving programming tasks. A design recipe is a template for the solution to a problem: a contract for the function, analogous to a type signature (but HtDP takes an untyped approach, so this signature is informal); a statement of purpose; a function header; example inputs and outputs; and a skeleton of the function body. Following the design recipe entails completing the template—filling in a particular contract, etc—then fleshing out the function body from its skeleton, and finally testing the resulting program against the initial examples.

The primary strategy for problem solving in the book is via analysis of the structure of the input. When the input is composite, like a record, the skeleton should name the available fields as likely ingredients of the solution. When the input has “mixed data”, such as a union type, the skeleton should enumerate the alternatives, leading to a case analysis in the solution. When the input is of a recursive type, the skeleton encapsulates structural recursion—a case analysis between the base case and the inductive case, the latter case entailing recursive calls.

So, the design recipe for structural recursion looks like this:

Phase	Goal	Activity
Data Analysis and Design	to formulate a data definition	develop a data definition for mixed data with at least two alternatives; one alternative must not refer to the definition; explicitly identify all self-references in the data definition
Contract Purpose and Header	to name the function; to specify its classes of input data and its class of output data; to describe its purpose; to formulate a header	name the function, the classes of input data, the class of output data, and specify its purpose: ;; name : in1 in2 … –> out ;; to compute … from x1 … (define (name x1 x2 …) …)
Examples	to characterize the input-output relationship via examples	create examples of the input-output relationship; make sure there is at least one example per subclass
Template	to formulate an outline	develop a cond-expression with one clause per alternative; add selector expressions to each clause; annotate the body with natural recursions; Test: the self-references in this template and the data definition match!
Body	to define the function	formulate a Scheme expression for each simple cond-line; explain for all other cond-clauses what each natural recursion computes according to the purpose statement
Test	to discover mistakes (“typos” and logic)	apply the function to the inputs of the examples; check that the outputs are as predicted

The motivating example for structural recursion is Insertion Sort: recursing on the tail of a non-empty list and inserting the head into the sorted subresult.

A secondary, more advanced, strategy is to use generative recursion, otherwise known as divide-and-conquer. The skeleton in this design recipe incorporates a test for triviality; in the non-trivial cases, it splits the problem into subproblems, recursively solves the subproblems, and assembles the subresults into an overall result. The motivating example for generative recursion is QuickSort (but not the fast in-place version): dividing a non-empty input list into two parts using the head as the pivot, recursively sorting both parts, and concatenating the results with the pivot in the middle.

As far as I can see, no other program structures than structural recursion and generative recursion are considered in HtDP. (Other design recipes are considered, in particular accumulating parameters and imperative features. But these do not determine the gross structure of the resulting program. In fact, I believe that the imperative recipe has been dropped in the Second Edition.)

Co-programs

My thesis is that HtDP has missed an opportunity to reinforce its core message, that data structure determines program structure. Specifically, I believe that the next design recipe to consider after structural recursion, in which the shape of the program is determined by the shape of the input, should be structural corecursion, in which the shape of the program is determined instead by the shape of the output.

More concretely, a function that generates “mixed output”—whether that is a union type, or simply a boolean—might be defined by case analysis over the output. A function that generates a record might be composed of subprograms that generate each of the fields of that record. A function that generates a recursive data structure from some input data might be defined with a case analysis as to whether the result is trivial, and for non-trivial cases with recursive calls to generate substructures of the result. HtDP should present explicit design recipes to address these possibilities, as it does for program structures determined by the input data.

For an example of mixed output, consider a program that may fail, such as division, guarded so as to return an alternative value in that case:

The program performs a case analysis, and of course the analysis depends on the input data; but the analysis is not determined by the structure of the input, only its value. So a better explanation of the program structure is that it is determined by the structure of the output data.

For an example of generating composite output, consider the problem of extracting a date, represented as a record:

from a formatted string. The function is naturally structured to match the output type:

For an example of corecursion, consider the problem of “zipping” together two input lists to a list of pairs—taking and to , and for simplicity let’s say pruning the result to the length of the shorter input. One can again solve the problem by case analysis on the input, but the fact that there are two inputs makes that a bit awkward—whether to do case analysis on one list in favour of the other, or to analyse both in parallel. For example, here is the outcome of case analysis on the first input, followed if that is non-empty by a case analysis on the second input:

Case analysis on both inputs would lead to four cases rather than three, which would not be an improvement. One can instead solve the problem by case analysis on the output—and it is arguably more natural to do so, because there is only one output rather than two. When is the output empty? (When either input is empty.) If it isn’t empty, what is the head of the output? (The pair of input heads.) And from what data is the tail of the output recursively constructed? (The pair of input tails.)

And whereas Insertion Sort is a structural recursion over the input list, inserting elements one by one into a sorted intermediate result, Selection Sort is a structural corecursion towards the output list, repeatedly extracting the minimum remaining element as the next element of the output: When is the output empty? (When the input is empty.) If the output isn’t empty, what is its head? (The minimum of the input.) And from what data is the tail recursively generated? (The input without this minimum element.)

(here, denotes list with the elements of list removed).

I’m not alone in making this assertion. Norman Ramsey wrote a nice paper On Teaching HtDP; his experience led him to the lesson that

Last, and rarely, you could design a function’s template around the introduction form for the result type. When I teach [HtDP] again, I will make my students aware of this decision point in the construction of a function’s template: should they use elimination forms, function composition, or an introduction form? They should use elimination forms usually, function composition sometimes, and an introduction form rarely.

He also elaborates on test coverage:

Check functional examples to be sure every choice of input is represented. Check functional examples to be sure every choice of output is represented. This activity is especially valuable for functions returning Booleans.

(his emphasis). We should pay attention to output data structure as well as to input data structure.

Generative recursion, aka divide-and-conquer

Only once this dual form of program structure has been explored should students be encouraged to move on to generative recursion, because this exploits both structural recursion and structural corecursion. For example, the QuickSort algorithm that is used as the main motivating example is really structured as a corecursion to construct an intermediate tree, followed by structural recursion over that tree to produce the resulting list:

The structure of both functions and is determined by the structure of the intermediate datatype, the first as structural corecursion and the second as structural recursion. A similar explanation applies to any divide-and-conquer algorithm; for example, MergeSort is another divide-and-conquer sorting algorithm, with the same intermediate tree shape, but this time with a simple splitting phase and all the comparisons in the recombining phase:

(Choosing this particular tree type is a bit clunky for Merge Sort, because of the two calls to required in . It would be neater to use non-empty externally labelled binary trees, with elements at the leaves and none at the branches:

Then you define the main function to work only for non-empty lists, and provide a separate case for sorting the empty list. This clunkiness is a learning opportunity: to realise the problem, come up with a fix (no node labels in the tree), rearrange the furniture accordingly, then replay the development and compare the results.)

Having identified the two parts, structural recursion and structural corecursion, they may be studied separately; separation of concerns is a crucial lesson in introductory programming. Moreover, the parts may be put together in different ways. The divide-and-conquer pattern is known in the MPC community as a hylomorphism, an unfold to generate a call tree followed by a fold to consume that tree. As the QuickSort example suggests, the tree can always be deforested—it is a virtual data structure. But the converse pattern, of a fold from some structured input to some intermediate value, followed by an unfold to a different structured output, is also interesting—you can see this as a change of structured representation, so I called it a metamorphism. One simple application is to convert a number from an input base (a sequence of digits in that base), via an intermediate representation (the represented number), to an output base (a different sequence of digits). More interesting applications include encoding and data compression algorithms, such as arithmetic coding.

Laziness

Although I have used Haskell as a notation, nothing above depends on laziness; it would all work as well in ML or Scheme. It is true that the mathematical structures underlying structural recursion and structural corecursion are prettier when you admit infinite data structures—the final coalgebra of the base functor for lists is the datatype of finite and infinite lists, and without admitting the infinite ones some recursive definitions have no solution. But that sophistication is beyond the scope of introductory programming, and it suffices to restrict attention to finite data structures.

HtDP already stipulates a termination argument in the design recipe for generative recursion; the same kind of argument should be required for structural corecursion (and is easy to make for the sorting examples given above). Of course, structural recursion over finite data structures is necessarily terminating. Laziness is unnecessary for co-programming.

Structured programming

HtDP actually draws on a long tradition on relating data structure and program structure, which is a theme dear to my own heart (and indeed, the motto of this blog). Tony Hoare wrote in his Notes on Data Structuring in 1972:

There are certain close analogies between the methods used for structuring data and the methods for structuring a program which processes that data.

Fred Brooks put it pithily in The Mythical Man-Month in 1975:

Show me your flowcharts and conceal your tables, and I shall continue to be mystified. Show me your tables, and I won’t usually need your flowcharts; they’ll be obvious.

which was modernized by Eric Raymond in his 1997 essay The Cathedral and the Bazaar to:

Show me your code and conceal your data structures, and I shall continue to be mystified. Show me your data structures, and I won’t usually need your code; it’ll be obvious.

HtDP credits Jackson Structured Programming as partial inspiration for the design recipe approach. As Jackson wrote, also in 1975:

The central theme of this book has been the relationship between data and program structures. The data provides a model of the problem environment, and by basing our program structures on data structures we ensure that our programs will be intelligible and easy to maintain.

and

The structure of a program must be based on the structures of all of the data it processes.

(my emphasis). In a retrospective lecture in 2001, he clarified:

program structure should be dictated by the structure of its input and output data streams

—the JSP approach was designed for processing sequential streams of input records to similar streams of output records, and the essence of the approach is to identify the structures of each of the data files (input and output) in terms of sequences, selections, and iterations (that is, as regular languages), to refine them all to a common structure that matches all of them simultaneously, and to use that common data structure as the program structure. So even way back in 1975 it was clear that we need to pay attention to the structure of output data as well as to that of input data.

Ad-hockery

HtDP apologizes that generative recursion (which it identifies with the field of algorithm design)

is much more of an ad hoc activity than the data-driven design of structurally recursive functions. Indeed, it is almost better to call it inventing an algorithm than designing one. Inventing an algorithm requires a new insight—a “eureka”.

It goes on to suggest that mere programmers cannot generally be expected to have such algorithmic insights:

In practice, new complex algorithms are often developed by mathematicians and mathematical computer scientists; programmers, though, must th[o]roughly understand the underlying ideas so that they can invent the simple algorithms on their own and communicate with scientists about the others.

I say that this defeatism is a consequence of not following through on the core message, that data structure determines program structure. QuickSort and MergeSort are not ad hoc. Admittedly, they do require some insight in order to identify structure that is not present in either the input or the output. But having identified that structure, there is no further mystery, and no ad-hockery required.

The previous post turned out to be rather complicated. In this one, I return to much simpler matters: and on lists, and list homomorphisms with an associative binary operator. For simplicity, I’m only going to be discussing finite lists.

Fold right

Recall that is defined as follows:

It satisfies the following universal property, which gives necessary and sufficient conditions for a function to be expressible as a :

As one consequence of the universal property, we get a fusion theorem, which states sufficient conditions for fusing a following function into a :

(on finite lists—infinite lists require an additional strictness condition). Fusion is an equivalence if is surjective. If is not surjective, it’s an equivalence on the range of that fold: the left-hand side implies

only for of the form for some , not for all .

As a second consequence of the universal property (or alternatively, as a consequence of the free theorem of the type of ), we have map–fold fusion:

The code golf “” is a concise if opaque way of writing the binary operator pointfree: .

Fold left

Similarly, is defined as follows:

( is tail recursive, so it is unproductive on an infinite list.)

also enjoys a universal property, although it’s not so well known as that for . Because of the varying accumulating parameter , the universal property entails abstracting that argument on the left in favour of a universal quantification on the right:

(For the proof, see Exercise 16 in my paper with Richard Bird on arithmetic coding.)

From the universal property, it is straightforward to prove a map– fusion theorem:

Note that . There is also a fusion theorem:

This is easy to prove by induction. (I would expect it also to be a consequence of the universal property, but I don’t see how to make that go through.)

Duality theorems

Of course, and are closely related. §3.5.1 of Bird and Wadler’s classic text presents a First Duality Theorem:

when is associative with neutral element ; a more general Second Duality Theorem:

when associates with (that is, ) and (for all , but fixed ); and a Third Duality Theorem:

(again, all three only for finite ).

The First Duality Theorem is a specialization of the Second, when (but curiously, also a slight strengthening: apparently all we require is that , not that both equal ; for example, we still have , even though is not the neutral element for ).

Characterization

“When is a function a fold?” Evidently, if function on lists is injective, then it can be written as a : in that case (at least, classically speaking), has a post-inverse—a function such that —so:

and so, letting , we have

But also evidently, injectivity is not necessary for a function to be a fold; after all, is a fold, but not the least bit injective. Is there a simple condition that is both sufficient and necessary for a function to be a fold? There is! The condition is that lists equivalent under remain equivalent when extended by an element:

We say that is leftwards. (The kernel of a function is a relation on its domain, namely the set of pairs such that ; this condition is equivalent to for every .) Clearly, leftwardsness is necessary: if and , then

Moreover, leftwardsness is sufficient. For, suppose that is leftwards; then pick a function such that, when is in the range of , we get for some such that (and it doesn’t matter what value returns for outside the range of ), and then define

This is a proper definition of , on account of leftwardsness, in the sense that it doesn’t matter which value we pick for , as long as indeed : any other value that also satisfies entails the same outcome for . Intuitively, it is not necessary to completely invert (as we did in the injective case), provided that preserves enough distinctions. For example, for (for which indeed implies ), we could pick . In particular, is obviously in the range of ; then is chosen to be some such that , and so by construction —in other words, acts as a kind of partial inverse of . So we get:

and therefore where .

Monoids and list homomorphisms

A list homomorphism is a fold after a map in a monoid. That is, define

provided that and form a monoid. (One may verify that this condition is sufficient for the equations to completely define the function; moreover, they are almost necessary— and should form a monoid on the range of .) The Haskell library defines an analogous method, whose list instance is

—the binary operator and initial value are determined implicitly by the instance rather than being passed explicitly.

Richard Bird’s Introduction to the Theory of Lists states implicitly what might be called the First Homomorphism Theorem, that any homomorphism consists of a reduction after a map (in fact, a consequence of the free theorem of the type of ):

Explicitly as Lemma 4 (“Specialization”) the same paper states a Second Homomorphism Theorem, that any homomorphism can be evaluated right-to-left or left-to-right, among other orders:

I wrote up the Third Homomorphism Theorem, which is the converse of the Second Homomorphism Theorem: any function that can be written both as a and as a is a homomorphism. I learned this theorem from David Skillicorn, but it was conjectured earlier by Richard Bird and proved by Lambert Meertens during a train journey in the Netherlands—as the story goes, Lambert returned from a bathroom break with the idea for the proof. Formally, for given , if there exists such that

then there also exists and associative such that

Recall that is “leftwards” if

and that the leftwards functions are precisely the s. Dually, is rightwards if

and (as one can show) the rightwards functions are precisely the s. So the Specialization Theorem states that every homomorphism is both leftwards and rightwards, and the Third Homomorphism Theorem states that every function that is both leftwards and rightwards is necessarily a homomorphism. To prove the latter, suppose that is both leftwards and rightwards; then pick a function such that, for in the range of , we get for some such that , and then define

As before, this is a proper definition of : assuming leftwardsness and rightwardsness, the result does not depend on the representatives chosen for . By construction, again satisfies for any , and so we have:

Moreover, one can show that is associative, and its neutral element (at least on the range of ).

For example, sorting a list can obviously be done as a , using insertion sort; by the Third Duality Theorem, it can therefore also be done as a on the reverse of the list; and because the order of the input is irrelevant, the reverse can be omitted. The Third Homomorphism Theorem then implies that there exists an associative binary operator such that . It also gives a specification of , given a suitable partial inverse of —in this case, suffices, because is idempotent. The only characterization of arising directly from the proof involves repeatedly inserting the elements of one argument into the other, which does not exploit sortedness of the first argument. But from this inefficient characterization, one may derive the more efficient implementation that merges two sorted sequences, and hence obtain merge sort overall.

The Trick

Here is another relationship between the directed folds ( and ) and list homomorphisms—any directed fold can be implemented as a homomorphism, followed by a final function application to a starting value:

Roughly speaking, this is because application and composition are related:

(here, is right-associating, loose-binding function application). To be more precise:

This result has many applications. For example, it’s the essence of parallel recognizers for regular languages. Language recognition looks at first like an inherently sequential process; a recognizer over an alphabet can be represented as a finite state machine over states , with a state transition function of type , and such a function is clearly not associative. But by mapping this function over the sequence of symbols, we get a sequence of functions, which should be subject to composition. Composition is of course associative, so can be computed in parallel, in steps on processors. Better yet, each such function can be represented as an array (since is finite), and the composition of any number of such functions takes a fixed amount of space to represent, and a fixed amount of time to apply, so the steps take time.

Similarly for carry-lookahead addition circuits. Binary addition of two -bit numbers with an initial carry-in proceeds from right to left, adding bit by bit and taking care of carries, producing an -bit result and a carry-out; this too appears inherently sequential. But there aren’t many options for the pair of input bits at a particular position: two s will always generate an outgoing carry, two s will always kill an incoming carry, and a and in either order will propagate an incoming carry to an outgoing one. Whether there is a carry-in at a particular bit position is computed by a of the bits to the right of that position, zipped together, starting from the initial carry-in, using the binary operator defined by

Again, applying to a bit-pair makes a bit-to-bit function; these functions are to be composed, and function composition is associative. Better, such functions have small finite representations as arrays (indeed, we need a domain of only three elements, ; and are both left zeroes of composition, and is neutral). Better still, we can compute the carry-in at all positions using a , which for an associative binary operator can also be performed in parallel in steps on processors.

The Trick seems to be related to Cayley’s Theorem, on monoids rather than groups: any monoid is equivalent to a monoid of endomorphisms. That is, corresponding to every monoid , with a set, and an associative binary operator with neutral element , there is another monoid on the carrier of endomorphisms of the form ; the mappings and are both monoid homomorphisms, and are each other’s inverse. (Cayley’s Theorem is what happens to the Yoneda Embedding when specialized to the one-object category representing a monoid.) So any list homomorphism corresponds to a list homomorphism with endomorphisms as the carrier, followed by a single final function application:

Note that takes a list element the endomorphism . The change of representation from to is the same as in The Trick, and is also what underlies Hughes’s novel representation of lists; but I can’t quite put my finger on what these both have to do with Cayley and Yoneda.