Composite data structures have components, and those components should be referenceable. Examples include the fields of a record, the variants of a union, and the elements of a container; one should be able to refer to “the root of the left child (if present)” of a binary tree node.
Individual data accessors for simple data structures are easy to write, for example as pairs of “getter” and “setter” methods. However, it is not obvious how to combine component references, in such a way that the reference for a component within a compound data structure is composed out of smaller references within the parts of that structure. Generally, one has to write a sequence of statements or declarations that navigate step by step through the data structure, accessing one level at a time—which is to say, component references are traditionally not first-class citizens, combinable in their own right.
I will describe profunctor optics, a neat representation of component references that naturally supports composition. The profunctor representation exploits higher-order functions (“lambdas”) and higher-kinded types (“generics”), so serves as a compelling argument for the value of these language features. It turns out to be a fairly direct application of the Yoneda Lemma, arguably the most important result in category theory, for which we hope to provide some insight.
I am Professor of Computing in the Department of Computer Science at the University of Oxford. I am currently Director of the Software Engineering Programme, which offers part-time professional Masters’ degrees in Software Engineering and in Software and Systems Security. I also lead the Algebra of Programming research group. I am Editor-in-Chief of the Journal of Functional Programming, Past Vice Chair of ACM SIGPLAN, Past Chair of IFIP WG2.1. Before taking up this post in 1999, I held lectureships at Oxford Brookes University and the University of Auckland, New Zealand.
Mon 5 NovDisplayed time zone: Guadalajara, Mexico City, Monterrey change
16:30 - 17:30 | |||
16:30 60mTalk | Composable References and the Yoneda Lemma SPLASH-I Jeremy Gibbons University of Oxford Link to publication Pre-print |