Skip to main content
Upcoming Events:
Distinguished Lecture Series: Jeremy Gibbons, University of Oxford

Distinguished Lecture Series: Jeremy Gibbons, University of Oxford

Date & Time:
   Add All to Calendar


Event Contact:

Dr. Fei Chiang, Dr. Jacques Carette


Concrete computations from abstract algebra; or, "You can tell a lot about a person by the company they keep"
A recent trend in functional programming has been to concretize highly abstract mathematics, mostly various forms of logic and category theory, revealing practical applications for actual programs.  One prime example is the Yoneda Lemma, which has been called "arguably the most important result in category theory".  Despite this central importance, the Yoneda Lemma has a very short statement, a very simple proof, and a number of familiar special cases. One such application is the "rule of indirect inequality", that B<=A if and only if A<=C implies B<=C for every C. Another application is Cayley's Theorem, which explains the "accumulating parameter" technique - for example, transforming a naive quadratic-time reverse function into a linear-time one.

I will present another application of the Yoneda Lemma, using it to derive so-called "profunctor optics". These are a class of "bidirectional data accessors", which arose from database applications. The database-inspired approach entails gadgets called "lenses" and "prisms" -- essentially partial projections and partial pattern matches, respectively -- represented as pairs of "getter" and "setter" functions. But this representation is inconvenient to work with, and does not compose well. In contrast, the "profunctor" representation -- exploiting the bread-and-butter tools of modern typed functional programming, namely higher-order functions and higher-kinded types -- is neat and composable. The relationship between the two representations is not at all obvious; however, it turns out to be a fairly direct application of Yoneda. (This is joint work with my student Guillaume Boisseau.)

Bio: Jeremy Gibbons is Professor of Computing at the University of Oxford, where he teaches on the part-time professional Master's programme in Software Engineering. He is Editor-in-Chief of the Journal of Functional Programming, and until recently served as Chair of IFIP Working Group 2.1 on Algorithmic Languages and Calculi and Vice Chair of ACM SIGPLAN, the ACM Special Interest Group on Programming Languages.