Three Complementary Approaches to Bidirectional Programming

J. Nathan Foster, Kazutaka Matsuda, Janis Voigtländer. Three Complementary Approaches to Bidirectional Programming. In Jeremy Gibbons, editor, Generic and Indexed Programming - International Spring School, SSGIP 2010, Oxford, UK, March 22-26, 2010, Revised Lectures. Volume 7470 of Lecture Notes in Computer Science, pages 1-46, Springer, 2010. [doi]

Abstract

This paper surveys three distinct approaches to bidirectional programming. The first approach, syntactic bidirectionalization, takes a program describing the forward transformation as input and calculates a well-behaved reverse transformation. The second approach, semantic bidirectionalization, is similar, but takes the forward transformation itself as input rather than a program describing it. It requires the transformation to be a polymorphic function and uses parametricity and free theorems in the proof of well-behavedness. The third approach, based on bidirectional combinators, focuses on the use of types to ensure well-behavedness and special constructs for dealing with alignment problems. In presenting these approaches, we pay particular attention to use of complements, which are structures that represent the information discarded by the transformation in the forward direction.