Hsiang-Shang Ko
Tao Zan
ABSTRACT
Putback-based bidirectional programming allows the programmer to write only one putback transformation, from which the unique corresponding forward transformation is derived for free. The logic of a putback transformation is more sophisticated than that of a forward transformation and does not always give rise to well-behaved bidirectional programs; this calls for more robust language design to support development of well-behaved putback transformations. In this paper, we design and implement a concise core language BiGUL for putback-based bidirectional programming to serve as a foundation for higher-level putback-based languages. BiGUL is completely formally verified in the dependently typed programming language Agda to guarantee that any putback transformation written in BiGUL is well-behaved.
Supplemental Material
Available for Download
Agda source code, typechecked with Agda version 2.4.2.4 and standard library version 0.11, and a browsable html version.
- T. Altenkirch and C. McBride. Generic programming within dependently typed programming. In IFIP TC2/WG2.1 Working Conference on Generic Programming, pages 1–20. Kluwer, B.V., 2003. Google Scholar
Digital Library
- D. M. J. Barbosa, J. Cretin, J. N. Foster, M. Greenberg, and B. C. Pierce. Matching lenses: alignment and view update. In International Conference on Functional Programming, pages 193–204. ACM, 2010. Google ScholarDigital Library
- A. Bohannon, B. C. Pierce, and J. A. Vaughan. Relational lenses: a language for updatable views. In Principles of Database Systems, pages 338–347. ACM, 2006. Google ScholarDigital Library
- J. Cheney. F LUX : functional updates for XML. In International Conference on Functional Programming, pages 3–14. ACM, 2008. Google ScholarDigital Library
- K. Czarnecki, J. N. Foster, Z. Hu, R. Lämmel, A. Schürr, and J. Terwilliger. Bidirectional transformations: a cross-discipline perspective. In International Conference on Model Transformation, volume 5563 of Lecture Notes in Computer Science, pages 260–283. Springer-Verlag, 2009. Google ScholarDigital Library
- N. A. Danielsson, J. Gibbons, J. Hughes, and P. Jansson. Fast and loose reasoning is morally correct. In Principles of Programming Languages, pages 206–217. ACM, 2006. Google ScholarDigital Library
- J. N. Foster. Bidirectional Programming Languages. PhD thesis, University of Pennsylvania, 2009. Google ScholarDigital Library
- J. N. Foster, M. B. Greenwald, J. T. Moore, B. C. Pierce, and A. Schmitt. Combinators for bidirectional tree transformations: a linguistic approach to the view-update problem. ACM Transactions on Programming Languages and Systems, 29(3):17, 2007. Google ScholarDigital Library
- J. N. Foster, A. Pilkiewicz, and B. C. Pierce. Quotient lenses. In International Conference on Functional Programming, pages 383–396. ACM, 2008. Google ScholarDigital Library
- J. Gibbons. Datatype-generic programming. In Spring School on Datatype-Generic Programming, volume 4719 of Lecture Notes in Computer Science, pages 1–71. Springer-Verlag, 2007. Google ScholarDigital Library
- J. Gibbons. Functional programming for domain-specific languages. In Central European Functional Programming School, volume 8606 of Lecture Notes in Computer Science, pages 1–28. Springer-Verlag, 2015.Google Scholar
- H. Grohne, A. Löh, and J. Voigtländer. Formalizing semantic bidirectionalization with dependent types. In International Workshop on Bidirectional Transformations, pages 75–81. CEUR-WS, 2014.Google Scholar
- S. Hidaka, Z. Hu, K. Inaba, H. Kato, K. Matsuda, and K. Nakano. Bidirectionalizing graph transformations. In International Conference on Functional Programming, pages 205–216. ACM, 2010. Google ScholarDigital Library
- M. Hofmann, B. C. Pierce, and D. Wagner. Symmetric lenses. In Principles of Programming Languages, pages 371–384. ACM, 2011. Google ScholarDigital Library
- M. Hofmann, B. C. Pierce, and D. Wagner. Edit lenses. In Principles of Programming Languages, pages 495–508. ACM, 2012. Google ScholarDigital Library
- Z. Hu, H. Pacheco, and S. Fischer. Validity checking of putback transformations in bidirectional programming. In International Symposium on Formal Methods, volume 8442, pages 1–15. Springer-Verlag, 2014.Google Scholar
- S. Lindley and C. McBride. Hasochism: the pleasure and pain of dependently typed Haskell programming. In Haskell Symposium, pages 81–92. ACM, 2013. Google ScholarDigital Library
- K. Matsuda, Z. Hu, K. Nakano, M. Hamana, and M. Takeichi. Bidirectionalization transformation based on automatic derivation of view complement functions. In International Conference on Functional Programming, pages 47–58. ACM, 2007. Google ScholarDigital Library
- E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92, 1991. Google ScholarDigital Library
- U. Norell. Towards a Practical Programming Language based on Dependent Type Theory. PhD thesis, Chalmers University of Technology, 2007.Google Scholar
- U. Norell. Dependently typed programming in Agda. In Advanced Functional Programming, volume 5832 of Lecture Notes in Computer Science, pages 230–266. Springer-Verlag, 2009. Google ScholarDigital Library
- U. Norell. Interactive programming with dependent types. In International Conference on Functional Programming, pages 1–2. ACM, 2013. Google ScholarDigital Library
- H. Pacheco and A. Cunha. Generic point-free lenses. In Mathematics of Program Construction, volume 6120 of Lecture Notes in Computer Science, pages 331–352. Springer-Verlag, 2010. Google ScholarDigital Library
- H. Pacheco, Z. Hu, and S. Fischer. Monadic combinators for “putback” style bidirectional programming. In Partial Evaluation and Program Manipulation, pages 39–50. ACM, 2014. Google ScholarDigital Library
- H. Pacheco, T. Zan, and Z. Hu. BiFluX: a bidirectional functional update language for XML. In Principles and Practice of Declarative Programming, pages 147–158. ACM, 2014. Google ScholarDigital Library
- J. Voigtländer. Bidirectionalization for free! In Principles of Programming Languages, pages 165–176. ACM, 2009. Google ScholarDigital Library
- P. Wadler. The essence of functional programming. In Principles of Programming Languages, pages 1–14. ACM, 1992. Google ScholarDigital Library
- Z. Zhu, H.-S. Ko, P. Martins, J. Saraiva, and Z. Hu. BiYacc: roll your parser and reflective printer into one. In International Workshop on Bidirectional Transformations, pages 43–50. CEUR-WS, 2015.Google Scholar
Index Terms
- BiGUL: a formally verified core language for putback-based bidirectional programming
Recommendations
Putback-based bidirectional model transformations
ESEC/FSE 2018: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software EngineeringBidirectional model transformation (BX) plays a vital role in Model-Driven Engineering. A major challenge in conventional relational and bidirectionalization-based BX approaches is the ambiguity issue, i.e., the backward transformation may not be ...
Monadic combinators for "Putback" style bidirectional programming
PEPM '14: Proceedings of the ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program ManipulationBidirectional transformations, in particular lenses, are programs with a forward get transformation and a backward putback transformation that keep source and view data types synchronized. Several bidirectional programming languages exist to aid ...
Validity Checking of Putback Transformations in Bidirectional Programming
Proceedings of the 19th International Symposium on FM 2014: Formal Methods - Volume 8442A bidirectional transformation consists of pairs of transformations --a forward transformation get produces a target view from a source, while a putback transformation put puts back modifications on the view to the source-- satisfying sensible roundtrip ...
Comments