Inductive datatypes and parametric polymorphism are two key features introduced in the ML family of languages, which have already been widely exploited for structuring programs: Haskell and ML programs are often more elegant and more correct by construction. Still, we sometimes need code to be refactored or adapted to be reused in a slightly different context. While the type system is considerably helpful in these situations, by automatically locating type-inconsistent program points or incomplete pattern matchings, this process could be made safer and more automated by further exploiting parametricity. We propose a posteriori program abstraction as a principle for such code transformations.

We apply this principle to ornamentation which is 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 view ornamentation as an a posteriori abstraction of the bare code, called a generic lifting, which can then be instantiated into a concrete lifting, meta-reduced, and simplified. Both the source and target code live in core ML while the lifted code lives in a meta-language above ML equipped with a limited form of dependent types needed to capture some invariants of the generic lifting so that the concrete lifting can be simplified back into an ML program. Importantly, the lifted code can be closely related to the bare code, using logical relations thanks to the generic lifting detour.

Different, typical use cases of ornaments will be shown and the approach will be mainly illustrated on examples.