Coalgebraic Update Lenses

Lenses are mathematical structures used in the context of bidirectional transformations.In this paper, we introduce update lenses as a refinement of ordinary (asymmetric) lenses in which we distinguish between views and updates. In addition to the set of views, there is a monoid of updates and an action of the monoid on the set of views. Decoupling updates from views allows for other ways of changing the source than just merging a view into the source. We also consider a yet finer dependently typed version of update lenses.We give a number of characterizations of update lenses in terms of bialgebras and coalgebras, including analogs to O'Connor's coalgebraic and Johnson, Rosebrugh and Wood's algebraic characterizations of ordinary lenses. We consider conversion of views and updates, a tensor product of update lenses and composition of update lenses.