Generic programming for indexed datatypes
José Pedro Magalhães, Johan T. Jeuring · 2011
An indexed datatype is a type that uses a parameter as a type-level tag; a typical example is the type of vectors, which are indexed over a type-level natural number encoding their length. Since the introduction of generalised algebraic datatypes, indexed datatypes have become commonplace in Haskell. Values of indexed datatypes are often more involved than values of plain datatypes, and programmers would benefit from having generic programs on indexed datatypes. However, no generic programming library adequately supports them, leaving programmers with the tedious task of writing repetitive code.