Have you seen the paper "Editing Functional Programs Without Breaking Them" by Amsden et al. [1]? It does something similar. It allows you to transform any prog

Have you seen the paper "Editing Functional Programs Without Breaking Them" by Amsden et al. [1]? It does something similar. It allows you to transform any program (in an idealised typed programming languages) into any other using a small collection of transformation operations. The highlight is that this is possible without compormising typability. This is also related to patch theory [2, 3, 4, 5, 6], a theory that seeks mathematise version control systems like, and to provide provably correct merging algorithms. Patch theory arose in the context of the DARCS system. [7] connects patch theory with homotopy type theory. [1] https://ifl2014.github.io/submissions/ifl2014_submission_32.pdf https://ifl2014.github.io/submissions/ifl2014_submission_32.... [2] J. Dagit, Type-Correct Changes - A Safe Approach to Version Control Implementation. [3] G. Sittampalam, Some properties of darcs patch theory. [4] I. Lynagh, Camp Patch Theory. [5] D. Roundy, Implementing the darcs patch formalism ... and verifying it. [6] J. Jacobson, A Formalization Of Darcs Patch Theory Using Inverse Semigroups. [7] C. Angiuli, E. Morehouse, D. R. Licata, R. Harper, Homotopical Patch Theory.