The Essence of Ornaments (pdf) is a draft of a new article, hoping to provide an accessible introduction to the theory of ornaments. Any feedback on the draft, in the comments or by email, is warmly welcome.

You should not need to be familiar with inductive encodings of datatype universes or category theory to read this new article. It is still less practice-oriented, however, that the Ornaments in practice work with Thomas Williams and Didier Rémy, to which you should give a try first if you’re more into the programming applications than the theory.

.

The Essence of Ornaments (pdf)
Pierre-Évariste Dagand 2014

Functional programmers from all horizons strive to use, and sometimes abuse, their favorite type system in order to capture the invariants of their programs. A widely-used tool in that trade consists in defining finely-indexed datatypes. Operationally, these types classify the programmer’s data, following the ML tradition. Logically, these types enforce the program invariants in a novel manner. This new programming pattern, by which one programs over inductive definitions to account for some invariants, is the motivation behind the theory of ornaments.

However, ornaments originate from dependent type theory and may thus appear rather daunting to a functional programmer of the non dependent kind. Ornaments may also appear quite specific to a particular type theory whilst, in fact, they are a very general notion. This article aims at presenting the notion of ornament from first-principles and, in particular, decluttered from syntactic considerations.

To do so, we shall give a sufficiently abstract model of indexed datatypes by means of many-sorted signatures. In this process, we formalise our intuition that an indexed datatype is the combination of a data-structure and a data-logic. Unlike a purely categorical presentation, this model will appeal to our programmer’s intuition: we shall be manipulating (type-theoretic) functions, remaining close to our functional comfort zone.

Over this abstraction of datatypes, we shall recast the definition of ornaments, effectively giving a model of ornaments. Benefiting both from the operational and abstract nature of many-sorted signatures, we cast ornaments under an operational and an abstract light. The versatility of our model has been instrumental in the development of a genuine “calculus of data-structures”: with a few combinators, new datatypes can be engineered by composing off-the-shelf data-structures with special-purpose data-logics. In this article, we shall illustrate these techniques by way of examples.

As a result, ornaments should appear applicable and, one hopes, of interest beyond the type-theoretic circles, case in point being languages with generalized abstract datatypes, such as Haskell or ML.