A Categorical Treatment of Ornaments

Ornaments aim at taming the multiplication of special-purpose datatypes in dependently typed programming languages. In type theory, purpose is logic. By presenting datatypes as the combination of a structure and a logic, ornaments relate these special-purpose datatypes through their common structure. In the original presentation, the concept of ornament was introduced concretely for an example universe of inductive families in type theory, but it was clear that the notion was more general. This paper digs out the abstract notion of ornaments in the form of a categorical model. As a necessary first step, we abstract the universe of datatypes using the theory of polynomial functors. We are then able to characterise ornaments as cartesian morphisms between polynomial functors. We thus gain access to powerful mathematical tools that shall help us understand and develop ornaments. We shall also illustrate the adequacy of our model. Firstly, we rephrase the standard ornamental constructions into our framework. Thanks to its conciseness, we gain a deeper understanding of the structures at play. Secondly, we develop new ornamental constructions, by translating categorical structures into type theoretic artefacts.