Much has been said and done about generic programming approaches in strongly-typed functional languages such as Haskell and Agda. Different approaches use different techniques and are better or worse suited for certain uses, depending on design decisions such as generic view, universe size and complexity, etc. We present a simple and intuitive yet powerful approach to generic programming in Agda using indexed functors. We show a universe incorporating fixed points that supports composition, indexing, and isomorphisms, and generalizes a number of previous approaches to generic programming with fixed points. Our indexed functors come with a map operation which obeys the functor laws, and associated recursion morphisms. Albeit expressive, the universe remains simple enough to allow defining standard recursion schemes as well as decidable equality. As for type-indexed datatypes, we show how to compute the type of one-hole contexts and define the generic zipper.
Generic programming with indexed functorsWGP '11 Proceedings of the seventh ACM SIGPLAN workshop on Generic programming, 2011
