Understanding Profunctor Optics: a representation theorem
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 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
11:00 - 12:30 | Mathematical FoundationsBx at Baie des Anges B Chair(s): Jeremy Gibbons Department of Computer Science, University of Oxford | ||
11:00 30mFull-paper | Cospans and Symmetric Lenses Bx | ||
11:30 30mShort-paper | Understanding Profunctor Optics: a representation theorem Bx | ||
12:00 30mTalk | Bimorphic lenses in compositional game theory Bx Jules Hedges University of Oxford |