We have identified a class of regular, whole-program transformations that cannot be safely performed with typical transformation techniques because transformation requires changing the types of terms. In these transformations, we want to change typically large parts of a program from using one type to using another type while simultaneously preserving the original program semantics after transformation.
In this paper, we present type-and-transform systems, an automated approach to the whole-program transformation of terms involving type A to terms involving the isomorphic type B using type-changing rewrite rules. Type-and-transform systems establish typing and semantics relations between all source and target subprograms such that a complete transformation can guarantee the equivalent semantics of a whole program. We describe the type-and-transform system for the lambda calculus with let-polymorphism and general recursion, including several examples from the literature and properties of the system.
Type-changing rewriting and semantics-preserving transformationPEPM '14 Proceedings of the ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation, 2014
