Relating Algebraic and Coalgebraic Descriptions of Lenses

Abstract

Lenses are a heavily studied form of bidirectional transformation with diverse applications including database view updating, software development and memory management. Recent work has explored lenses category theoretically, and established that the category of lenses for a fixed "view" V is, up to isomorphism, the category of algebras for a particular monad on Set/V. In this paper we show that in addition lenses are the coalgebras for the comonad generated by the cartesian closure adjunction on Set. We present a fully constructive proof of the coalgebra correspondence, we note that the algebra correspondence extends to arbitrary categories with products and that the coalgebra correspondence extends to arbitrary cartesian closed categories, and we show that both correspondences extend to isomorphisms of categories. The resulting isomorphism between a category of algebras and a category of coalgebras is unexpected, and we analyze it isolating its underlying generality, and also the particularity that restricts its applicability. We end with remarks about the utility of the two different treatments of lenses,especially for obtaining further, more realistic, generalizations of the notion of lens.