Algorithmics

Abstract

Algorithmics is the study and practice of taking a high-level description of a program’s purpose and, from it, producing an executable program of acceptable efficiency. Each step in that process is justified by rigorous, careful reasoning at the moment it is taken; and the repertoire of steps allowed by that rigour, at each stage, guides the development of the algorithm itself.

IFIP’s Working Group 2.1 [i] has always been concerned with Algorithmics: both the design of its notations and the laws that enable its calculations. ALGOL 60 had already shown that orthogonality, simplicity and rigour in a programming language improves the quality of its programs.

Our Group’s title “Algorithmic Languages and Calculi” describes our activities: the discovery of precise but more general rules of calculational reasoning for the many new styles of programming that have developed over the 60 years since IFIP’s founding. As our contribution to the birthday celebrations, we outline how we have tried to contribute during those decades to the rigorous and reliable design of computer programs of all kinds—to Algorithmics. (Roman-numbered references like [i] in this abstract refer to details given in Sect. 10.)

1 Introduction

WG2.1 is one of the the first Working Groups of IFIP, and the oldest extant: it was founded at the request of TC2, which had begun its own very first meeting only two days before [ii]. Initially the “IFIP Working Group 2.1 on ALGOL”, it is now known as the

IFIP Working Group 2.1 on Algorithmic Languages and Calculi.   [iii]

The Group has always focused on methods for systematic program construction; and our goal is to make the methods steadily more powerful and more general. For example, the formalisation of the inductive assertion method [iv] led to a logical method based on pre- and postconditions [v], and then to a strongly calculational goal-directed method [vi]. Generalising programs to special cases of specifications [vii] led to the Mathematics of Program Construction. And a program-algebraic approach evolved from that: the “Laws of Programming” [viii].

Mathematics (of program construction or otherwise) can be carried out with pencil and paper. For programs, however, there are more significant advantages in automation than for mathematics generally; thus the Group has always paid attention to program transformation systems [ix]—but their design should be based on the ‘by hand’ calculations that preceded them.

Language design, including the advancement of ALGOL, remained a main interest for many years, focussing for a period specifically on a more advanced language called “Abstracto”. Abstracto generalised what ‘programming’ languages actually should be: rather than just for programming or writing executable code, they should also be able to describe algorithms in an abstract way. They should allow expressing (initially vague) ideas about an algorithm’s high-level structure and, after transformations adding details, reach a level from which the final step to ‘real’ programming-language code is simple enough to minimise the risk of transcription errors. In sum, Abstracto was supposed to support and codify our Algorithmics activity: but our activity itself outgrew that.

ALGOL 60 and 68 were languages more oriented to programmers’ thoughts than to computers’ hardware. In their ‘successor’ Abstracto, we wanted [xi]

(1)

Abstracto was to be an algorithmic language: one for describing the algorithmic steps in a computation, not just the input-output relation or similar behavioural specification. But it was still intended to be a ‘tool of thought’, rather than primarily an implementation language.

But the Abstracto approach was itself soon abstracted by abandoning the imperative ALGOL-like language structures, switching to a more functional presentation [xii] in which there was an algebra of programs themselves, rather than say an algebra of statements about programs. The framework for this became known as the “Bird–Meertens Formalism”, a very concise notation in which algorithmic strategies can be expressed and transformed (Sect. 2). That exposed many general algorithmic patterns and calculational laws about them that had, until then, been obscured by the earlier imperative control structures.

A similar abstracting approach was applied to data structures in the form of a hierarchy –the Boom hierarchy– leading from sets through multisets (bags) and lists to (binary) trees [xiii] (Subsect. 2.3, Sect. 3). The insight was that all these structures had a common pattern of constructors (an empty structure, a singleton constructor, and a binary combiner). They were distinguished from each other not by the signatures of their operations, but rather by the algebraic laws imposed on the constructors: the fewer laws, the more structure in the generated elements. 

A further abstraction was to allow the constructors to vary, i.e. to have an even more general approach in which one could say rigorously “Sum the integers in a structure, no matter what its shape.” and then reason effectively about it, for example that “Square all the integers in a structure, and then add them up.” is the same as “Sum the squares of all the integers in that structure.” This led to generic programming (Sect. 3). Genericity was achieved by using elementary concepts from algebra and category theory — functors, initial and final algebras, and the various kinds of morphisms on them [xiv] (Sect. 4). Programs taking advantage of this are called “polytypic”,  i.e. allowing many kinds of type structures, in the same way that polymorphic programs allow many kinds of type values within a single class of structures.

Unfortunately, the kind of specification that most polytypic languages support in their type signatures is very limited. Type theory [xv] however showed how any specification expressible in predicate logic could serve as the type of a program. That enables programmers to capture arbitrary invariants and specifications of their programs, such as balanced trees or sorted lists, simply as part of the program’s type. Since types are checked at compile-time, any type-correct program will never violate those specifications at runtime. This is supported by dependently typed programming languages (Sect. 5).

Besides the activities around data structures there was also a branch of work dealing with the task of mimicking imperative structures, as, e.g., necessary to describe interaction with the environment, in a purely functional context. Monads, applicative functors, and algebraic effects have provided a mathematically solid account that could be formulated in a way that allowed program-algebraic calculation after all (Sect. 6).

The investigations into data structures and generic algorithms on them were mainly carried out around (quotients of) tree-like structures. However, there are numerous more general (graph-like) structures which are not easily represented in that framework. As these should be approachable by calculations as well, our activities have therefore also dealt with relational or relationally based structures, which is their natural mathematical representation. Abstracting relations to algebraic structures such as Kleene algebras provides notions well suited for describing not only data structures but also control structures of various kinds (Sect. 7). This approach also links nicely to the predicate transformer approaches [vi] and the “Laws of Programming” [viii].

Systematic program construction benefits greatly from program construction systems — tools to support the work of the program constructor. This work involves reasoning about programs, which can be shallow and tedious; automated tools are less error-prone than humans at such activities. Moreover, programs are usually much longer than formal expressions in other contexts, such as in traditional mathematics; so tool support is also a convenience. Finally, a system can record the development history, producing automatically the software documentation that allows a replay, upon a change of specification, or an audit if something goes wrong. The Group has always worked on design and engineering of transformation systems in parallel with the work on the underlying transformation calculi; our survey therefore concludes with a more detailed account of corresponding tool support (Sect. 8).

Generally, the Group’s pattern has always been to expand the concepts that enable rigorous construction of correct programs, then streamline their application, and finally simplify their presentation. And then... expand again.

As the trajectory in this section has described (with the benefit of hindsight) the Group has always had diverse interests that arise from our program-calculational ‘mindset’ applied to other computer-science interest areas and even real-world contemporary problems [xvi].

2 From ALGOL, via Abstracto... to Squiggol

2.1 Abstracto: the first move towards algorithmics

After the completion of the Revised Report on ALGOL 68 [xix], the Group set up a Future Work subcommittee to decide how to progress. This subcommittee in turn organised two public conferences on New Directions in Algorithmic Languages [xi], after which the Group focussed again on specific topics. The Chair highlighted two foci: programming languages for beginners [xvii], and “Abstracto”. The first led to the development of the beginner’s language ABC and hence eventually to Python [xviii]; the other was Abstracto, and was

... not a specification language as such since it is still concerned with how to do things and not just what is to be done, but [allowing] the expression of the ‘how’ in the simplest and most abstract possible way. [xi]

Fig. 1.

Abstracto 84 [xx]

A representative example of Abstracto is shown in Fig. 1. It is part of the development of a ‘fast exponentiation’ algorithm: given natural numbers X and Y, compute $z = X^{Y}$ using only $O(\log _2 Y)$ iterations. The program on the left shows a ‘while’ loop, with invariant $z \times x^y = X^{Y}$, variant y, and guard $y \ne 0$. The program on the right factors out $r = y \mathbin {\mathrm {mod}} 2$, refining the nondeterminism in the first program to a deterministic loop. Thus our vision for Abstracto was as a kind of ‘refinement calculus’ for imperative programs [xxi].

2.2 The Bird–Meertens Formalism (BMF): A Higher-Level Approach

Although the Abstracto approach was successful, in the sense that it could be used to solve the various challenge problems that the Group worked on, after some time it was realised that the transformation steps needed were too low level — and so a key insight was to lift the reasoning to a higher level [xxii], namely to abandon the imperative ALGOL-like style and the corresponding refinement-oriented approach of Abstracto, and to switch instead to a more algebraic, functional presentation.

Fig. 2.

The oldest inhabitant, in Abstracto [136]

Fig. 3.

The maximum segment sum problem [xxiv]

It made a big difference. Consider for example the two programs in Fig. 2 [xx], where the problem is to find the (assumed unique) oldest inhabitant of the Netherlands. The data is given by a collection $dm$ of Dutch municipalities, and an array $mr [-]$ of municipal registers of individuals, one register per municipality. The program on the left combines all the municipal registers into one national register; the program on the right finds the oldest inhabitant of each municipality, and then findest the oldest among those ‘local Methuselahs’. Provided that no municipality is uninhabited, the two programs have equivalent behaviour. However, one cannot reasonably expect that precise transformation, from the one to the other, to be present in any catalogue of transformations. Instead, the development should proceed by a series of simpler steps that, because of their simplicity, can feasibly be collected in a smaller and more manageable catalogue of general-purpose transformations.

The equivalent higher-level transformation is this one: [xxii]

Its left-hand side takes the oldest in the union of the registers of each of the municipalities, and the right-hand side takes the oldest among those local Methuselahs. The “$\oplus /$” reduces a collection using binary operator $\oplus$; the “$+$” is binary union; the “$\uparrow _f$” chooses which of two arguments has the greater f-value; the “” maps function g over a collection; and finally, function composition is indicated by juxtaposition. The functional presentation is clearly an order of magnitude shorter than the Abstracto one. It is also easier to see what form the small general-purpose transformation steps should take—simple equations such as “reduce promotion” () and “map fusion” () [xxiii]. The notation evolved further through the 1980s [xxiv], and came to be known as “Squiggol”. It was later given the more respectable name “Bird–Meertens Formalism” [xxv], and inspired the Group’s further efforts in rigorous, concise program development.

Another example of concise calculation is given in Fig. 3.

2.3 The Boom Hierarchy of Data Structures

The operators and transformation rules of Squiggol/BMF apply equally to lists, bags, and sets. And those three datatypes are conceptually linked by their common signature of constructors (an empty structure, a singleton constructor, and a binary combination) but satisfying different laws (associativity, commutativity, and idempotence of the binary combination, with the empty structure as a unit). Moreover, the core operations (maps, filters, and reductions) are homomorphisms over this algebraic structure.

Crucially, each datatype is the free algebra on that common signature, with a given set of equations, generated from a domain of individual elements; that is, there exists a unique homomorphism from the datatype to any other algebra of the same kind. For example, writing “$[\,]$” for the empty structure, “[x]” for a singleton, “$\mathbin {+\!\!\!+}$” for the binary combination, and given a binary operator $\oplus$ with unit e, the three equations

$$ \begin{array}{lcl} \mathord {\oplus /} [\,] &{}=&{} e \\ \mathord {\oplus /} [a] &{}=&{} a \\ \mathord {\oplus /} {(x \mathbin {+\!\!\!+}y)} &{}=&{} \mathord {\oplus /}x \,\oplus \, \mathord {\oplus /}y \end{array} $$

determine the reduction operator $\mathord {\oplus /}$ uniquely: provided that $\oplus$ is associative, these three equations have as their unique solution the aggregation function from lists. But if we add the assumption that $\oplus$ is also commutative, then there is a unique function from bags; and if we add idempotence, then there is a unique function from sets.

If out of curiosity we assert no equations of the binary operator alone, only that the empty structure is its unit, then we obtain a fourth member of the family, a peculiar sort of binary tree. The four members form a hierarchy, by adding the three equations one by one to this tree type. The resulting hierarchy of data structures was called the “Boom” hierarchy [xiii]. Its connections to the Eindhoven quantifier notation [xxvi] greatly simplified the body of operators and laws needed for a useful theory.

3 Generic Programming: Function Follows Form

The Boom hierarchy is an example of how we can use algebras and homomorphisms to describe a collection of datatypes, together with a number of basic operations on those datatypes. In the case of the Boom hierarchy, the constructors of the algebra are fixed, and the laws the operators satisfy vary. Another axis along which we can abstract is the constructors of a datatype: we realised that concepts from category theory can be used to describe a large collection of datatypes as initial algebras or final coalgebras of a functor [xiv]. The action of the initial algebra represents the constructors of the datatype it models. And it has the attractive property that any homomorphism on the functor algebra induces a unique function from the initial algebra. Such a function was called a catamorphism [xxvii]. A catamorphism captures the canonical recursive form on a datatype represented by an initial algebra. In the functional programming world, a catamorphism is called a fold, and in object-oriented programming languages the concept corresponds closely to visitors. Typical examples are functions like map, applying an argument function to all elements in a value of a datatype, and size, returning the number of elements in a value of a (container) datatype. Catamorphisms satisfy a nice fusion property, which is the basis of many laws in programming calculi. This work started a line of research on datatype-generic programming [xxviii], capturing various forms of recursion as morphisms, more about which in Sect. 4.

The program calculus thus developed could be used to calculate solutions to many software problems. As a spin-off, the theory described programs that could be implemented in a standard, but different, way on datatypes that can be described as initial functor-algebras. No general-purpose programming language supported such typed, generic functions, so these functions had to be implemented over and again for different datatypes.

Using the structure of polynomial functors, the language PolyP was designed that extended the lazy, higher-order functional programming language Haskell [xxix]. In PolyP, a generic function is defined by means of induction on the structure of functors. Using this programming language it was possible to define not only the recursive combinators from the program calculus, such as folds and unfolds, but also to write generic programs for unification, term rewriting, pattern matching, etc. Figure 4 shows an example of a polytypic program.

Fig. 4.

A PolyP program to flatten a container to a list [xxix]

PolyP supported the definition of generic functions on datatypes that can be described as initial functor-algebras but do not involve mutual recursion. While sufficient for proof-of-concept demonstration purposes, this last restriction was a severe limitation on practical applicability. Generic programming is particularly attractive in situations with large datatypes, such as the abstract syntax of programming languages, and such datatypes are usually mutually recursive. Generic Haskell was developed to support generic functions on sets of mutually recursive datatypes [xxx]. Generic functions defined in Generic Haskell can be applied to values of almost any datatype definable in Haskell. Figure 5 shows how a generic equality function is implemented in Generic Haskell.

The approach of defining generic functions in Generic Haskell can also be used to define type-indexed (or generic) datatypes. A type-indexed datatype is a data type that is constructed in a generic way from an argument data type. For example, in the case of digital searching, we have to define a search tree type by induction on the structure of the type of search keys. Generic Haskell also supports the possibility of defining type-indexed datatypes [xxxi]. The functional programming language Haskell now supports a light-weight variant of type-indexed datatypes through type families.

Fig. 5.

A generic Haskell program for equality [xxx]

The fixed-point structure of datatypes is lost in Generic Haskell, however, and with it the capability of defining the generic fold function. It was then discovered how to obtain a fixed-point representation of possibly mutually recursive datatypes, bringing the generic fold function back into the fold [xxxii]. Thus we can define the fold function for the abstract syntax of a programming language, bringing generic programming within reach of compiler writers.

Meanwhile, Haskell –or, more precisely, compilers supporting various Haskell extensions– evolved considerably since PolyP and Generic Haskell were developed. With respect to types, GHC, the Glasgow Haskell Compiler, now supports multiple-parameter type classes, generalised algebraic datatypes (gadts), type families, etc. Using these extensions, it is now possible to define generic functions in Haskell itself, using a library for generic programming. Since 2000, tens of such libraries have been developed world-wide [xxxiii]. Since –from a generic programming perspective– the expressiveness of these libraries is almost the same as the special-purpose language extensions, and since such libraries are much easier to develop, maintain, and ship, these libraries make generic programming more generally available. Indeed, these libraries have found their way to a wider audience: for example, Scrap Your Boilerplate has been downloaded almost 300,000 times, and Generic Deriving almost 100,000 times [xxxiii].

4 Morphisms: Suddenly They Are Everywhere

In Sect. 3 we identified catamorphisms as a canonical recursive form on a datatype represented by an initial algebra: in functional-programming parlance, a fold. From there, however, further work [xxxiv] led to a rich research agenda concerned with capturing the pattern of many other useful recursive functions that did not quite fit that scheme, that were not quite ‘catamorphic’. Indeed, it gave rise to a whole zoo of morphisms: mutumorphisms, zygomorphisms, histomorphisms, generalised folds, and generic accumulations [xxxv]. Just as with catamorphisms, those recursion schemes attracted attention because they made termination or progress manifest (no need to prove or check it) and they enjoyed many useful and general calculational properties — which would otherwise have to be established afresh for each new application.

4.1 Diversification

Where while-loops are governed by a predicate on the current state, and for loops by an incrementing counter, structured recursion schemes such as catamorphisms take a more restricted approach where it is the structure of the input data itself that controls the flow of execution (“function follows form”).

As a simple example, consider how a list of integers is summed: a catamorphism simply recurses over the structure of the list. No for-loop index variable, and no predicate: when the list is empty the sum is zero, and when the list contains at least one number it should be added to the sum of the residual list. While-loops could easily encode such tasks, but their extra expressive power is also their weakness: we know that it is not always tractable to analyse loops in general. With catamorphisms, the analysis is much simpler — the recursion scheme is simply induction over a datatype.

The analogy with induction goes further. Number theorists have long studied computable functions on natural numbers, and an important class are the primitive recursive functions, which provide the recursive step with the original argument as well as the result of recursing on that argument. Such functions are an instance of the paramorphism [xxxvi], which is an interchangeable variation on the catamorphism.

Further still, an attractive variant of induction is strong induction, where the inductive step can rely on all the previous steps. Its parallel as a recursion scheme is the histomorphism and, just as strong induction and induction are interchangeable, histomorphisms are encodable as catamorphisms. The utility of these schemes –the point of it all– is however to make it convenient to describe programs that would otherwise be difficult to express, and to derive others from them. In the case of histomorphisms (strong recursion), for example, it is the essence of simple dynamic programming programs such as the knapsack problem, or counting the number of possible bracketings, that was captured. More complex dynamic programming problems, such as the multiplication of a chain of matrices, requires a slightly more nuanced recursion scheme, the dynamorphism, where an intermediate data structure is generated.

We recall that the exploitation of various forms of duality revolutionalised the field of physics; algorithmics similarly benefits from an important form of input-output duality. Each recursion scheme features a dual scheme: while one focuses on consuming the input, the other emphasizes producing the output. To illustrate, consider how insertion sort deconstructs a list by extracting numbers one at a time (input), inserting them appropriately into a sorted list (output). Whereas the deconstruction of the original list is another catamorphism, the construction of the sorted list exemplifies an anamorphism—it is the dual situation. Thus expressing insertion sort in terms of recursion schemes allows us to dualize the algorithm to obtain another sorting algorithm for free: selection sort. This works by constructing a sorted list (an anamorphism), and at each step performs a selection that deconstructs the unsorted list to extract the smallest element (a paramorphism).

Another way to understand a catamorphism is that it applies a strategy that takes subsolutions and conquers them (with a so-called algebra) to provide a final solution. Dually, an anamorphism applies a strategy that takes a problem and splits it up into subproblems (with a so-called coalgebra). Those can be understood as the two components of a divide-and-conquer strategy, and the combination is known as a hylomorphism, depicted in the diagram below:

Catamorphisms are then the special case of this diagram where the dividing step simply deconstructs a data structure, and anamorphisms the special case where the conquering step constructs a data structure.

4.2 Unification

The multitude of generalisations of catamorphisms and their duals is bewildering.

Many of them were defined as adaptations of catamorphisms, but in most cases showing that those corresponded directly to catamorphisms required careful calculation. And with so many different variations, a natural question is whether there is some underlying commonality that unifies them all. Indeed there is.

The unification was achieved by borrowing some slightly more sophisticated machinery from category theory. A first attempt was to use comonads, which allow access to contextual information [xxxvii], to organise the structure of recursive calls. Another attempt used adjunctions instead as the common thread [xxxviii]. That resulted in so-called “adjoint” folds, which show how a catamorphism in one category can give rise to a different recursion scheme in another. Although the two methods were initially thought to be disjoint, later work revealed recursion schemes from comonads to be a special case of adjoint folds with an appropriate distributive law.

Each of these two unifications of recursion schemes treated generalizations of catamorphisms separately to their dual counterparts of anamorphisms. But both are special cases of hylomorphisms; and so the next step was to generalise all inductive and coinductive recursion schemes within the single unifying theme of conjugate hylomorphisms — or ‘the mother of all recursion schemes’. Naturally, the Group named it the mamamorphism. This time, the more sophisticated categorical techniques were used to extend the work on adjoint folds with conjugate distributive laws to connect pairs of adjunctions.

All in all, the unifying work on recursion schemes benefitted greatly from the unifying power of category theory — which is what category theory is for.

5 Dependent Types: Types You Can Depend on

Datatype-generic programming explores how to define functions and datatypes by induction over the structure of algebraic types. This line of research within the Group sparked further interest in the exploration of how to use static type information in the construction of programs. In particular, emerging programming languages with dependent types offered new opportunities for program verification, program transformation, program calculation and type-directed program development.

5.1 What Are Dependent Types?

The idea of programming with dependent types dates back at least as far as the 1970’s, when it became increasingly clear that there was a deep connection between constructive mathematics and computer programming [xxxix]. In the late 20th century, a number of new programming languages emerged, exploring these ideas [xl]. Those languages, and their implementations, enabled the further exploration of the possibilities that statically typed languages with dependent types offered. Each of them adopted the Curry-Howard correspondence [xli], connecting programming languages and mathematical logic, as the guiding principle of program language design. The terms of each language correspond to both programs and proofs; a type can equally well be read as a specification or a proposition. To ensure the logic underlying a language’s type system is sound, all functions must be total, disallowing partial incomplete pattern matching and diverging functions. The benefit of this disciplined approach to software development is that these languages provide a unified setting for both programming and program verification. Given the strong traditions of program calculation and functional programming within the Group, for instance, using the Bird–Meertens Formalism to perform equational reasoning about Haskell programs, there was a clear interest in these new languages. Furthermore, the richer language of algebraic data types offered the ability to enforce invariants during a program’s construction.

5.2 Dependent Types

At the beginning of the 21st century, the relation between dependently typed programming and datatype generic programming was clearly emerging [xlii] leading to several influential PhD theses on this topic. The interest in dependent types from members of the Group dates back to the late 80’s [xliii].

The new languages based on type theory reinvigorated some of the past research that members of the Group have done on the derivation of correct programs. Following the Agda tutorial at Meeting #63 [xliv], the work on relational program calculation, for example, was shown to be possible within dependently typed languages. Similarly, the refinement calculus, used to derive a program from its specification, could be embedded in a proof assistant, enabling pen and paper proofs to be machine-checked. Program calculation in the style of Dijkstra using predicate transformer semantics could be modelled using type theory, rather than the traditional impredicative set theory. Types and proof assistants based on type theory became a central tool in the calculation of correct programs [xlv].

At that point, an influx of new members broadened the Group’s interest to novel application areas for dependently typed programming [xlvi], such as scientific computation, decision problems, and even the study of climate change. Combinator parsing, previously studied in the context of functional programming (see Subsect. 6.2), was implemented in a total language with dependent types [xlvii].

The new languages with dependent types also enabled new opportunities to exploit static type information to guide program development [xlviii] — in the same spirit as the research on datatype generic programming. Types can be read as a (partial) specification. The discovery of a type-correct program can arise from a dialogue with the type checker, helping establish a program’s correctness as it is written. There are numerous domain-specific languages and data types designed to enforce certain correctness properties by construction.

Dependently typed programming languages marry constructive logic and programming in a manner unfamiliar to most programmers. To ensure that the type system is sound, all programs must be total. Yet any mainstream language relies on numerous effects, such as general recursion, mutable state, concurrency, or exceptions, each of which break the promise of totality. To address this, there has been a line of research on how to incorporate effects in dependently typed program languages [xlix]. This, in turn, led to renewed interest from the Group on how to program safely and robustly in the presence of arbitary side-effects in any language, resulting in the study of algebraic effects (see Sect. 6).

6 Computational Effects: Beyond the Functional

When the Group switched to a purely functional presentation of programs [xxii], that is from Abstracto to Squiggol (Sect. 2), at first this also meant doing away with a group of programming-language features known collectively as “effects”.

6.1 Effects and Monads

Effects cover all behavioural aspects of a computational function that go beyond the input-output behaviour of mathematical functions. It includes interaction of a program with its environment (the file system and operating system, other processes, human operators, distant servers, ...), mechanisms for structuring the internal control flow (partiality and exceptions, backtracking, nondeterminism and probability, delimited control, ...), and implicit dataflows (mutable state and global variables).

While some of these effects are indeed symptoms of a low-level imperative encoding, such as local mutable state, others are essential in real-world programs that interact with the environment. And they can be important for structuring programs compositionally: examples are exceptions and backtracking.

Fortunately, it turned out that useful effects need not be abandoned in a purely functional setting [l]—the ‘doing away with’ was only temporary. Effects can after all be modelled with pure functions. Here are some examples:

$$\begin{aligned} \begin{array}{ll} a \rightarrow b &{}\qquad \text {a pure function} \\ a \rightarrow 1 + b &{}\qquad \text {a partial function} \\ a \rightarrow e + b &{}\qquad \text {a function with exceptions } e \\ a \rightarrow b^+ &{}\qquad \text {a nondeterministic function} \\ a \rightarrow b^* &{}\qquad \ldots \text { which might also fail} \\ a \rightarrow b \times o^* &{}\qquad \text {a function that sends }o\text {'s to its environment} \\ a \rightarrow \mu x. ((i \rightarrow x) + b) &{}\qquad \text {a function that reads }i\text {'s from its environment} \\ a \rightarrow (s \rightarrow (b \times s)) &{}\qquad \text {a function with implicit state }s \\ \quad \vdots &{} \end{array} \end{aligned}$$

(where $b^+$ denotes non-empty sequences of b’s, and $b^*$ possibly empty sequences).

It turned out that all those different types of functions with effects are ‘Kleisli’ arrows for appropriately structured monads [li]. The utility of the monad was that it handled calculation, in particular composition, of the types above in a single unified way. Whereas two functions of types $a\,{\rightarrow }\,b$ and $b\,{\rightarrow }\,c$ are easily composed to make a single function of type $a\,{\rightarrow }\,c$, it is not clear at first how to compose $a\,{\rightarrow }\,e{+}b$ and $b\,{\rightarrow }\,e{+}c$ to $a\,{\rightarrow }\,e{+}c$, or for that matter $a\,{\rightarrow }\,b^+$ and $b\,{\rightarrow }\,c^+$ to $a\,{\rightarrow }\,c^+$. And even when the (in retrospect) obvious definitions are adopted, one for each, the challenge is then to see those definitions as instances of a single generalised composition. That’s what Kleisli composition achieves.

6.2 Functions Too Weak, Monads Too Strong: Applicative Functors? Just Right

Once monads had brought effects back in the purview of purely functional reasoning, the Group turned its attention to reasoning about such programs—‘effectful’ programs. One fruitful example has been the study of recursive descent parsers [lii]. They lend themselves to a combinator style of programming. Moreover, the combinators fall neatly out of the observation that the datatype of parsers that return a parsed value is another monad, a combination of implicit state and nondeterminism with failure: the Kleisli arrows are of the form

$$ a \rightarrow (\varSigma ^* \rightarrow (b \times \varSigma ^*)^*) $$

where the alphabet of symbols is $\varSigma$ or, in verse [liii],

• A parser for things

• is a function from strings

• to lists of pairs

• of things and strings.

But the monadic presentation makes static analysis difficult: the interface allows earlier inputs to determine the parser used for later inputs, which is both more expressive than necessary (because few applications require such configurable syntax) and too expressive to analyse (because the later parser is not statically available). A weaker interface for effects turns out to be nearly as expressive, and much more amenable to analysis. The essence of this weaker interface was abstracted as an ‘applicative functor’, and has served as the foundation of significant subsequent work [liv].

6.3 Algebraic Effects and Handlers

But how to reason about effectful programs, such as applicative parsers, nondeterministic functions, and programs that perform I/O? A first step is to treat the effectful operations as an abstract datatype, provide a purely functional specification of that data abstraction, prove the program correct with respect to the algebraic specification, but run the program against the ‘real’ implementation that incurs actual effects such as I/O. In fact, one could consider the algebraic specification as the interface in the first place, and incorporate its axioms into traditional equational reasoning; it is then the responsibility of the implementer of the effect to satisfy the axioms. This approach is cleanly formalized in the notion of algebraic effects and handlers, whereby a pure functional program assembles a term describing the effects to be performed, and a complementary environment handles the term, by analogy with handling an exception [lv]. In fact, that term is a value of a type captured as the free monad on the signature of the effect operations, a datatype-generic notion (see Sect. 3).

7 Lifting the Game: A Purely Algebraic View of Algorithms and Languages

The systematic construction of algorithms –or, more generally, of computer programs– needs languages that are precise, effective, and that allow calculational reasoning. Previous sections showed how the Group discovered the striking similarities between derivations from quite different areas, such as path problems and regular languages [lvi]. Using algebra in its purest form, i.e. starting with a collection of postulated axioms and carrying out (program) derivations based on those laws alone, therefore enables an extremely abstract treatment: those derivations are then valid in any programming model that satisfies the axioms.

Calculi based on the algebra of binary relations [lvii] were prime candidates for that, since they allow a natural treatment of directed graphs—and they abstract and unify data structures (e.g. trees), transition systems and many more concepts.

Also, relations are intimately connected with predicates and hence can be used to describe (by pre- and postconditions) and calculate input-output behaviour. In particular, they cover principles of algorithm design such as dynamic programming, greedy algorithms etc. [lvi]

Relation Algebras make relations, i.e. sets of argument-value pairs, ‘first-class citizens’ by viewing them as algebraic elements subject to operators that treat them as a whole without looking at their internal structure. The ‘point-free’ approach that this enables often admits considerable concision. The basic relational operators (Fig. 6, right) are simply set union, intersection and complement, supplemented by sequential composition.

Although a relation-algebraic approach already allows the unified treatment of different instances of graph problems [lviii], replacing sets of pairs (single relations) by other entities yields further models of the same algebraic signature, known as (idempotent) semirings. Figure 6 (left) shows the operators common to semirings.

Fig. 6.

Operators of semirings and relation algebras

And those structures have applications in programming languages, algorithms, logic and software engineering:

• Classical logic is a well known simple semiring, in which choice corresponds to disjunction, composition to conjunction, 0 to false and 1 to true. To subsume classical logic fully, however, one requires negation — i.e. a Boolean algebra.

• When elements of a semiring are interpreted as (arbitrary) programs, the basic operators represent nondetermistic choice and sequential composition; 0 corresponds to the program abort and 1 to skip. Equations such as $1 \cdot x = x = x \cdot 1$ and $0 \cdot x = 0 = x \cdot 0$ form the basis of algebraic reasoning, including program transformations. The equations describe the facts that any program x composed with skip is identical to the program itself, and that any program composed with abort is identical to abort. This allows the expression of programs and specifications in the same framework. A program P satisfies a specification S if $P\le S$, where $\le$ expresses refinement, which is the canonical order available in every idempotent semiring. (In other styles of program calculation, that would be written $S\sqsubseteq P$.) This simple formulation of program correctness enables a wide range of methods for calculational program derivation and program verification [lix].

• Using partial maps as algebraic elements allows treating data structures with pointers. This usage was inspired by Squiggol (Sect. 2) [lx].

• When the underlying structure reflects the memory cells (heaps), the algebraic framework provides an abstract version of separation logic [lxi].

• When the algebraic elements are interpreted as sets of sets or sets of lists it is possible to derive aspects of feature-oriented software development, including the formal characterisation of product families and of feature interactions [lxii].

• Graphs are often equipped with edge labels representing weights, capacities or probabilities; likewise automata and labelled transition systems carry extra edge information in addition to source and target. Those can be treated by generalising Boolean matrices to matrices over other algebras. For classical graph algorithms, such as shortest-path algorithms, the max-plus algebra and the min-plus algebra are useful as underlying structure—here, min/max play the roles of (biased) choice, and plus is the operator for sequential composition (that is, adding path lengths/costs).

• Probabilistic aspects can be represented by matrices with real values between 0 and 1, and fit into the very same algebraic framework. Applications include calculational derivations of fuzzy algorithms.

• Fundamental concepts of programming-language semantics, including concurrent programs and termination, can be handled algebraically as well. Beyond the areas mentioned above, the Group has also applied this algebra in several areas, included object-oriented programming, data processing, game analysis and routing in mobile networks [lxii].

But semirings can be extended: and those extensions are used to capture additional concepts from data structures, program logics and program transformation. Here are some examples.

Kleene algebras, generalising the algebra of regular expressions, offer the additional operator $\_^*$ of arbitrary finite iteration. Algebraically, the loop while p do x becomes $(p \cdot x)^* \cdot \lnot p$, which is the least fixed-point of the function $\lambda y.$ if p then $x\cdot y$ else skip [lxiii].

Here p is a specific element, called a test, representing a predicate on the state space. The set of tests offers a negation operator $\lnot$ and hence forms a Boolean algebra [lxiv]. In the interpretation where algebraic elements are programs, a test p corresponds to an assert statement. For tests p, q and program element x the inequation $p\cdot x \le x\cdot q$ algebraically expresses the Hoare triple $\{p\} x \{q\}$ [lxi].

Furthermore, in certain Kleene algebras, known as quantales, the principle of fixed-point fusion [lxv] is a theorem, i.e. it can be derived from the axioms. This illustrates once again the powers of ‘algebraic unification’. Fusion, shown in Sects. 2 and 3 to be an extremely practical law for transforming functional programs, is now available for many other kinds of program too. Examples include merging of programs with the same loop structure, or ‘deforestation’, i.e. avoiding the generation of a large intermediate data structure that afterwards is ‘consumed’ again, in favour of ‘generation and consumption on the fly’. This is also known as “virtual” data structures [lxvi].

Omega algebras [lxvii], which offer an operator $\_^\omega$ for infinite iteration, allow the description and analysis of systems or programs with potentially never-ending behaviour, such as operating systems.

In algebras with finite and infinite behaviour, some algebraic laws of sequential composition need to be adapted by separating the finite and the infinite traces of a program x into the disjoint sets $\textsf {fin}\, x$ and $\textsf {inf}\, x$. While the above law $x \cdot 1 = x$ still holds for all elements, the property $x \cdot 0 = 0$ no longer holds when x contains infinite traces; it weakens to $(\textsf {fin}\, x) \cdot 0 = 0$. The intuitive explanation is that infinite traces do not terminate, and therefore a possible successor, including abort, can never be ‘executed’. Therefore the while-loop now has the more general behaviour

$$ (p \cdot x)^* \cdot \lnot p \quad =\quad (p \cdot \textsf {fin}\, x)^*\cdot (\lnot p + p\cdot \textsf {inf}\, x)\quad , $$

which means that after a finitely many finite traces from x the loop either terminates by not satisfying the test p any longer, or an infinite trace from x takes over, leading to overall non-termination. When x is purely finite, i.e., satisfies $\textsf {inf}\, x = 0$, this reduces to the expression given previously.

Like the operators of semirings, the operators of finite and infinite iterations (and many of their combinations) satisfy a common set of laws, and thus algebra helps to unify their treatment including the derivation of program transformations and refinement theorems. Applications range from termination in classical programs, via protocols, to dynamic and hybrid systems [lxvii].

Omega algebras are also used to develop a unified framework for various logics, including the temporal logics LTL, CTL and CTL$^*$, neighbourhood logic and separation logic [lxi].

To sum up: algebraic characterisations have helped to express (and prove) new notions and results and to unify concepts and identify the above-mentioned similarities. The Group has developed a coherent view on algorithms and languages from an algebraic perspective, and applies the same algebraic techniques to tackle modern technology, including the analysis of protocols and quantum computing. All the algebras in question provide a first-order equational calculus, which makes them ideal to be supported by automated theorem provers and interactive proof assistants [lxviii] [xliv]. As a consequence, they are well suited for developing tools that support program derivations and refinement in a (semi-)automated style.

8 System Support: the Right Tool for the Job

Calculational program construction derives a program from a formal specification by manageable, controlled steps that –because they are calculated– guarantee that the final product meets its initial specification. As we have seen, this methodology has been practised by many Group members, and many others too [lxix]. And it applies to many programming styles, including both functional and imperative. For the former one uses mostly equational reasoning, applying the defining equations of functions together with laws of the underlying data structures. For the latter, inequations deploying a refinement relation are common [lxx]. A frequent synonym for “calculation rules” is “transformation rules”.

A breakthrough occurred when the Group raised the level of reasoning (Sect. 2): from manipulations of imperative code (Abstracto) to algebraic abstractions of functional control patterns (Squiggol). This made it possible to compact derivations of several pages in traditional approaches down to one page or even less. A similar observation concerns the general theme of ‘algebraicisation’ (see Sect. 7).

8.1 System Support

Of course, calculational program construction can be done with pencil and paper, and initially it should be so: that encourages a simplicity and elegance in its methods. Ultimately, if the method proves to be useful, there are a number of good reasons for introducing system support:

• By its very nature, program transformation leads to frequent rewritings of program fragments; such clerical work should be automatic. And, by its very nature, a system does this mechanical activity better than a human can.

• The system can record the applicability conditions and help in reducing them to simpler forms, ideally all the way to “true”.

• And, as mentioned in Sect. 1, the system can construct a development history, again a clerical task. This history serves as detailed software documentation, since it reflects every design decision that enters into the final program. Thus, if a line of development turns out to be a blind alley, the history can be used for backtracking to try out alternative design decisions. Moreover, it is the key aid to software maintenance: when the specification has to be modified (because of new requirements), one can try to ‘replay’ a recorded development accordingly.

Thus the Group gave considerable attention to program transformation systems [ix] once the methods they automated were sufficiently mature. In the remainder of this section we take a brief look at one of them: it touches on several areas within the Group, and several Group members were involved in it and in follow-on projects.

8.2 An Example: The Project CIP

The project CIP (Computer-aided, Intuition-guided Programming) at TU Munich ran roughly through the period 1977–1990.

The Wide-Spectrum Language CIP-L. The CIP approach was based on a particular ‘life cycle of transformational program development’, roughly characterised by the following levels [lxxi]:

• 1. formal problem specification (usually descriptive, not (yet) executable, possibly non-deterministic);

• 2. recursive functional program;

• 3. efficiency-improved functional program;

• 4. deterministic, tail-recursive solution;

• 5. efficient procedural or machine-oriented program.

However, not all of these levels need occur: a development may start below Level 1 and end above Level 5; and it may skip some of the intermediate levels.

The language CIP-L was however especially designed to cover all five levels [lxxii]. Since transformations usually do not change a program as a whole, only small portions of it, it was mandatory to design one integrated wide-spectrum language rather separate languages for each level. In particular, the language included assertion constructs at all levels, thus allowing the incorporation of pre- and postconditions uniformly for functions and statements — so it is also connected to the refinement calculi that were developed around the same time [lxx]. CIP-L was partly inspired by Abstracto (Subsect. 2.1); in a sense, it tried to present a model of a possible concrete instance of Abstracto.

The Transformation System CIP-S. The purpose of CIP-S was the transformational development of programs and program schemes. In addition to bookkeeping tasks, that included the manipulation of concrete programs, the derivation of new transformation rules within the system, and support for the verification of side conditions of transformation rules [lxxiii].

In keeping with the overall CIP methodology, the kernel of the system was itself formally specified: starting from that specification, all routines were developed to Pascal-level CIP-L using an earlier prototype system. The results were embedded into an appropriate user environment, yielding a first operational version of CIP-S around 1990. In conjunction with a compiler for a substantial executable subset of CIP-L, the CIP-S system has been successfully used in education. The transformational approach was continued by the Group.

Experiences. There is an extensive body of case studies using the CIP methodology. They concern mostly small and medium-sized algorithms, e.g., sorting and parsing [lxxiv]. The formal development of CIP-S itself showed that the method is suitable for larger software projects too.

9 Summary; but No Conclusion

This is not a ‘conclusion’. And this article is not a history. It is a description of a goal, a justification of its importance, and a summary of the trajectory that has led, and still leads to progress towards that goal. And what we especially enjoy about that trajectory we have followed, right from the start 60 years ago, is that it has always been the same one:

Let us calculate!                     (Sect. 2 p6)

Why is that goal so important?

Writing programs using a careful process of walk-throughs and reviews is (alone) not enough; “growing” programs [lxxv] in a top-down way is (alone) not enough; proving your program correct afterwards is (alone) not enough. We have always believed that maintaining correctness from the very top, and then ‘all the way down’ is what we all should be aiming for.

But will we ever get there? No, we will not.

During the 1970’s, an array-out-of-bounds error in a high-level program would typically lead to a core dump, an inch-high stack of paper that was examined at just one spot, an “Ah, yes!” and then the whole thing just thrown away. Thirty years of progress brought us to ‘Interactive Development Environments’ and the internet, where sometimes the programmer was not even sure where the just-corrected version of a program had been ‘deployed’, nor exactly whether it contained the fix (because of caching). Error messages from a remote server in some far-away city flicked up out of the window, too quickly to be read, and could not be scrolled back. And twenty more years bring us up-to-date, with ‘intelligent’ aquarium thermometers that can be hacked from half a world away and used to raid a company’s private database. Plus ça change...

The one constant through all of this is people, their tolerance for impediments to getting their work done and their perseverance in spite of them. The technology we are trying to control, to approach rigorously, is always sitting on that boundary, just beyond our reach: we will never calculate far enough.

Thus, however good we become at calculating, and convincing others to do so, there will always be economic forces that promote and propagate computer applications that we cannot develop by careful walk-throughs, or grow top-down, or prove correct... or calculate. This ‘catching up’ factor is what drives all the IFIP working groups — we constantly extend our methods improve the impact of computers generally, to make them safer and increase their reliability, as their use becomes ever more ambitious and spreads ever more widely.

We are not so much ‘pushing’ as ‘being pulled’. There is the excitement.

10 Detailed Attributions and Citations

• [i] Contributors —

  All of the members members of WG2.1, past and present, deserve credit for what is reported here. Among those who provided actual text were Richard Bird, Jeremy Gibbons, Ralf Hinze, Peter Höfner, Johan Jeuring, Lambert Meertens, Bernhard Möller, Carroll Morgan, Tom Schrijvers, Wouter Swierstra and Nicolas Wu.

  Carroll Morgan was Group Chair at the time of writing, and is the corresponding author.

• [ii] The founding of IFIP —

  It was established on 23 March 1962 [158, 26].

• [iii] Change of name —

  At Meeting #39 in Chamrousse in January 1989, Formal Resolution 2 was to recommend to TC2 that the Group’s name be changed to “WG2.1 on ALGOL: Algorithmic Languages and Calculi”. But TC2 rejected the recommendation, as reported at Meeting #40. At Meeting #41 in Burton in May 1990, it was reported that TC2 suggested instead simply “Algorithmic Languages and Calculi”, and this suggestion was accepted by the Group. TC2 approved the change, which was reported at Meeting #42 in Louvain-la-Neuve in January 1991.

• [iv] Assigning meanings to programs —

  This was Floyd’s association of predicates with flowchart arcs [70].

• [v] An axiomatic basis for computer programming —

  This was Hoare’s logic for partial correctness [95].

• [vi] A Discipline of Programming —

  This was Dijkstra’s calculus of weakest preconditions [65].

• [vii] Predicative programming —

  This generalisation was the work of Hoare and Hehner [87, 88, 96].

• [viii] Laws of Programming —

  This work was presented by a number of authors, including Hoare, at Oxford’s Programming Research Group [97].

• [ix] Program-transformation systems —

  Systems designed and implemented by Group members include the Argonne TAMPR (Transformation-Assisted Multiple Program Realization) System [41, 42, 43], ARIES (Acquisition of Requirements and Incremental Evolution of Specifications) [113], (R)APTS (Rutgers Abstract Program Transformation System) [162], KIDS (Kestrel Interactive Development System) [185], POPART (Producer of Parsers And Related Tools) [201, 202], ZAP [67, 68], and the Munich CIP (Computer-aided, Intuition-guided Programming) project [21, 23, 149]. Comparisons of various transformation systems are presented in [69, 170].

• [x] The name “Abstracto” —

  The lecturer who made that remark was Leo Geurts [73, p57]; he added that “in abstracto” was Dutch [sic!] for “in the abstract”.

• [xi] Criteria for Abstracto —

  These criteria for Abstracto were proposed by Robert Dewar, who was the Group’s chairman at the time [64]. His letter was written in July 1977 [64], in advance of Meeting #23 of the Group in Oxford in December of that year. The New Directions in Algorithmic Languages conferences were in 1975 and 1976, the work of a subcommittee chaired by Robert Dewar and with proceedings [181, 182] edited by Stephen Schuman.

• [xii] Abstracting Abstracto —

  This landmark step was suggested and developed by Richard Bird and Lambert Meertens.

• [xiii] The Boom Hierarchy —

  The Boom hierarchy was introduced by Hendrik Boom [38], and thus namesd “Boom” (by others) — another pun, since Hendrik is Dutch, and “boom” is Dutch for tree. Backhouse [11] presents a detailed study of the Boom Hierarchy, and compares it to the quantifier notation introduced by Edsger Dijkstra and colleagues at Eindhoven.

• [xiv] The appeal to category theory —

  The introduction of concepts from category theory was due to Grant Malcolm [126], based on the work of Hagino [86].

• [xv] The connection between type structure and data structure —

  This observation was made by Martin Löf [130], and later by many others, including by Roland Backhouse in his work on type theory [13].

• [xvi] The Group’s diverse interests —

  Our methods have been applied to separation logic [56], pointer structures [34, 142], database queries [79, 146], geographic information systems [145], climate change [39, 108, 110], scientific computation [109], planning [36] and logistics [172], and domain-specific languages for parsing/pretty printing/program calculation.

• [xvii] Beginner’s programming languages —

  Beginner’s programming languages designed and implemented by Group members include Peter King’s MABEL, Kees Koster’s ELAN, and Lambert Meertens’ ABC [74].

• [xviii] Inspiration for Python —

  ABC’s influence on Python [176] can be seen at Guido van Rossum’s biographical page, and at the ABC and Python pages on Wikipedia:

  https://gvanrossum.github.io/bio.html

  https://en.wikipedia.org/wiki/ABC_(programming_language)

  https://en.wikipedia.org/wiki/Python_(programming_language)

• [xix] Revised Report on ALGOL 68 —

  ALGOL 68 was designed by WG2.1 at the direction of TC2. On December 20, 1968, the language was formally adopted by the Group, and subsequently approved for publication by the General Assembly of IFIP.

• [xx] Example of Abstracto —

  This example is from Lambert Meertens [135].

• [xxi] Refinement calculus —

  The ‘Abstracto vision’ was Lambert Meertens’. It was developed in much greater depth by Ralph Back (independently) [9, 10] and, later, by Carroll Morgan [151, 152]. When Morgan asked Meertens why he had not pursued the refinement calculus further, Meertens’ reply was “It didn’t work.”

• [xxii] Higher-level reasoning —

  Meertens became disillusioned with Abstracto’s low-level transformations, as described in [137]. It was Richard Bird who provided the key insight needed to lift the reasoning to a higher level [30]. Examples are given in [136].

• [xxiii] Program transformations —

  These examples, and many others, were described by Bird [30].

• [xxiv] Evolving notation —

  Bird took the work forwards through the 1980’s, notably in a series of tutorial papers [31, 32, 33] produced in quick succession; an example, the calculation for the Maximum Segment Sum problem, is shown in Fig. 3.

• [xxv] The names “Squiggol” and “BMF” —

  Meertens recalls that Robert Dewar passed a note to him with the single word “Squigol” on it, making a pun with language names such as ALGOL, COBOL, and SNOBOL [138]. The first appearance of the name in the minutes is for Meeting #35 in Sausalito in December 1985. However, it has come to be written “Squiggol”, perhaps to emphasise that the pronunciation should be ˈskwɪgɒl (“qui”) rather than ˈskwaɪgɒl (“quae”). Later, at a meeting of the STOP project in Nijmegen in 1988, Doaitse Swierstra coined the more sober name “Bird–Meertens Formalism” (BMF), making a different pun with “Backus–Naur Form” (BNF).

• [xxvi] The Eindhoven quantifier notation —

  The Eindhoven quantifier notation rationalised the notation for binding a variable, determining its range and forming elements from it [11, 153]. In the conventional $\sum _{n=0}^N n^2$ for example, the n below the $\sum$ is a binding occurrence; but the n in $n^2$ is bound; and the $n^2$ forms elements from that bound variable. The 0 and the N determine the range of n, and the $\sum$ itself gives the ‘quantifier’, the operation (usually associative and commutative) carried out on the elements. In the Eindhoven notation that would be written in the order quantifier, bound variable(s), range, element-former. The whole expression is always enclosed by binding-scope delimiters — so the example above might be written $(+n:0\,{\le }\,n\,{\le }\,N:n^2)$.

  The advantage of using the Eindhoven notation is that uniform calculational laws apply to the manipulation of those expressions, and they greatly reduce the risk of error.

• [xxvii] Catamorphisms —

  Meertens coined the term catamorphism for the unique function induced by a homomorphism from the initial algebra, in a working document presented at Meeting #38 in Rome (1988).

• [xxviii] Datatype-generic programming —

  The term ‘datatype-generic programming’ was coined by Roland Backhouse and Jeremy Gibbons for a project that ran 2003–2006 [14]; the point was to distinguish from the different use of the term ‘generic programming’ in languages like C++, where it essentially means parametric polymorphism. Within the context of the Group, ‘datatype-generic programming’ has come to mean parametrization by a functor, as with catamorphisms, and plain ‘generic programming’ to mean functions defined more specifically over the sum-of-products structure of a polynomial functor, as with PolyP and Generic Haskell.

• [xxix] Polytypic programming languages and PolyP —

  The language PolyP, an extension of the lazy, higher-order functional programming language Haskell [173], was designed by Jansson and Jeuring at Chalmers, Gothenburg [111]. The development of PolyP and its applications was discussed at Meeting #49 in Rancho Santa Fe (1996), Meeting #51 in Oxford (1998), and Meeting #53 in Potsdam (1999).

• [xxx] Generic datatypes with mutual recursion —

  The theory to make Generic Haskell possible was developed by Hinze, a first-time observer in Potsdam (1999). He presented his theory at Meeting #54 in Blackheath (2000) [91]. To support generic functions on sets of mutually recursive datatypes, Hinze, Jeuring, and Löh developed Generic Haskell from 2000 onwards [94, 119]. Various aspects of Generic Haskell were discussed also at Meeting #59 in Nottingham in 2004.

• [xxxi] Type-indexed datatypes —

  Type-indexed datatypes were introduced by Hinze et al. [94]. The type families extension of Haskell is based on the work of Chakravarty et al. [50].

• [xxxii] Fixed-point representation of mutually recursive datatypes —

  Rodriguez and others developed MultiRec [178], a generic programming library that uses a fixed-point representation of possibly mutually recursive datatypes.

• [xxxiii] Generic programming libraries —

  For an early comparison of generic programming libraries, see Rodriguez et al. [177]. An early variant of Scrap Your Boilerplate [118] was discussed at Meeting #56 on Ameland, The Netherlands (2001). Generic Deriving [122] was discussed at Meeting #70 in Ulm.

• [xxxiv] Catamorphisms —

  This work was done mainly by Grant Malcolm [126].

• [xxxv] A zoo of morphisms —

  There were mutumorphisms [71], which are pairs of mutually recursive functions; zygomorphisms [125], which consist of a main recursive function and an auxiliary one on which it depends; histomorphisms [195], in which the body has access to the recursive images of all subterms, not just the immediate ones; so-called generalised folds [28], which use polymorphic recursion to handle nested datatypes; and then there were generic accumulations [163], which keep intermediate results in additional paramters for later stages in the computation.

• [xxxvi] Paramorphism —

  This was introduced by Lambert Meertens at Meeting #41 in Burton, UK (1990) [139].

• [xxxvii] Recursion schemes from comonads —

  This appeared in Uustalu et al [197]. Comonads capture the general idea of ‘evaluation in context’ [196], and this scheme makes contextual information available to the body of the recursion. It was used to subsume both zygomorphisms and histomorphisms.

• [xxxviii] Adjoint folds —

  This was done by Hinze [92]. Using adjunctions as the common thread, adjoint folds arise by inserting a left adjoint functor into the recursive characterisation, thereby adapting the form of the recursion; they subsume paramorphisms, accumulating folds, mutumorphisms (and hence zygomorphisms), and generalised folds. Later, it was observed that adjoint folds could be used to subsume recursion schemes from comonads by Hinze and Wu [93].

• [xxxix] Constructive mathematics and computer programming —

  The connection between constructive mathematics and computer programming was pioneered by the Swedish philosopher and logician Per Martin-Löf [130].

• [xl] Programming languages implementing dependent types —

  Programming languages with dependent types include ALF [124], Cayenne [7], ATS [203], Epigram [132], Agda [159] and Idris [44].

• [xli] Curry-Howard correspondence —

  The Curry-Howard correspondence describes how the typing rules of the lambda calculus are in one-to-one correspondence with the natural deduction rules in logic. Wadler [200] gives a historic overview of this idea, aimed at a more general audience.

• [xlii] Generic programming in dependently typed languages —

  The idea of using dependent types to define an explicit universe of types was one of the early applications of dependently typed programming [4, 27]. Since then, there have been several PhD theses exploring this idea further [53, 57, 115, 155, 123, 159]

• [xliii] WG2.1 and dependent types —

  Backhouse started exploring type theory in the mid 1980’s [13]. At Meeting #42, Nordström was invited as an observer and talked about the work on ALF. Throughout the early 21st century, observers and members were frequently active in the area of type theory or generic programming, including McBride, Löh, Jansson, Swierstra, Dagand, McKinna and many others.

• [xliv] Algebra of programming in Agda —

  Patrik Jansson gave a first tutorial on the dependently typed programming language Agda at Meeting #63 in Kyoto in 2007. This lead to an exploration of how to mechanize the kind of program that was previously carried out on paper [156].

• [xlv] Program calculation and type theory —

  As type theory is a language for describing both proofs and programs, it is no surprise that it provides the ideal setting for formalizing the program calculation techniques that members of the Group pioneered [3, 190, 192].

• [xlvi] Applications of dependent types —

  As languages with dependent types matured, various researchers started exploring novel and unexpected applications in a variety of domains [40, 58, 110, 109].

• [xlvii] Dependently typed combinator parsing —

  This was for example investigated by Nils Danielsson [58].

• [xlviii] Dependent types and program development —

  Many modern dependently typed programming languages are equipped with some sort of IDE. Once the type signature of a method has been fixed, the programmer can interactively find a suitable definition. There are numerous examples of how a powerful type signature can give strong guarantees about a data structure’s invariants [131], the correctness of a domain-specific language [59], or type preservation of a compiler [134].

• [xlix] Dependent types and effects —

  There is a large body of work studying how to incorporate side-effects in dependently typed programming languages. This can be done by constructing denotational models [189, 191], by adding new effectful primitives to the type theory [157], or by giving an algebraic account of the properties that laws that effects satisfy [45, 77].

• [l] Monads —

  This insight was made by Eugenio Moggi while studying semantics of programming languages [141].

• [li] Kleisli arrows —

  Mike Spivey adopted this notion of monads for writing purely functional programs with exceptions [186]; Phil Wadler generalized it to other effects, and popularized it as the main abstraction for dealing with effects in Haskell [198, 199].

• [lii] Parser combinators —

  The combinator style of parsing is due to William Burge [48]. The monadic presentation was popularized by Graham Hutton and Erik Meijer [107], and a dependently typed version presented by Nils Danielsson [xlvii].

• [liii] Parsers in verse —

  The verse characterization of the parser type is due Fritz Ruehr [179].

• [liv] Applicative functors —

  The applicative interface for parsers was invented by Doaitse Swierstra [188]. This and other applications inspired Conor McBride and Ross Paterson to identify the abstraction of applicative functors (also called “strong lax-monoidal functors” or “idioms”) [133]. Like monads, applicative functors have turned out to have unforeseen applications, such as in datatype traversals [29, 78] and distributed computing [75].

• [lv] Algebraic effects —

  Purely functional specifications of effects were studied by Wouter Swierstra in his PhD thesis [189, 191]. The axioms of an algebraic specification can be applied to equational reasoning involving either combinators or the imperative-flavoured comprehension notation provided for example by Haskell’s do notation [77]. Algebraic effects and handlers were introduced by Gordon Plotkin then explored more fully in Matija Pretnar’s PhD thesis [175], and are now the subject of much active work in the Group and beyond.

• [lvi] Applications of relation algebra —

  Roland Backhouse and B.A. Carré discovered similarities between an algebra for path problems and the algebra of regular languages [15]. Tony Hoare and others developed algebraic laws of programming, insisting that “specifications obey all the laws of the calculus of relations” [97]. Richard Bird and Oege de Moor used relations for the calculational derivation of programs covering principles of algorithm design such as dynamic programming, greedy algorithms, exhaustive search and divide and conquer [35].

• [lvii] Algebra of binary relations —

  Calculi based on the algebra of binary relations were developed by George Boole, Charles Peirce, Ernst Schröder, Augustus De Morgan and Alfred Tarski [171, 180, 194].

• [lviii] Graph algorithms —

  Walter Guttmann, for example, showed that the same correctness proof shows that well-known algorithms solve the minimum weight spanning tree problem, the minimum bottleneck spanning tree problem and similar optimisation problems with different aggregation functions [84]. Algebraic versions of Dijkstra’s shortest path algorithm and the one by Floyd/Warshall are applications of these algorithms to structures different from graphs, pinpointing the mathematical requirements on the underlying cost algebra that ensure their correctness [102]. Roland Backhouse and colleagues are currently writing a book on algorithmic graph theory presented relationally [18].

• [lix] Program analysis —

  Program analysis using an algebraic style of reasoning has always been a core activity of the Group; for examples see [62, 63, 66].

• [lx] Pointer structures —

  Bernhard Möller and Richard Bird researched representations of data structures in general, and pointer structures in particular [34, 142].

• [lxi] Algebraic logics —

  An important step to an algebraic form of program logic was taken by Hoare and his colleagues [97]. More recently, the central aspects of Separation Logic [160, 161] were treated algebraically [54, 55, 56].

  Next to programming semantics, the infinite iteration operator can be applied to model various logics. The temporal logics LTL, CTL and CTL$^*$ have been in [60, 114, 150]. There were studies on logics for hybrid systems [100, 101] and Neighbourhood Logic [99].

• [lxii] Further applications of the algebraic approach —

  The Group discovered countless areas in computer science where semirings are the underlying structure. Applications reach from, fundamental concepts of programming language semantics, including concurrent programs [98] and termination [16, 61, 66, 90] via games [12, 17, 183] and data processing [174], to multi-agent systems [144] and quantum computing [193].

  Beyond that, matrix-style reasoning has applications in object-oriented programming [121] and feature-oriented software development, including aspects of product families [106] and of feature interactions [20].

• [lxiii] Algebraic semantics of the while loop —

  The fixed-point characterisation of while loops goes back to Andrzej Blikle and David Park [37, 164]. Dexter Kozen transferred the concept into the setting of Kleene algebras [116].

• [lxiv] Algebras with tests —

  Test elements form a Boolean subalgebra. It represents an algebraic version of the usual assertion logics like the Hoare calculus [117, 147]. There is a direct link to weakest (liberal) preconditions [35, 148].

• [lxv] Fixed-point fusion —

  Fixed-point fusion is a consequence of the fixed-point semantics of recursion [1, 140].

• [lxvi] Virtual data structures —

  These were described by Doaitse Swierstra and Oege de Moor [187].

• [lxvii] Omega algebras —

  The omega operator was introduce by Cohen [51]; Möller performed a systematic study of its foundations [143].

  Guttmann used it for analysing executions of lazy and strict computations [82]. Infinite traces, also called streams, have many applications including the modelling protocols [142], as well as dynamic and hybrid systems [100, 183, 184] . The corresponding algebras can also be used to formally reason about (non)termination in classical programs [104].

• [lxviii] Tool-Support for algebraic reasoning —

  Peter Höfner and Georg Struth proved countless theorems of all these algebras in automated theorem provers, such as Prover9 [103, 105]. Walter Guttmann, Peter Höfner, Georg Struth and others used the interactive proof assistant Isabelle/HOL to implement the algebras, the concrete models, as well as many program derivations, e.g. [5, 6, 80, 83].

• [lxix] Program transformation —

  In the functional realm, fundamental ideas in program transformation were introduced by Cooper [52] and subsequently developed by others, in particular Burstall and Darlington [49]. Later activities occurred within the ISI project [19, 120] and at Kestrel Institute [81]. In the realm of artificial intelligence there were ideas in the field of automated programming (e.g., the DEDALUS system [127] and its successor [128, 129]).

• [lxx] Refinement calculi —

  Imperative programming calculi based on refinement include those of Dijkstra [65], Back [8], Hoare [96, 97], Hehner [87, 88, 89], Morris [154], and Morgan [151, 152].

• [lxxi] Transformational development —

  For background on the ‘life cycle of transformational program development’, see Broy [2]. The five levels of the ‘wide spectrum’ are due to Partsch [168].

• [lxxii] The language CIP-L —

  The language CIP-L is described in detail in the first of two volumes about the CIP project as a whole [24]. For some of the motivation, see Bauer [22] and Broy and Pepper [47].

• [lxxiii] The system CIP-S —

  The specification of the CIP-S system can be found in the second volume about the CIP project [25]. The more interesting parts of the formal development of the system, together with the transformation rules used, can also be found there. Successors to CIP-S were developed by Partsch [169] and Guttmann et al. [85].

• [lxxiv] Experiences with CIP —

  Smaller CIP case studies include sorting [46, 165] and parsing [166, 167, 168]. As noted above, the CIP-S system itself [25] constitutes a larger case study.

• [lxxv] Programs should be grown —

  Fred Brooks wrote “Some years ago Harlan Mills proposed that any software system should be grown by incremental development.” [72]