Second Workshop on Haskell And Rewriting Techniques (HART 2014)

The following contributions were selected (out of 15 submissions) for presentation at the workshop:

- Anthony Anjorin, Gergely Varro and Andy Schürr.
**Complex Attribute Manipulation in TGGs with Constraint-Based Programming Techniques.**

**Abstract:**Model transformation plays a central role in Model-Driven Engineering (MDE) and providing bidirectional transformation languages is a current challenge with important applications. Triple Graph Grammars (TGGs) are a formally founded, bidirectional model transformation language shown by numerous case studies to be quite promising and successful. Although TGGs provide adequate support for structural aspects via object patterns in production rules, support for handling complex relationships between different attributes is still missing in current implementations. For certain applications, such as bidirectional model-to-text transformations, being able to manipulate attributes via string manipulation or arithmetic operations in TGG production rules is vital. Our contribution in this paper is a novel TGG extension that provides a means for complex attribute manipulation in TGG production rules. Our extension is compatible with the existing TGG formalization, and retains the "single specification" philosophy of TGGs.

- Jeremy Gibbons and Michael Johnson.
**Relating Algebraic and Coalgebraic Descriptions of Lenses.**

**Abstract:**Lenses are a heavily studied form of bidirectional transformation, with diverse applications including database view updating, software development and memory management. Previous work has explored lenses category-theoretically, and established that lenses are isomorphic to algebras for a particular monad on a slice category. It has recently been shown that lenses are the coalgebras for the comonad generated by cartesian closure. We present an equational proof of the coalgebra correspondence, note that the algebra correspondence extends to arbitrary categories with products and that the coalgebra correspondence extends to arbitrary cartesian closed categories, and show that both correspondences extend to isomorphisms of categories. The resulting isomorphism between a category of algebras and a category of coalgebras is unexpected, and we analyze it, isolating its underlying generality, and also the particularity that restricts its applicability.

- Hugo Pacheco, Alcino Cunha and Zhenjiang Hu.
**Delta Lenses over Inductive Types.**

**Abstract:**Existing bidirectional languages are either state-based or operation-based, depending on wether they represent updates as mere states or as sequences of edit operations. In-between both worlds are delta-based frameworks, where updates are represented using alignment relationships between states. In this paper, we formalize delta lenses over inductive types using dependent type theory and develop a point-free delta lens language with an explicit separation of shape and data. In contrast with the already known issue of data alignment, we identify the new problem of shape alignment and solve it by lifting standard recursion patterns such as folds and unfolds to delta lenses that use alignment to infer meaningful shape updates.

- Vadim Zaytsev.
**Language Evolution, Metasyntactically.**

**Abstract:**We use a formal specification for syntactic notations in order to simulate a scenario of notational evolution: a special language evolution case when the language itself is preserved, but the notation which is used to write down its grammar in the documentation, changes, and those changes need to be propagated to coupled grammar refactorings, grammarbase mutations and other connected artefacts. Both the megamodel and the prototypical implementation of this scenario are explained. They employ bidirectional grammar transformation for the purposes of adaptation and convergence, transformable notation specifications and coupled unidirectional grammar mutations.

- Michael Johnson and Robert Rosebrugh.
**Lens put-put laws: Monotonic and mixed.**

**Abstract:**Since the introduction of very well behaved lenses, several authors have argued, for good reasons, that in many applications the put-put law is too strong. On the other hand, the present authors have shown that such lenses, including the put-put law, are algebras for a certain monad, and that this viewpoint admits fruitful generalisations of the lens concept to a variety of base categories. In the algebra approach to lenses, the put-put law corresponds to the associativity axiom, and so is fundamentally important. Thus we have a dilemma. The put-put law seems inappropriate for a variety of applications, but is fundamental to the mathematical development that can support a range of applications. In this paper we resolve this dilemma. The put-put law as normally stated is indeed too strong when the category of models is non-trivial (not just a set of models). We describe monotonic put-put laws -- those in which successive puts are, loosely speaking, both along deletes, or both along inserts, and note that such laws do not suffer the criticisms of the classical put-put law and incidentally provide a counterexample to the mistaken belief that the presence of put-put laws implies constant complement updating. Of course, of much greater interest than monotonic put-put laws are mixed put-put laws that treat together both inserts and deletes. The main contribution of this paper is the development and analysis of a new mixed put-put law which is very general, is indeed weaker than classical put-put, does not seem to be subject to the criticisms of the classical put-put law, and is sufficient to support the monad based mathematical treatment of generalised lenses.

- Leen Lambers, Stephan Hildebrandt, Holger Giese and Fernando Orejas.
**Attribute Handling for Bidirectional Model Transformations: The Triple Graph Grammar Case.**

**Abstract:**When describing bidirectional model transformations in a declarative (relational) way, the relation between structures in source and target models is specified. But not only structural correspondences between source and target models need to be described. Another important aspect is the specification of the relation between attribute values of elements in source and target models. However, existing approaches either do not allow such a relational kind of specification for attributes or allow it only in a restricted way. We consider the challenge of bridging the gap between a flexible declarative attribute specification and its operationalization for the triple graph grammar (TGG) specification technique as an important representative for describing bidirectional model transformations in a relational way. First, we present a formal way to specify attributes in TGG rules in a purely declarative (relational) way. Then, we give an overview of characteristic barriers that bidirectional model transformation tool developers are confronted with when operationalizing relational attribute constraints for different TGG application scenarios. Moreover, we present pragmatic solutions to overcome the operationalization barriers for different TGG application scenarios in our own TGG implementation.

- Erwann Wernli.
**Bidirectional transformations meets dynamic updates: promise & perils.**

**Abstract:**Dynamic updates that transform objects in an unidirectional manner face timing issues that might lead to run-time type errors. A way to avoid such run-time type errors is to keep both versions of objects and synchronize them with bidirectional transformations. Keeping objects synchronized this way raises some challenges in term of performance, thread safety, and practicality. We present implementation strategies and explore the solution space of such an approach. We put theoretical issues into perspective by considering results of existing empirical research in the field, and investigate the use of a simple bidirectional language to express object transformations. We conclude that this scheme can be made practical, and we sketch future research directions to reach this goal.

- Perdita Stevens.
**Observations relating to the equivalences induced on model sets by bidirectional transformations.**

**Abstract:**A bidirectional transformation on a pair of sets of models induces two principal equivalence relations on each set of models. Since a model can be uniquely identified by specifying its equivalence class in each of these relations, they function as a coordinate system for the model sets, with respect to the transformation. We give a collection of results relating to this observation and explore the consequences for the study of the transformation.