Internal lenses as functors and cofunctors

TL;DR

This paper introduces a unified framework for lenses as functors and cofunctors within categories with pullbacks, simplifying their composition and connecting various lens types.

Contribution

It presents a novel internal categorical perspective on lenses, unifying classical, c-, and d-lenses as functors and cofunctors, with a canonical representation.

Findings

Lenses can be represented as a commuting triangle of functors.

Unified framework simplifies lens composition.

Connects classical, c-, and d-lenses within a single categorical model.

Abstract

Lenses may be characterised as objects in the category of algebras over a monad, however they are often understood instead as morphisms, which propagate updates between systems. Working internally to a category with pullbacks, we define lenses as simultaneously functors and cofunctors between categories. We show that lenses may be canonically represented as a particular commuting triangle of functors, and unify the classical state-based lenses with both c-lenses and d-lenses in this framework. This new treatment of lenses leads to considerable simplifications that are important in applications, including a clear interpretation of lens composition.