一句话：用多类签名抽象索引数据类型，为 ornaments 建立去语法化模型，使其可推广到 GADTs/refinement types。
函数式程序员常用精细索引的数据类型来刻画程序不变式，并由此发展出 ornaments 理论；但 ornaments 原生于依赖类型，对非依赖类型的程序员而言较为艰深。本文旨在从第一性原理介绍 ornaments，并剥离其语法细节。作者用 many-sorted signatures（多类签名）为索引数据类型建立足够抽象的模型，将索引数据类型形式化为数据结构与数据逻辑的组合。在此抽象之上重新表述 ornaments 的定义，从而给出 ornaments 的模型。该模型兼具操作性与抽象性，使 ornaments 有望超越类型论圈子，适用于支持 GADTs 或 refinement types 的语言。
Abstract 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, 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.