Quotient lenses

There are now a number of bidirectional programming languages, where every program can be read both as a forward transformation mapping one data structure to another and as a reverse transformation mapping an edited output back to a correspondingly edited input. Besides parsimony--the two related transformations are described by just one expression--such languages are attractive because they promise strong behavioral laws about how the two transformations fit together--e.g., their composition is the identity function. It has repeatedly been observed, however, that such laws are actually a bit too strong: in practice, we do not want them "on the nose," but only up to some equivalence, allowing inessential details, such as whitespace, to be modified after a round trip. Some bidirectional languages loosen their laws in this way, but only for specific, baked-in equivalences. In this work, we propose a general theory of quotient lenses-bidirectional transformations that are well ...

• Type: Conference
• Year: 2008
• Where: ICFP
• Authors: J. Nathan Foster, Alexandre Pilkiewicz, Benjamin C. Pierce
• Keywords: Bidirectional Programming Languages, ICFP 2008, Programming Languages, Quotient Lenses, Quotient Lenses-bidirectional Transformations