Towards a unified framework for Functional Optics implementation and verification

This project falls within the EPSRC Programming Languages research area.

Modularity is at the heart of good software engineering. It allows for efficient software development, and enables reasoning about correctness at scale.
In the context of structured data, modularity usually comes from compound data types, i.e. data types made of the composition of elementary shapes (sums, products, mappings). However, even though compound data types are modular, manipulating them is less directly so: one usually needs to write combinators on a case-by-case basis for a given compound datatype.

The recent years have seen the development of a class of tools to solve this problem in a generic way, called functional references, or functional optics. Generalizing from the simple idea of a lens from the bidirectional programming literature[1], functional optics define families of combinators to query, access and modify certain elementary shapes[3][9]. Together they generalize well-known programming patterns such as iterators[2] and folds[4], and allow them to be composed in arbitrary ways while ensuring type safety.
These tools are becoming more and more common in the functional programmer's toolbox, especially in Haskell where most of their development has taken place. Despite their popularity in the software development world, optics have yet received little attention from the academic world. This project will aim at closing this gap by bringing theoretical grounding and foundation to the study of optics.

Using advanced reasoning techniques from category theory[7][6] and recent insights into the algebraic structure of optics[8][5], this project aims at developing a generic algebraic framework for specifying optics, as well as a unified description of optics well-behavedness laws to allow for modular verification of programs constructed with optics. Its objectives are providing a base for reasoning about optics and programs that use them, in addition to enabling specification of both efficient and correct implementations of those combinators.
This project relates to the EPSRC Programming Languages area and aligns with its objective to help development of reliable and robust software systems.
This project will be realized under the supervision of Prof. Jeremy Gibbons at the Department of Computer Science of the University of Oxford.

References
[1] J. Nathan Foster et al. "Combinators for Bi-directional Tree Transformations: A Linguistic Approach to the View Update Problem". In: SIGPLAN Not. (Jan. 2005).
[2] Jeremy Gibbons and Bruno César dos Santos Oliveira. "The Essence of the Iterator Pattern". In: Journal
of Functional Programming 19.3-4 (2009), pp. 377-402. DOT: 10.1017/S0956796809007291. URL: http: //www.comlab.ox.ac.uk/jeremy.gibbons/publications/iterator.pdf.
[3] Edward Kmett. Haskell Lens library. URL: https://hackage.haskell.org/package/lens.
[4] Edward Kmett. Haskell Lens library: Control.Lens.Fold. URL: https://hackage.haskell.org/package/ lens/docs/Control-Lens-Fold.html.

[5] Bartosz Milewski. Profunctor Optics: The Categorical View. URL: https://bartoszmilewski.com/2017/ 07/07/profunctor-optics-the-categorical-view/.
[6] nLab: Coalgebra. URL: https://ncatlab.org/nlab/show/coalgebra.
[7] nLab: End. URL: https://ncatlab.org/nlab/show/end.
[8] Matthew Pickering, Jeremy Gibbons, and Nicolas Wu. "Profunctor Optics - Modular Data Accessors". 2017.
[9] Purescript Lens library. URL: https://pursuit.purescript.org/packages/purescript-profunctor-lenses/2.2. 0.