Space-time tradeoffs of lenses and optics via higher category theory

TL;DR

This paper explores the space-time tradeoffs in lenses and optics using higher category theory, revealing operational differences and lifting categorical structures to the 2-categorical level for better understanding.

Contribution

It introduces a 2-category framework that captures internal configurations of optics, clarifies the relationship between lenses and optics, and discusses the limitations of existing categorical models.

Findings

Operational differences between cartesian optics and lenses are characterized.

A 2-category $ extbf{2-Optic}( extbf{C})$ is defined to track internal configurations.

The relationship between lenses and optics is explained via a lax 2-adjunction.

Abstract

Optics and lenses are abstract categorical gadgets that model systems with bidirectional data flow. In this paper we observe that the denotational definition of optics - identifying two optics as equivalent by observing their behaviour from the outside - is not suitable for operational, software oriented approaches where optics are not merely observed, but built with their internal setups in mind. We identify operational differences between denotationally isomorphic categories of cartesian optics and lenses: their different composition rule and corresponding space-time tradeoffs, positioning them at two opposite ends of a spectrum. With these motivations we lift the existing categorical constructions and their relationships to the 2-categorical level, showing that the relevant operational concerns become visible. We define the 2-category $\textbf{2-Optic}(\mathcal{C})$ whose 2-cells explicitly track optics' internal configuration. We show that the 1-category $\textbf{Optic}(\mathcal{C})$ arises by locally quotienting out the connected components of this 2-category. We show that the embedding of lenses into cartesian optics gets weakened from a functor to an oplax functor whose oplaxator now detects the different composition rule. We determine the difficulties in showing this functor forms a part of an adjunction in any of the standard 2-categories. We establish a conjecture that the well-known isomorphism between cartesian lenses and optics arises out of the lax 2-adjunction between their double-categorical counterparts. In addition to presenting new research, this paper is also meant to be an accessible introduction to the topic.