Generic Numerical Representations as Ornaments

Abstract

The concept of numerical representations as defined by Okasaki [Oka98] explains how certain datastructures resemble number systems, and motivates how number sys- tems can be used as a basis to design datastructures. Using McBride’s ornaments [McB14], the method of designing datastructures starting from number systems can be made precise. In order to study a broad spectrum of indexed and unindexed numeri- cal representations, we encode a universe allowing the expression of nested datatypes, and the internalization of descriptions of composite types. By equipping the universe with metadata, we can describe number systems and numerical representations in the same setup. Adapting ornaments to this universe allows us to generalize well-known sequences of ornaments, such as naturals-lists-vectors. We demonstrate this by imple- menting the indexed and unindexed numerical representations as ornament-computing functions, producing a sequence of ornaments on top of the number system.