Summary: Bidirectional programming is concerned with pairs of transformations that together realize the forward and backward relationship between two data domains. Semantic bidirectionalization is a specific technique that takes a get-function (mapping forward from sources to views) as input and automatically gives a put-function (mapping an original source and an updated view back to an updated source), while guaranteeing standard well-behavedness properties. Proofs of those properties have been done by hand originally, and later extensions of the technique have also come with by-hand proofs or sketches thereof.
Here we provide a formalization of semantic bidirectionalization and proof of those properties in the dependently typed programming language Agda. We then explore two previously considered variations of the original technique, using our initial formalization as a baseline and showing that the well-behavedness properties are preserved as adjustments are made. Also, we find that using very precise types pays off, as a means to express insight about the bidirectionalization technique and by even allowing us to further improve it. In particular, shape-changing updates are known to be problematic for semantic bidirectionalization, and one of the variations considered addresses this by using “shape bidirectionalizers”. In the past, these have been thought of as extra components, but by leveraging information about the relationship between the shapes of sources and views now being expressed at the type level, we show that these “plug-ins” can sometimes be replaced by just type inference.
Beside the results about bidirectionalization, the article may also serve as an introduction and concrete example of using Agda to formalize and verify applications of functional programming.