  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.
