NOTE: the 2LT project is moving to: 2LT at Google Code.
A two-level data transformation consists of a type-level transformation of a data format coupled with value-level transformations of data instances corresponding to that format. Examples of two-level data transformations include XML schema evolution coupled with document migration, and data mappings that couple a data format mapping with conversions between mapped formats.
In the 2LT project we apply theories of calculational data refinement and of point-free program transformation to two-level transformations.
DATA REFINEMENT
A refinement of an abstract type A into a concrete type B, is witnessed by conversion functions to:A->B (injective and total) and from:B->A (surjective and partial).
TYPE-CHANGING REWRITES
Such data refinements can be modeled by a type-changing rewrite system, where each rewite step takes the form A => (B,to,from). In other words, each step produces not only a new type, but also the conversion functions between the old and new type. By repeatedly applying such rewrite steps, complex conversion functions are calculated incrementally while a new type is being derived.
PROGRAM CALCULATION
The complex conversion functions derived after type-changing rewriting can be subjected to subsequent simplification using laws of point-free program calculation. The same holds for compositions of conversion functions with queries on the target or source data types. Such simplifications then amount for instance to:
generation of efficient low-level data migrations from high-level migrations
program migration of queries on the source data type to queries on a target data type
Apart from transformation of point-free functions, we have implemented rewrite systems for transformation of structure-shy functions (XPath expressions and strategic functions), and for transformation of binary relation expressions.
HASKELL IMPLEMENTATION
We have implemented both type-changing rewrite systems and type-preserving rewrite systems in Haskell. The implementations involve generalized algebraic datatypes (GADTs), strategy combinators, type-safe representations of types and of functions, and other advanced Haskell techniques.
Alcino Cunha, Joost Visser. Strongly Typed Rewriting For Coupled Software Transformation. In Proceedings of RULE 2006, ENTCS, to appear. (PDF).
Pablo Berdaguer, Alcino Cunha, Hugo Pacheco, Joost Visser. Coupled Schema Transformation and Data Conversion For XML and SQL. In PADL 2007: Practical Aspects of Declarative Languages, to appear. (PDF).
Alcino Cunha and Joost Visser, Transformation of Structure-Shy Programs, Applied to XPath Queries and Strategic Functions, In Proceedings of the 2007 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2007, to appear. (PDF)
Claudia Mónica Necco, José Nuno Oliveira, and Joost Visser, Extended Static Checking By Strategic Rewriting of Pointfree Relational Expressions, Draft of februari 3, 2007. (PDF)
TECHNICAL REPORT
Alcino Cunha, José Nuno Oliveira, Joost Visser. Type-safe Two-level Data Transformations -- with derecursivation and dynamic typing, DI-Research.PURe-06.03.01, March 2006. (PDF).
