Understanding Profunctor Optics: a representation theorem

Optics, aka functional references, are classes of tools that allow composable access into compound data structures. Usually defined as programming language libraries, they provide combinators to manipulate different shapes of data such as sums, products and collections, that can be composed to operate on larger structures. Together they form a powerful language to describe transformations of data. Among the different approaches to describing optics, one particular type of optics, called profunctor optics, stands out. It describes alternative but equivalent representations of most of the common combinators, and enhances them with elegant composability properties via a higher-order encoding. Notably, it enables easy composition across different optic families. Unfortunately, profunctor optics are difficult to reason about, and linking usual optics with an equivalent profunctor representation has so far been done on a case-by-case basis, with definitions that sometimes seem very ad hoc. This makes it hard both to analyse properties of existing profunctor optics and to define new ones. This thesis presents an equivalent representation of profunctor optics, called isomorphism optics, that is both closer to intuition and easier to reason about. This tool enables powerful theorems to be derived generically about profunctor optics. Finally, this thesis develops a framework to ease deriving new profunctor encodings from concrete optic families.