Automating Changes of Data Type in Functional Programs

Abstract

I present an automatic technique for transforming a program by changing the data types in that program to ones which are more appropriate for the task. Programs are synthesised by proving modified synthesis theorems in the proofs-as-programs paradigm. The transformation can be verified in the logic of type theory. Transformations are motivated by the presence of subexpressions in the synthesised program. A library of data type changes is maintained, indexed by the motivating subexpressions. These transformations are extended from the motivating expressions to cover as much of the program as possible. I describe the general pattern of the revised synthesis proof, and show how such a proof can be guided by difference matching followed by rippling.