Bidirectionalization for Free!
The paper is available via the ACM DL Author-ize feature:
| Author: | J. Voigtländer |
|---|---|
| Published: | In 36th Symposium on Principles of Programming Languages (POPL'09, acceptance rate 36/160), Savannah, Georgia, Proceedings, volume 44(1) of SIGPLAN Notices, pages 165-176, ACM, January 2009. |
| DOI: | 10.1145/1480881.1480904 |
| BibTeX: | Voi09a.bib |
| Abstract: | A bidirectional transformation consists of a function get that takes a source (document or value) to a view and a function put that takes an updated view and the original source back to an updated source, governed by certain consistency conditions relating the two functions. Both the database and programming language communities have studied techniques that essentially allow a user to specify only one of get and put and have the other inferred automatically. All approaches so far to this bidirectionalization task have been syntactic in nature, either proposing a domain-specific language with limited expressiveness but built-in (and composable) backward components, or restricting get to a simple syntactic form from which some algorithm can synthesize an appropriate definition for put. Here we present a semantic approach instead. The idea is to take a general-purpose language, Haskell, and write a higher-order function that takes (polymorphic) get-functions as arguments and returns appropriate put-functions. All this on the level of semantic values, without being willing, or even able, to inspect the definition of get, and thus liberated from syntactic restraints. Our solution is inspired by relational parametricity and uses free theorems for proving the consistency conditions. It works beautifully. |
| Download: | http://dl.acm.org/authorize?160397 (free) |
| Slides: | Slides of my talk at the conference are here. |
A web interface to the library developed in this paper is now accessible here. (The links mentioned in the paper itself are outdated.)