Skip to Main content Skip to Navigation

Refactoring functional programs with ornaments

Abstract : Ornaments provide a way to express transformations of inductive datatypes that reorganize, specialize, and add fields to already existing datatypes. From such a transformation, we consider the problem of semi-automatically refactoring an already existing ML program operating on the base type into a program operating on the ornamented type. We describe a framework for such transformations by decomposing them in two phases: first, the base term is maximally generalized by abstracting over the details of the manipulated datatypes. This generic term is subsequently specialized to operate only on the ornamented type. We describe an intermediate language providing the necessary abstractions to present the generic term. This language notably includes dependent abstractions, allows representing the equalities learned from pattern matching, and provide a way to refer to the opaque result of previous computations. We exploit the parametricity of the generic term to derive a coherence relation between the base term and the ornamented term, guaranteeing the correctness of the ornamented term. We present an implementation of this transformation on a core ML language, and illustrate its usefulness in many common cases of program transformation: pure refactoring, adding new data and specialization. We also present a new unfolding technique afforded by our transformation and present its use for optimizing certain data representation and for generic programming.
Document type :
Complete list of metadata
Contributor : ABES STAR :  Contact
Submitted on : Wednesday, June 30, 2021 - 10:43:10 AM
Last modification on : Wednesday, June 8, 2022 - 12:50:03 PM


Version validated by the jury (STAR)


  • HAL Id : tel-03126602, version 2



Ambre Williams. Refactoring functional programs with ornaments. Programming Languages [cs.PL]. Université Paris Cité, 2020. English. ⟨NNT : 2020UNIP7161⟩. ⟨tel-03126602v2⟩



Record views


Files downloads