#### The Essence of Ornaments

##### Pierre-Evariste Dagand

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.