Ornaments are a way to describe changes in datatype definitions reorganizing, adding, or dropping some pieces of data so that functions operating on the bare definition can be partially and sometimes totally lifted into functions operating on the ornamented structure. We propose an extension of ML with higher-order ornaments, demonstrate its expressiveness with a few typical examples, including code refactoring, study the metatheoretical properties of ornaments, and describe their elaboration process. We formalize ornamentation via a posteriori abstraction of the bare code, called generic lifting, which lives in a meta-language above ML. The lifted code is obtained by application of the generic lifting to well-chosen arguments, followed by staged reduction, and some remaining simplifications. We use logical relations to closely relate the lifted code to the bare code.
See the preprint of our POPL 2018 paper or its extended version and the slides of the talk. See also a run of all examples in the new prototype. You may also see this talk presented in Edinburgh in May 2017 or the invited talk presented at the Haskell Symposium.
Our work on ornaments was first presented presented at the WGP 2014 workshop. We proposed a concrete syntax for defining ornaments of datatypes and the lifting of bare functions to their ornamented counterparts, described the lifting process, and presented several interesting use cases of ornaments. (You may also see the slides.) Examples of source programs from this paper and their elaboration can be found here.