A Principled Approach to Ornamentation in ML

[uchwings]

Thomas Williams, Didier Rémy (POPL '18)

Ornaments are a way to describe changes in datatype defnitions reorganizing, adding, or dropping some pieces of data so that functions operating on the bare defnition can be partially and sometimes totally lifed 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 lifing, which lives in a meta-language above ML. The lifed code is obtained by application of the generic lifing to well-chosen arguments, followed by staged reduction, and some remaining simplifcations. We use logical relations to closely relate the lifed code to the bare code.

http://pauillac.inria.fr/%7Eremy/ornaments/mlorn-2017-09.pdf

[brianhempel]

Discussed 2018–01–09. https://uchicago-cs.github.io/plrg/