Martin Hofmann, Benjamin C Pierce, and Daniel Wagner (2011)

# Symmetric lenses

In: POPL, pp. 371-384.

Lenses - bidirectional transformations between pairs of connected$~$structures - have been extensively studied and are beginning to ﬁnd$~$their way into industrial practice. However, some aspects of their$~$foundations remain poorly understood. In particular, most previous$~$work has focused on the special case of asymmetric lenses, where$~$one of the structures is taken as primary and the other is thought of$~$as a projection, or view. A few studies have considered symmetric$~$variants, where each structure contains information not present in$~$the other, but these all lack the basic operation of composition.$~$Moreover, while many domain-speciﬁc languages based on lenses$~$have been designed, lenses have not been thoroughly explored from$~$an algebraic perspective. We offer two contributions to the theory of lenses. First, we$~$present a new symmetric formulation, based on complements, an$~$old idea from the database literature. This formulation generalizes$~$the familiar structure of asymmetric lenses, and it admits a good$~$notion of composition. Second, we explore the algebraic structure$~$of the space of symmetric lenses. We present generalizations of a$~$number of known constructions on asymmetric lenses and settle$~$some longstanding questions about their properties - in particular,$~$we prove the existence of (symmetric monoidal) tensor products$~$and sums and the non-existence of full categorical products or sums$~$in the category of symmetric lenses. We then show how the methods of universal algebra can be applied to build iterator lenses for$~$structured data such as lists and trees, yielding lenses for operations$~$like mapping, ﬁltering, and concatenation from ﬁrst principles. Finally, we investigate an even more general technique for constructing mapping combinators, based on the theory of containers.

Document Actions