Generic Programming Within Dependently Typed Programming

Thorsten Altenkirch (joint work with Conor McBride, Durham)

We show how higher kinded generic programming can be represented faithfully within a dependently typed programming system. The paper describes an implementation in the OLEG system which is used as a programming language here. The present work can be seen as evidence for our thesis that extensions of type systems can be done by *programming* within a dependently typed language, using data as codes for types.