Generic Programming for Dependent Types

Abstract We begin by revisiting the idea of using a universe of types to write generic programs,in a dependently,typed setting by con- structing a universe for Strictly Positive Types (SPTs). Here we extend this construction to cover dependent types, i.e. Strictly Pos- itive Families (SPFs), thereby fixing a gap left open in previous work. Using the approach,presented here we are able to represent all of Epigram’s datatypes within Epigram including the universe of datatypes itself. Keywords Data type generic programming, dependently typed programming, Epigram