I (Thomas Williams) am currently doing an internship with Pierre Dagand and Didier Rémy on ornaments, a way to relate datatypes sharing a common structure. Ornaments come from the scary world of dependent types, and the goal of my internship is to implement them in the more familiar setting of ML datatypes. We’ve produced a draft where we present how ornaments can be useful in practice in an ML-like programming language.
Ornaments in practice
Thomas Williams, Pierre-Évariste Dagand, Didier Rémy
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. 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.
I plan to release a usable version of the prototype described in the paper before the end of my internship, but you can find it in its current state on gitorious. Meanwhile, you can have a look at the examples presented in the paper.