Guillaume Boisseau
Jeremy Gibbons
Skip Abstract Section
Skip Supplemental Material SectionAbstract
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.
Supplemental Material
- Theodor Adorno. 1956. Fragment über Musik und Sprache. Reprinted in Gesammelte Schriften, Band 16: Musikalische Schriften I–III, Suhrkamp Verlag, 1978, p251–256.Google Scholar
- Kazuyuki Asada. 2010. Arrows are Strong Monads. In Mathematically Structured Functional Programming. ACM. Google ScholarDigital Library
- Alexey Avramenko. 2017. Yoneda and Coyoneda Trick. (April 2017). https://medium.com/@olxc/ yoneda- and- coyoneda- trick- f5a0321aeba4 .Google Scholar
- Steve Awodey. 2006. Category Theory. Oxford University Press.Google ScholarDigital Library
- Roland Backhouse. 2003. Program Construction: Calculating Implementations from Specifcations. Wiley. Google ScholarDigital Library
- F. Bancilhon and N. Spyratos. 1981. Update Semantics of Relational Views. ACM Trans. Database Syst. 6, 4 (Dec. 1981), 557–575. Google ScholarDigital Library
- Richard S. Bird. 1984. The Promotion and Accumulation Strategies in Transformational Programming. ACM Transactions on Programming Languages and Systems 6, 4 (Oct. 1984), 487–504. Google ScholarDigital Library
- Edsger W. Dijkstra. 1991. Why Preorders Are Beautiful. (June 1991). EWD1102; available from http://www.cs.utexas.edu/ ~EWD/ewd11xx/EWD1102.PDF .Google Scholar
- Wim Feijen. 2001. The Joy of Formula Manipulation. Inform. Process. Lett. 77 (2001), 89–96. Google ScholarDigital Library
- J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce, and Alan Schmitt. 2005. Combinators for Bidirectional Tree Transformations: A Linguistic Approach to the View Update Problem. In Principles of Programming Languages. ACM Press, 233–246. Google ScholarDigital Library
- Jeremy Gibbons. 2016. Free Delivery (Functional Pearl). In Haskell Symposium. ACM, 45–50. Google ScholarDigital Library
- Jeremy Gibbons. 2017. APLicative Programming with Naperian Functors. In European Symposium on Programming (Lecture Notes in Computer Science), Hongseok Yang (Ed.), Vol. 10201. Springer Berlin Heidelberg, 556–583.Google Scholar
- Jeremy Gibbons and Bruno César dos Santos Oliveira. 2009. The Essence of the Iterator Pattern. Journal of Functional Programming 19, 3,4 (2009), 377–402. Google ScholarDigital Library
- Oleg Grenrus. 2017. Affine Traversal. http://oleg.fi/gists/posts/2017- 03- 20- affine- traversal.htmlGoogle Scholar
- Peter Hancock. 2005. What is a Naperian Container? (June 2005). http://sneezy.cs.nott.ac.uk/containers/blog/?p=14 .Google Scholar
- Ralf Hinze and Daniel W. H. James. 2010. Reason Isomorphically!. In Workshop on Generic Programming, Bruno C. d. S. Oliveira and Marcin Zalewski (Eds.). ACM, 85–96. Google ScholarDigital Library
- R. John Muir Hughes. 1986. A Novel Representation of Lists and Its Application to the Function ‘Reverse’. Inform. Process. Lett. 22 (1986), 141–144. Google ScholarDigital Library
- Mauro Jaskelioff and Russell O’Connor. 2015. A Representation Theorem for Second-Order Functionals. Journal of Functtional Programming 25 (2015).Google Scholar
- Edward Kmett. 2015. profunctor library, Version 5. https://hackage.haskell.org/package/profunctors- 5Google Scholar
- Edward Kmett. 2018. lens library, Version 4.16. https://hackage.haskell.org/package/lens- 4.16Google Scholar
- Tom Leinster. 2000. The Yoneda Lemma: What’s It All About? (Oct. 2000). http://www.maths.ed.ac.uk/~tl/categories/ yoneda.ps .Google Scholar
- Saunders Mac Lane. 1971. Categories for the Working Mathematician. Springer-Verlag.Google Scholar
- Oleksandr Manzyuk. 2013. Co-Yoneda Lemma. (Jan. 2013). https://oleksandrmanzyuk.wordpress.com/2013/01/18/ co- yoneda- lemma/ .Google Scholar
- Kazutaka Matsuda and Meng Wang. 2015. Applicative Bidirectional Programming with Lenses. In International Conference on Functional Programming, Kathleen Fisher and John H. Reppy (Eds.). ACM, 62–74. Google ScholarDigital Library
- Shoukei Matsumoto. 2018. I Clean, Therefore I Am. The Guardian (5th January 2018). https://www.theguardian.com/ commentisfree/2018/jan/05/buddhist- monk- cleaning- good- for- you .Google Scholar
- Guerino Mazzola. 2002. The Topos of Music. Birkhäuser.Google Scholar
- Conor McBride and Ross Paterson. 2008. Applicative Programming with Effects. Journal of Functional Programming 18, 1 (2008), 1–13. Google ScholarDigital Library
- Bartosz Milewski. 2017a. Profunctor Optics: The Categorical Approach. https://www.youtube.com/watch?v=l1FCXUi6Vlw . Keynote at Lambda World conference, Cadiz.Google Scholar
- Bartosz Milewski. 2017b. Profunctor Optics: The Categorical View. (July 2017). https://bartoszmilewski.com/2017/07/07/ profunctor- optics- the- categorical- view/ .Google Scholar
- Max New. 2017. Closure Conversion as CoYoneda. (Aug. 2017). http://prl.ccs.neu.edu/blog/2017/08/28/ closure- conversion- as- coyoneda/ .Google Scholar
- Russell O’Connor. 2014. Mainline Profunctor Hierarchy for Optics. http://r6research.livejournal.com/27476.htmlGoogle Scholar
- Russell O’Connor. 2015a. Grate: A new kind of Optic. https://r6research.livejournal.com/28050.htmlGoogle Scholar
- Russell O’Connor. 2015b. mezzolens library, Version 0. https://hackage.haskell.org/package/mezzolens- 0Google Scholar
- Matthew Pickering, Jeremy Gibbons, and Nicolas Wu. 2017. Profunctor Optics: Modular Data Accessors. The Art, Science, and Engineering of Programming 1, 2 (2017), Article 7.Google Scholar
- Dan Piponi. 2006. Reverse Engineering Machines with the Yoneda Lemma. (Nov. 2006). http://blog.sigfpe.com/2006/11/ yoneda- lemma.html .Google Scholar
- Emily Riehl. 2016. Category Theory in Context. Dover Publications. Available from http://www.math.jhu.edu/~eriehl/ context.pdf .Google Scholar
- Mike Stay. 2008. The Continuation Passing Transform and the Yoneda Embedding. (Jan. 2008). https://golem.ph.utexas.edu/ category/2008/01/the_continuation_passing_trans.html .Google Scholar
- Perdita Stevens. 2010. Bidirectional Model Transformations in QVT: Semantic Issues and Open Questions. Software and System Modeling 9, 1 (2010), 7–20.Google ScholarCross Ref
- Paul Valéry. 1937. Leçon Inaugurale du Cours de Poétique du Collège de France. Reprinted in Variété V, Gallimard, 1944, p295–322.Google Scholar
- Twan van Laarhoven. 2009. CPS-Based Functional References. (July 2009). http://www.twanvl.nl/blog/haskell/ cps- functional- referencesGoogle Scholar
- Burghard von Karger. 2002. Temporal Algebra. In Algebraic and Coalgebraic Methods in the Mathematics of Program Construction (Lecture Notes in Computer Science), Roland Backhouse, Roy Crole, and Jeremy Gibbons (Eds.), Vol. 2297. Springer-Verlag, 310–386. Google ScholarDigital Library
- Philip Wadler. 1987. The Concatenate Vanishes. (Dec. 1987). University of Glasgow. Revised November 1989.Google Scholar
Index Terms
- What you needa know about Yoneda: profunctor optics and the Yoneda lemma (functional pearl)
Recommendations
Formalizing the ∞-Categorical Yoneda Lemma
CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and ProofsFormalized 1-category theory forms a core component of various libraries of mathematical proofs. However, more sophisticated results in fields from algebraic topology to theoretical physics, where objects have “higher structure,” rely on infinite-...
Communes via Yoneda, from an Elementary Perspective
From Mathematical Beauty to the Truth of Nature: to Jerzy Tiuryn on his 60th BirthdayWe present the Yoneda Lemma in terms of categories without explicit reference to the notion of functor. From this perspective we then define a commune as a common generalization of Chu spaces and presheaves, and give some applications.
Comments