Quotient lenses

Abstract

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.