Ornamental Algebras, Algebraic Ornaments
Conor Thomas McBride · 2014
This paper re-examines the presentation of datatypes in dependently typed languages, addressing in particular the issue of what it means for one datatype to be in various ways more informative than another. Informal human observations like ‘lists are natural numbers with extra decoration’ and ‘vectors are lists indexed by length’ are expressed in a first class language of ornaments — presentations of fancy new types based on plain old ones — encompassing both decoration and, in the sense of Tim Freeman and Frank Pfenning (1991), refinement. Each ornament adds information, so it comes with a forgetful function from fancy data back to plain, expressible as the fold of its ornamental algebra: lists built from numbers acquire the ‘length’ algebra. Conversely, each algebra for a datatype induces a way to index it — an algebraic ornament. The length algebra for lists induces the construction of the paradigmatic dependent vector types. Dependent types thus provide not only a new ‘axis of diversity’ — indexing — for data structures, but also new abstractions to manage and exploit that diversity. In the spirit of ‘the new programming’ (McBride & McKinna, 2004), the engineering of coincidence is replaced by the propagation of consequence.