Ornaments

Ornaments

This project is joint work between Pierre Dagand, Didier Rémy, and Thomas Williams .

Ornaments in Practice.

Ornaments have been introduced as a way to describe some changes in datatype definitions that preserve their recursive structure, reorganizing, adding, or dropping some pieces of data. After a new data structure has been described as an ornament of an older one, some functions operating on the bare structure can be partially or sometimes totally lifted into functions operating on the ornamented structure. We explore the feasibility and the interest of using ornaments in practice by applying these notions in an ML-like programming language.

In this paper presented at the WGP 2014 workshop, we propose a concrete syntax for defining ornaments of datatypes and the lifting of bare functions to their ornamented counterparts, describe the lifting process, and present 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.

A Meta-Language for Ornamentation in ML.

We formalize ornaments as logical relations, which seamlessly extends to higher-order ornaments and allows to precisely relate the ornamented code with the base code. This uses an intermediate meta-language that extends ML with a limited form of dependent types in which ML programs are first lifted before being specialized and then simplified back into ML programs. See our draft paper and a run of all examples in the new prototype.