## Understanding Profunctor Optics: a representation theorem

**Tue 10 Apr 2018 11:30 - 12:00 at Baie des Anges B**- Mathematical Foundations Chair(s): Jeremy Gibbons

Profunctor optics are composable building blocks used to define bidirectional data accessors. They form a powerful language to describe transformations of data. Unfortunately, contrary to more familiar optics like put-get lenses, profunctor optics have a complex type that makes them difficult to reason about. Moreover, linking usual optics with an equivalent profunctor representation has so far been done on a case-by-case basis, with definitions that sometimes feel very ad hoc. This makes it hard both to analyse properties of existing profunctor optics and to define new ones. This extended abstract proposes a general form for profunctor optics, and presents an equivalent representation called existential optics that is closer to intuition. This representation enables easier understanding of how profunctor optics function and are combined, as well as easier definition of useful new such optics.

#### Tue 10 Apr

11:00 - 12:30: Bx 2018 - Mathematical Foundations at Baie des Anges B Chair(s): Jeremy GibbonsDepartment of Computer Science, University of Oxford | ||||||||||||||||||||||||||||||||||||||||||

11:00 - 11:30Full-paper | ||||||||||||||||||||||||||||||||||||||||||

11:30 - 12:00Short-paper | ||||||||||||||||||||||||||||||||||||||||||

12:00 - 12:30Talk | Jules HedgesUniversity of Oxford |