Martin Hofmann, Edit Lenses
Edit Lenses (Martin Hofmann)
A lens is a bidirectional transformation between a pair of
connected data structures, capable of translating an edit on one
structure into an appropriate edit on the other. Many varieties of
lenses have been studied, but none, to date, has offered a satisfactory
treatment of how edits are represented. Many foundational accounts only
consider edits of the form "overwrite the whole structure," leading to
poor behavior in many situations by failing to track the associa- tions
between corresponding parts of the structures when elements are inserted
and deleted in ordered lists, for example. Other theo- ries of lenses do
maintain these associations, either by annotating the structures
themselves with change information or with auxiliary data structures,
but every extant theory assumes that the entire original source
structure is part of the information passed to the lens--a rather
special (and perhaps inefficient) choice. We offer here a general theory
of edit lenses, which work with descriptions of changes to structures,
rather than with the structures themselves. We identify a simple notion
of "editable structure"-- a set of states plus a monoid of edits with a
partial action on the states--and construct a semantic space of lenses
between such structures, with natural laws governing their behavior. We
show how a range of constructions from earlier papers on "state-based"
lenses--composition, products, sums, lists operations, etc.--can be
carried out in this space. Further, we show how to construct edit lenses
for arbitrary containers in the sense of Abbott, Altenkirch, and Ghani.
Finally, we show that edit lenses refine a well-known formulation of
state-based lenses, in the sense that every state- based lens gives rise
to an edit lens over structures with a simple overwrite-only edit
language, and conversely every edit lens on such structures gives rise
to a state-based lens.
This is joint work with Benjamin Pierce and Daniel Wagner.
Artikelaktionen