AbstractFunctional 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, lead to the development of a theory of ornaments (McBride, 2011 Ornamental Algebras, Algebraic Ornaments. Unpublished). However, ornaments originate as a dependently-typed object and may thus appear rather daunting to a functional programmer of the non-dependent kind. This article aims at presenting ornaments from first-principles and, in particular, to declutter their presentation 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 formalize our intuition that an indexed datatype is the combination of a data-structure and a data-logic. 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, 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.
Refinement Types as Proof Irrelevance
