A family of universes for generic programming

Abstract

Datatype-generic programming in the dependently typed setting can be achieved using the universe construction. The set of codes of the universe has an impact on the datatypes it can express and also on the set of supported datatype-generic functions. For example a universe with a code for functions can express datatypes such as the Brouwer ordinals: data Ord : Set where zero : Ord suc : Ord ! Ord limit : (N ! Ord) ! Ord -- The function code is needed to -- describe limit. It cannot support a meaningful datatype-generic decidable equality however, because generally equality of functions is undecidable. This problem often leads to the adaptation of several universes, for example one without a code for functions for which we can have decidable equality and another with a code for functions for which we can express datatypes such as the Brouwer ordinals. Both universes might support, for example, a datatypegeneric mapping and iteration function however, this leads to code duplication-defeating one of the very aims of datatype-generic programming. This work proposes a way around this problem by presenting a family of universes(or an indexed universe), where the index explains what class of datatypes that is supported. Datatype-generic functions which work over multiple classes of datatypes, such as mapping and iterating, are implemented using a polymorphic index. The entire development is carried out in Agda. It is at least partially compatible with levitation and ornamentation, which are recently proposed techniques for avoiding code duplication, both based on the universe construction.