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.  Previous 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. It has recently been shown that lenses are the coalgebras for the comonad generated by the cartesian closure adjunction on Set. In this paper, we present an equational proof of the coalgebra correspondence, note that the algebra correspondence extends to arbitrary categories with products and that the coalgebra correspondence extends to arbitrary cartesian closed categories, and 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 its underlying generality and 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.