More Web Proxy on the site http://driver.im/

Article

Type-safe two-level data transformation

Authors:

José Nuno Oliveira,

Joost VisserAuthors Info & Claims

FM'06: Proceedings of the 14th international conference on Formal Methods

Pages 284 - 299

https://doi.org/10.1007/11813040_20

Published: 21 August 2006 Publication History

Abstract

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 used for interoperability and persistence.

We provide a formal treatment of two-level data transformations that is type-safe in the sense that the well-formedness of the value-level transformations with respect to the type-level transformation is guarded by a strong type system. We rely on various techniques for generic functional programming to implement the formalization in Haskell.

The formalization addresses various two-level transformation scenarios, covering fully automated as well as user-driven transformations, and allowing transformations that are information-preserving or not. In each case, two-level transformations are disciplined by one-step transformation rules and type-level transformations induce value-level transformations. We demonstrate an example hierarchical-relational mapping and subsequent migration of relational data induced by hierarchical format evolution.

References

[1]

T.L. Alves, P.F. Silva, J. Visser, and J.N. Oliveira. Strategic term rewriting and its application to a VDM-SL to SQL conversion. In J. Fitzgerald, IJ. Hayes, and A. Tarlecki, editors, Proc. Int. Symposium of Formal Methods Europe, volume 3582 of LNCS, pages 399-414. Springer, 2005.

[2]

F. Atanassow and J. Jeuring. Inferring type isomorphisms generically. In D. Kozen, editor, Proc. 7th Int. Conference on Mathematics of Program Construction, volume 3125 of LNCS, pages 32-53. Springer, 2004.

[3]

M.v.d Brand, P. Klint, and J. Vinju. Term rewriting with type-safe traversal functions. ENTCS, 70(6), 2002.

[4]

A. Cleve, J. Henrard, and J.-L. Hainaut. Co-transformations in information system reengineering. ENTCS, 137(3):5-15, 2005.

[5]

A. Cunha, J.N. Oliveira, and J. Visser. Type-safe two-level data transformation - with derecursivation and dynamic typing. Technical Report DI-PURe-06.03.01, Univ. Minho, 2006.

[6]

J.N. Foster et al. Combinators for bi-directional tree transformations: a linguistic approach to the view update problem. In Proc. 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 233-246. ACM Press, 2005.

[7]

R. Hinze. Fun with phantom types. In J. Gibbons and O. de Moor, editors, The Fun of Programming, pages 245-262. Palgrave, 2003.

[8]

R. Hinze, A. Löh, and B. Oliveira. "Scrap your boilerplate" reloaded. In Proc. 8th Int. Symposium on Functional and Logic Programming, volume 3945 of LNCS, pages 13-29. Springer, 2006.

[9]

G. Hutton and E. Meijer. Back to Basics: Deriving Representation Changers Functionally. Journal of Functional Programming, 6(1):181-188, January 1996.

[10]

R. Lämmel. Coupled Software Transformations (Extended Abstract). In First International Workshop on Software Evolution Transformations, November 2004.

[11]

R. Lämmel. Transformations everywhere. Sci. Comput. Program., 52:1-8, 2004. Guest editor's introduction to special issue on program transformation.

[12]

R. Lämmel and W. Lohmann. Format Evolution. In Proc. 7th Int. Conf. on Reverse Engineering for Information Systems, volume 155 of [email protected], pages 113-134. OCG, 2001.

[13]

R. Lämmel and E. Meijer. Mappings make data processing go 'round. In R. Lämmel, J. Saraiva, and J. Visser, editors, Proc. Int. Summer School on Generative and Transformational Techniques in Software Engineering, Braga, Portugal, July 4-8, 2005, LNCS. Springer, 2006. To appear.

[14]

R. Lämmel and S. Peyton Jones. Scrap your boilerplate: a practical design pattern for generic programming. In Proc. ACM SIGPLAN Workshop on Types in Language Design and Implementation, pages 26-37. ACM Press, March 2003.

[15]

R. Lämmel and J. Visser. Strategic polymorphism requires just two combinators! Technical Report cs.PL/0212048, arXiv, December 2002. An early version was published in the informal preproceedings IFL 2002.

[16]

R. Lämmel and J. Visser. Typed combinators for generic traversal. In Proc. Practical Aspects of Declarative Programming, volume 2257 of LNCS, pages 137-154. Springer, January 2002.

[17]

C. Morgan and P.H. B. Gardiner. Data refinement by calculation. Acta Informatica, 27:481-503, 1990.

[18]

F.L. Neves, J.C. Silva, and J.N. Oliveira. Converting Informal Meta-data to VDM-SL: A Reverse Calculation Approach. In VDM in Practice! A Workshop co-located with FM'99: The World Congress on Formal Methods, Toulouse, France, September 1999.

[19]

J.N. Oliveira. A reification calculus for model-oriented software specification. Formal Aspects of Computing, 2(1):1-23, April 1990.

[20]

J.N. Oliveira. Software reification using the SETS calculus. In T. Denvir, C.B. Jones, and R.C. Shaw, editors, Proc. of the BCS FACS 5th Refinement Workshop, Theory and Practice of Formal Software Development, pages 140-171. Springer, 1992.

[21]

J.N. Oliveira. Calculate databases with 'simplicity', September 2004. Presentation at the IFIPWG 2.1 #59 Meeting, Nottingham, UK.

[22]

S. Peyton Jones, G. Washburn, and S. Weirich. Wobbly types: type inference for generalised algebraic data types. Technical Report MS-CIS-05-26, Univ. of Pennsylvania, July 2004.

[23]

P. Wadler. The essence of functional programming. In Proc. 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 1-14. ACM Press, 1992.

Cited By

Pacheco HCunha A(2012)MultifocalProceedings of the 5th international conference on Theory and Practice of Model Transformations10.1007/978-3-642-30476-7_6(89-104)Online publication date: 28-May-2012
https://dl.acm.org/doi/10.1007/978-3-642-30476-7_6
Cunha JVisser JAlves TSaraiva J(2011)Type-safe evolution of spreadsheetsProceedings of the 14th international conference on Fundamental approaches to software engineering: part of the joint European conferences on theory and practice of software10.5555/1987434.1987453(186-201)Online publication date: 26-Mar-2011
https://dl.acm.org/doi/10.5555/1987434.1987453
Vermolen SWachsmuth GVisser E(2011)Generating database migrations for evolving web applicationsACM SIGPLAN Notices10.1145/2189751.204787647:3(83-92)Online publication date: 22-Oct-2011
https://dl.acm.org/doi/10.1145/2189751.2047876
Show More Cited By

Recommendations

Coupled Transformation of Schemas, Documents, Queries, and Constraints

Coupled transformation occurs when multiple software artifacts must be transformed in such a way that they remain consistent with each other. For instance, when a database schema is adapted in the context of system maintenance, the persistent data ...
Strongly Typed Rewriting For Coupled Software Transformation

Coupled transformations occur in software evolution when multiple artifacts must be modified in such a way that they remain consistent with each other. An important example involves the coupled transformation of a data type, its instances, and the ...
Point-free Program Transformation
Program Transformation: Theoretical Foundations and Basic Techniques. Part 1

Functional programs are particularly well suited to formal manipulation by equational reasoning. In particular, it is straightforward to use calculational methods for program transformation. Well-known transformation techniques, like tupling or the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

FM'06: Proceedings of the 14th international conference on Formal Methods

August 2006

619 pages

ISBN:3540372156

Editors:
Jayadev Misra
The University of Texas at Austin
,
Tobias Nipkow
Institut für Informatik, Technische Universität, München
,
Emil Sekerinski
Department of Computing and Software, McMaster University, 1280 Main Street West, Hamilton, Ontario, Canada

Sponsors

MFE: MFE
McMaster Univ.: McMaster University
FORTIA: FORTIA
Micro Research: Micro Research
SQRL: SQRL

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 21 August 2006

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

16
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 11 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Pacheco HCunha A(2012)MultifocalProceedings of the 5th international conference on Theory and Practice of Model Transformations10.1007/978-3-642-30476-7_6(89-104)Online publication date: 28-May-2012
https://dl.acm.org/doi/10.1007/978-3-642-30476-7_6
Cunha JVisser JAlves TSaraiva J(2011)Type-safe evolution of spreadsheetsProceedings of the 14th international conference on Fundamental approaches to software engineering: part of the joint European conferences on theory and practice of software10.5555/1987434.1987453(186-201)Online publication date: 26-Mar-2011
https://dl.acm.org/doi/10.5555/1987434.1987453
Vermolen SWachsmuth GVisser E(2011)Generating database migrations for evolving web applicationsACM SIGPLAN Notices10.1145/2189751.204787647:3(83-92)Online publication date: 22-Oct-2011
https://dl.acm.org/doi/10.1145/2189751.2047876
Vermolen SWachsmuth GVisser EDenney ESchultz U(2011)Generating database migrations for evolving web applicationsProceedings of the 10th ACM international conference on Generative programming and component engineering10.1145/2047862.2047876(83-92)Online publication date: 22-Oct-2011
https://dl.acm.org/doi/10.1145/2047862.2047876
Pacheco HCunha AKhoo SSiek J(2011)Calculating with lensesProceedings of the 20th ACM SIGPLAN workshop on Partial evaluation and program manipulation10.1145/1929501.1929520(91-100)Online publication date: 24-Jan-2011
https://dl.acm.org/doi/10.1145/1929501.1929520
Cunha APacheco H(2011)Algebraic Specialization of Generic Functions for Recursive TypesElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2011.02.016229:5(57-74)Online publication date: 1-Mar-2011
https://dl.acm.org/doi/10.1016/j.entcs.2011.02.016
Pacheco HCunha A(2010)Generic point-free lensesProceedings of the 10th international conference on Mathematics of program construction10.5555/1886619.1886640(331-352)Online publication date: 21-Jun-2010
https://dl.acm.org/doi/10.5555/1886619.1886640
Cunha JSaraiva JVisser JPuebla GVidal G(2009)From spreadsheets to relational databases and backProceedings of the 2009 ACM SIGPLAN workshop on Partial evaluation and program manipulation10.1145/1480945.1480972(179-188)Online publication date: 19-Jan-2009
https://dl.acm.org/doi/10.1145/1480945.1480972
Foster JPilkiewicz APierce BHook JThiemann P(2008)Quotient lensesProceedings of the 13th ACM SIGPLAN international conference on Functional programming10.1145/1411204.1411257(383-396)Online publication date: 20-Sep-2008
https://dl.acm.org/doi/10.1145/1411204.1411257
Foster JPilkiewicz APierce B(2008)Quotient lensesACM SIGPLAN Notices10.1145/1411203.141125743:9(383-396)Online publication date: 20-Sep-2008
https://dl.acm.org/doi/10.1145/1411203.1411257
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents