Dependent Optics

TL;DR

This paper introduces a unified framework for dependent optics, encompassing various bidirectional data accessors, and classifies them using Tambara representations to generalize existing profunctor encodings.

Contribution

It formalizes dependent optics within a category-theoretic framework, defines their properties, and extends profunctor encoding to the dependent case.

Findings

Defined the category of dependent optics from indexed categories

Established conditions for the existence of coproducts in dependent optics

Generalized profunctor encoding via Tambara representations

Abstract

A wide variety of bidirectional data accessors, ranging from mixed optics to functor lenses, can be formalized within a unique framework-dependent optics. Starting from two indexed categories, which encode what maps are allowed in the forward and backward directions, we define the category of dependent optics and establish under what assumptions it has coproducts. Different choices of indexed categories correspond to different families of optics: we discuss dependent lenses and prisms, as well as closed dependent optics. We introduce the notion of Tambara representation and use it to classify contravariant functors from the category of optics, thus generalizing the profunctor encoding of optics to the dependent case.