Formalizing Semantic Bidirectionalization with Dependent Types

Helmut Grohne, Andres Löh, Janis Voigtländer

Bidirectionalization is the task of automatically inferring one of two transformations that as a pair realize the forward and backward relationship between two domains, subject to certain consistency conditions. A specific technique, semantic bidirectionalization, has been developed that takes a get-function (mapping forwards from sources to views) as input — but does not inspect its syntactic definition — and constructs a put-function (mapping an original source and an updated view back to an updated source), guaranteeing standard well-behavedness conditions. Proofs of the latter have been done by hand in the original paper, and recently published extensions of the technique have also come with more or less rigorous proofs or sketches thereof.

In this paper we report on a formalization of the original technique in a dependently typed programming language (turned proof assistant). This yields a complete correctness proof, with no details left out. Besides demonstrating the viability of such a completely formal approach to bidirectionalization, we see further benefits:

1. Exploration of variations of the original technique could use our formalization as a base line, providing assurance about preservation of the well-behavedness properties as one makes adjustments.
2. Thanks to being presented in a very expressive type theory, the formalization itself already provides more information about the base technique than the original work. Specifically, while the original by-hand proofs established only a partial correctness result, useful preconditions for total correctness come out of the mechanized formalization.
3. Finally, also thanks to the very precise types, there is potential for generally improving the bidirectionalization technique itself. Particularly, shape-changing updates are known to be problematic for semantic bidirectionalization, but a refined technique could leverage the information about the relationship between the shapes of sources and views now being expressed at the type level, in a way we sketch and plan to explore further.

Download

Paper, accepted at BX 2014

Andres Löh, 2014-01-09