Introduction

In computer systems, copies of data are very often stored in different formats. Bidirectional transformations are programs that synchronise the data pairwise: when one is changed, the appropriate transformation is run to incorporate the changes in the other format. For bidirectional transformations to be considered correct, they are generally expected to satisfy “round-tripping”: if A is transformed to B, and then back, it shall give back the same A. This pattern of bidirectional transformations is much more widely applicable than just to data synchronization. They form a fundamental part of modern software engineering, where designs in the form of high-level models are (very often mechanically) transformed into lower-level implementations, and one often needs to reverse engineer a revised high-level model from an updated implementation. Since programming bidirectional transformations separately in opposite directions is error-prone and hard to maintain, there has been increasing interest in designated bidirectional programming languages that allow both transformations to be derived from a single definition, to guarantee round-tripping by construction, and to remove this duplication and the problems it causes.

In the EXHIBIT project, we will design a new generation of bidirectional languages that are easy to use. The central idea is that the new languages will be closely integrated with mainstream general-purpose languages, naturally reusing existing language constructs, libraries, and programming patterns to maximise the usability of the new framework. The work will be based on the project team’s recent theoretical breakthroughs that enable the interconversion between bidirectional objects and mainstream programming units, making a close connection between the two types of languages possible. As a teaser, in one of the languages we designed HOBiT, a bidirectional transformation is represented by an ordinary function on BX-typed values, which enables us to program bidirectional transformations in a more conventional functional programming style.

appendB :: BX [a] -> BX [a] -> BX [a] 
appendB z y = case* z of
   []  -> y               with (\_ -> True) reconciled by (\_ _ -> [])
   a:x -> a : appendB x y with not . null   reconciled by (\_ _ -> undefined)

The point is that appendB uses pattern matching and structural recursion in the same way as how the unidirectional append may be defined in a standard functional programming, which can be contrasted to most other bidirectional languages that are based on stylised combinators. This design is also beneficial for program synthesis. The resulting function may execute in both directions and is total in both directions. For example, with the function uncurryB defined as

uncurryB :: (BX a -> BX b -> BX c) -> BX (a, b) -> BX c 
uncurryB f x = let* (a,b) = x in f a b

appendB can be executed in the two directions as follows.

HOBiT> :get (uncurryB appendB) ([1,2,3], [4,5])
[1,2,3,4,5]
HOBiT> :put (uncurryB appendB) ([1,2,3], [4,5]) [10, 20, 30, 40, 50]
([10,20,30], [40,50])
HOBiT> :put (uncurryB appendB) ([1,2,3], [4,5]) [10, 20, 30, 40]
([10,20,30], [40])
HOBiT> :put (uncurryB appendB) ([1,2,3], [4,5]) [10, 20]
([10,20], [])
HOBiT> :put (uncurryB appendB) ([1,2,3], [4,5]) [10,20,30,40,50,60]
([10,20,30], [40,50,60])

In this project, we will develop and refine languages such as HOBiT, and start to develop realistic software which is only made possible by the superior programming utility offered by the language. We aim to make bidirectional programming and its benefits more accessible to mainstream programmers, which will ultimately result in higher productivity and quality in software development.