The Essence of Ornaments
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. Finally, 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 or refinement types.