Person. Jeremy Gibbons

Papers

Turner, Bird, Eratosthenes: An eternal burning thread gibbons-2025-turner

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.
PDF · DOI · pldb

Profunctor Optics, a Categorical Update clarke-2024-profunctor

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.
DOI · arXiv

Breadth-First Traversal via Staging gibbons-2022-breadth

DOI

Algorithm Design with the Selection Monad hartmann-2022-algorithm

DOI

Continuation-Passing Style, Defunctionalization, Accumulations, and Associativity gibbons-2021-continuation

DOI

Algorithmics bird-2021-algorithmics

DOI

How to design co-programs gibbons-2021-how

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.
PDF · DOI · pldb

Algorithm Design with Haskell bird-2020-algorithm

DOI

The School of Squiggol: A History of the Bird–Meertens Formalism gibbons-2020-the

DOI

What you needa know about Yoneda: profunctor optics and the Yoneda lemma (functional pearl) boisseau-2018-what

Profunctor optics are a neat and composable representation of bidirectional data accessors, including lenses, and their dual, prisms. The profunctor representation exploits higher-order functions and higher-kinded type constructor classes, but the relationship between this and the familiar representation in terms of “getter” and “setter” functions is not at all obvious. We derive the profunctor representation from the concrete representation, making the relationship clear. It turns out to be a fairly direct application of the Yoneda Lemma, arguably the most important result in category theory. We hope this derivation aids understanding of the profunctor representation. Conversely, it might also serve to provide some insight into the Yoneda Lemma.
PDF · DOI · pldb

Relational algebra by way of adjunctions gibbons-2018-relational

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.
PDF · DOI · pldb

Profunctor Optics: Modular Data Accessors pickering-2017-profunctor

DOI

Conjugate Hylomorphisms -- Or: The Mother of All Structured Recursion Schemes hinze-2015-conjugate

PDF · DOI · pldb

Folding domain-specific languages: deep and shallow embeddings (functional Pearl) gibbons-2014-folding

PDF · DOI · pldb

Just do it: simple monadic equational reasoning gibbons-2011-just

PDF · DOI · pldb

The essence of the Iterator pattern gibbons-2009-the

The Iterator pattern gives a clean interface for element-by-element access to a collection, independent of the collection’s shape. Imperative iterations using the pattern have two simultaneous aspects: mapping and accumulating . Various existing functional models of iteration capture one or other of these aspects, but not both simultaneously. We argue that C. McBride and R. Paterson’s applicative functors (Applicative programming with effects, J. Funct. Program. , 18 (1): 1–13, 2008), and in particular the corresponding traverse operator, do exactly this, and therefore capture the essence of the Iterator pattern. Moreover, they do so in a way that nicely supports modular programming. We present some axioms for traversal, discuss modularity concerns and illustrate with a simple example, the wordcount problem.
PDF · DOI · pldb

Datatype-Generic Programming gibbons-2007-datatype

DOI

Unbounded Spigot Algorithms for the Digits of Pi gibbons-2006-unbounded

DOI
jeremygibbons person entries/rolodex/jeremygibbons.hel