Solutions to the longest increasing subsequence problem are typically implemented imperatively, relying on arrays for constant-time lookups and updates. Replacing these arrays with functional sequences allows a purely functional solution with the same asymptotic running time, but with significantly worse practical performance. In this pearl, we present a purely functional approach that is not only asymptotically optimal, but also efficient in practice. The core idea is to exploit the interplay between search, lookup, and update operations through Huet’s zipper. In addition, we improve the adaptive behaviour of imperative solutions commonly found in the literature.

Many programs process lists by recursing in a wide variety of sequential and/or divide-and-conquer patterns. Reasoning about the correctness and completeness of these programs requires reasoning about the lengths of the lists, techniques for which are typically undecidable or at least NP-complete. In this paper we show how introducing a relatively simple (sub-)language for expressions describing list lengths, whilst not completely general, covers a great number of these patterns. It includes not only doubling but also exponentiation (iterated doubling), and moreover admits a simple length-checking algorithm that is complete over a predictable problem domain. We prove termination of the algorithm via category-theoretic pullbacks, formalized in Agda, as well as providing a more realistic implementation in Rocq, and a toy language Fulbourn with interpreter in Haskell.

Functional programmers have many things for which to thank the late David Turner: design decisions he made in his languages SASL, KRC, and Miranda over the last 50 years are still influential and inspirational now. In particular, Turner was a strong advocate of lazy evaluation and of list comprehensions. As an illustration of these techniques, he popularized a one-line recursive “sieve” to generate the infinite list of prime numbers. Turner called this algorithm The Sieve of Eratosthenes. In a lovely paper called “The Genuine Sieve of Eratosthenes”, Melissa O’Neill argued that Turner’s program is not in fact a faithful implementation of the algorithm, and gave a detailed presentation using priority queues of the real thing. She included a variation by Richard Bird, which uses only lists but makes clever use of circular programming. Bird describes his circular program again in his textbook “Thinking Functionally with Haskell”, and sets its proof of correctness as an exercise. In particular, why is this circular program productive? Unfortunately, Bird’s hint for a solution is incorrect. So what should a proof look like? One of the last projects Turner worked on was the notion of “Total Functional Programming”. He observed that most programs are already structurally recursive or corecursive, therefore guaranteed respectively terminating or productive; he conjectured that “with more practice we will find this is always true”. We explore Bird’s circular Sieve of Eratosthenes as a challenge problem for Turner’s Total Functional Programming.

The observation that program structure follows data structure is a key lesson in introductory programming: good hints for possible program designs can be found by considering the structure of the data concerned. In particular, this lesson is a core message of the influential textbook “How to Design Programs” by Felleisen, Findler, Flatt, and Krishnamurthi. However, that book discusses using only the structure of input data for guiding program design, typically leading towards structurally recursive programs. We argue that novice programmers should also be taught to consider the structure of output data, leading them also towards structurally corecursive programs.

Bulk types such as sets, bags, and lists are monads, and therefore support a notation for database queries based on comprehensions. This fact is the basis of much work on database query languages. The monadic structure easily explains most of standard relational algebra—specifically, selections and projections—allowing for an elegant mathematical foundation for those aspects of database query language design. Most, but not all: monads do not immediately offer an explanation of relational join or grouping, and hence important foundations for those crucial aspects of relational algebra are missing. The best they can offer is cartesian product followed by selection. Adjunctions come to the rescue: like any monad, bulk types also arise from certain adjunctions; we show that by paying due attention to other important adjunctions, we can elegantly explain the rest of standard relational algebra. In particular, graded monads provide a mathematical foundation for indexing and grouping, which leads directly to an efficient implementation, even of joins.

We consider the task of constructing 2-3 trees. Given a sequence of elements we seek to build a 2-3 tree–in linear time–that contains the elements in symmetric order. We discuss three approaches: top-down, bottom-up, and incremental. The incremental approach is more flexible than the other two in that it allows us to interleave the construction work with other operations, for example, queries.