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.

This paper explores a novel approach to selection functions through the introduction of a generalised selection monad. The foundation is laid with the conventional selection monad J , defined as (A → R) → A , together with various combinators for computing new selection functions from old. However, inefficiencies in these combinators are identified. To address these issues, a specialised type K is introduced, and its isomorphism to J is demonstrated. The paper further generalises the K type to G , where performance improvements and enhanced intuitive usability are observed. The embeddings between J and G are established, offering a more efficient and expressive alternative to the well established J type for selection functions. The findings emphasise the advantages of the generalised selection monad and its applicability in diverse scenarios, paving the way for further exploration and optimisation.

We reconstruct some of the development in Richard Bird's [2008] paper Zippy Tabulations of Recursive Functions, using dependent types and string diagrams rather than mere simple types. This paper serves as an intuitive introduction to and demonstration of these concepts for the curious functional programmer, who ideally already has some exposure to dependent types and category theory, is not put off by basic concepts like indexed types and functors, and wants to see a more practical example. The paper is presented in the form of a short story, narrated from the perspective of a functional programmer trying to follow the development in Bird's paper. The first section recaps the original simply typed presentation. The second section explores a series of refinements that can be made using dependent types. The third section uses string diagrams to simplify arguments involving functors and naturality. The short story ends there, but the paper concludes with a discussion and reflection in the afterword.

Optics are bidirectional data accessors that capture data transformation patterns such as accessing subfields or iterating over containers. Profunctor optics are a particular choice of representation supporting modularity, meaning that we can construct accessors for complex structures by combining simpler ones. Profunctor optics have previously been studied only in an unenriched and non-mixed setting, in which both directions of access are modelled in the same category. However, functional programming languages are arguably better described by enriched categories; and we have found that some structures in the literature are actually mixed optics, with access directions modelled in different categories. Our work generalizes a classic result by Pastro and Street on Tambara theory and uses it to describe mixed V-enriched profunctor optics and to endow them with V-category structure. We provide some original families of optics and derivations, including an elementary one for traversals. Finally, we discuss a Haskell implementation.

The selection monad has proven useful for modelling exhaustive search algorithms. It is well studied in the area of game theory as an elegant way of expressing algorithms that calculate optimal plays for sequential games with perfect information; composition of moves is modeled as a 'product' of selection functions. This paper aims to expand the application of the selection monad to other classes of algorithms. The structure used to describe exhaustive search problems can easily be applied to greedy algorithms; with some changes to the product function, the behaviour of the selection monad can be changed from an exhaustive search behaviour to a greedy one. This enables an algorithm design framework in which the behaviour of the algorithm can be exchanged modularly by using different product functions.

The large-scale structure of executing a computation can often be thought of as being separated into distinct phases . But the most natural form in which to specify that computation may well have a different and conflicting structure. For example, the computation might consist of gathering data from some locations, processing it, then distributing the results back to the same locations; it may be executed in three phases—gather, process, distribute—but mostly conveniently specified orthogonally—by location. We have recently shown that this multi-phase structure can be expressed as a novel applicative functor (also known as an idiom , or lax monoidal functor). Here we summarize the idea from the perspective of software architecture. At the end, we speculate about applications to choreography and multi-tier architecture.

An effectful traversal of a data structure iterates over every element, in some predetermined order, collecting computational effects in the process. Depth-first effectful traversal of a tree is straightforward to define compositionally, since it precisely follows the shape of the data. What about breadth-first effectful traversal? An indirect route is to factorize the data structure into shape and contents, traverse the contents, then rebuild the data structure with new contents. We show that this can instead be done directly using staging, expressed using a construction related to free applicative functors. The staged traversals lend themselves well to fusion; we prove a novel fusion rule for effectful traversals, and use it in another solution to Bird’s ‘repmin’ problem.

Abstract 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.

Context: Reynolds showed us how to use continuation-passing style and defunctionalization to transform a recursive interpreter for a language into an abstract machine for programs in that language. The same techniques explain other programming tricks, including zippers and accumulating parameters. Inquiry: Buried within all those applications there is usually a hidden appeal to the algebraic property of associativity. Approach: Our purpose in this paper is to entice associativity out of the shadows and into the limelight. Knowledge: We revisit some well-known applications (factorial, fast reverse, tree flattening, and a compiler for a simple expression language) to spotlight their dependence on associativity. Grounding: We replay developments of these programs through a series of program transformations and data refinements, justified by equational reasoning. Importance: Understanding the crucial role played by associativity clarifies when continuation-passing style and defunctionalization can help and when they cannot, and may prompt other applications of these techniques.

The Bird–Meertens Formalism, colloquially known as “Squiggol”, is a calculus for program transformation by equational reasoning in a function style, developed by Richard Bird and Lambert Meertens and other members of IFIP Working Group 2.1 for about two decades from the mid 1970s. One particular characteristic of the development of the Formalism is fluctuating emphasis on novel ‘squiggly’ notation: sometimes favouring notational exploration in the quest for conciseness and precision, and sometimes reverting to simpler and more rigid notational conventions in the interests of accessibility. This paper explores that historical ebb and flow.

What does a probabilistic program actually compute? How can one formally reason about such probabilistic programs? This valuable guide covers such elementary questions and more. It provides a state-of-the-art overview of the theoretical underpinnings of modern probabilistic programming and their applications in machine learning, security, and other domains, at a level suitable for graduate students and non-experts in the field. In addition, the book treats the connection between probabilistic programs and mathematical logic, security (what is the probability that software leaks confidential information?), and presents three programming languages for different applications: Excel tables, program testing, and approximate computing. This title is also available as Open Access on Cambridge Core.

Monads are a popular feature of the programming language Haskell because they can model many different notions of computation in a uniform and purely functional way. Our particular interest here is the probability monad, which can be – and has been – used to synthesise models for probabilistic programming. Quantitative Information Flow, or QIF, arises when security is combined with probability, and concerns the measurement of the amount of information that ‘leaks’ from a probabilistic program’s state to a (usually) hostile observer: that is, not “whether” leaks occur but rather “how much?” Recently it has been shown that QIF can be seen monadically, a ‘lifting’ of the probability monad from (simply) distributions to distributions of distributions – so called “hyper-distributions”. Haskell’s support for monads therefore suggests a synthesis of an executable model for QIF. Here we provide the first systematic and thorough account of doing that: using distributions of distributions to synthesise a model for Quantitative Information Flow in terms of monads in Haskell.