Monadic combinators for "Putback" style bidirectional programming
Monadic combinators for "Putback" style bidirectional programming
复制标题
DOI：
10.1145/2543728.2543737
复制
发表时间：
2014-01
期刊：
影响因子：
--
通讯作者：
Hugo Pacheco;Zhenjiang Hu;Sebastian Fischer
中科院分区：
文献类型：
--
作者：
Hugo Pacheco;Zhenjiang Hu;Sebastian Fischer
双向转换，特别是镜头，是具有前向GET转换和后向PUTBACK转换的程序，它们保持源数据类型和视图数据类型同步。有几种双向编程语言可以帮助程序员编写(某种)前向转换，并免费派生后向转换。然而，这种语言提供的可维护性是以表达能力和(更重要的)可预测性为代价的，因为同步的模糊性“通过回放转换处理”是通过默认策略解决的，程序员几乎无法控制这些策略。在本文中，我们认为控制这种歧义对于双向转换是必不可少的，并提出了一种新的语言，程序员可以用它编写一种(排序的)Putback变换，并免费获得唯一的GET变换。像传统的双向语言一样，我们的面向PUT的语言允许根据其构建块的属性来推理所定义的转换的正确性。但它允许程序员更准确地描述双向转换的行为，同时保留编写单个程序的可维护性。我们通过一系列的例子展示了新方法的实用能力，从简单的例子到复杂的例子，对于复杂的例子，我们的基于putback的方法是指定重要的更新策略的核心。
Bidirectional 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 programmers in writing a (sort of) forward transformation, and deriving a backward transformation for free. However, the maintainability offered by such languages comes at the cost of expressiveness and (more importantly) predictability because the ambiguity of synchronization "handled by the putback transformation" is solved by default strategies over which programmers have little control. In this paper, we argue that controlling such ambiguity is essential for bidirectional transformations and propose a novel language in which programmers write a (sort of) putback transformation, and get the unique get transformation for free. Like traditional bidirectional languages, our put-oriented language allows reasoning about the correctness of defined transformations from the properties of their building blocks. But it allows programmers to describe the behavior of a bidirectional transformation much more precisely, while retaining the maintainability of writing a single program. We demonstrate the practical power of the new approach through a series of examples, ranging from simple ones that illustrate traditional lenses to complex ones for which our putback-based approach is central to specifying nontrivial update strategies.