Relating algebraic and coalgebraic descriptions of lenses

Jeremy Gibbons, Michael Johnson

Research output: Contribution to journalConference paperpeer-review

10 Citations (Scopus)


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.
Original languageEnglish
Pages (from-to)1-16
Number of pages16
JournalProceedings of the First International Workshop on Bidirectional Transformations : BX 2012
Publication statusPublished - 2012
EventInternational Workshop on Bidirectional Transformations (1st : 2012) - Tallinn, Estonia
Duration: 25 Mar 201225 Mar 2012


Dive into the research topics of 'Relating algebraic and coalgebraic descriptions of lenses'. Together they form a unique fingerprint.

Cite this