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
dependently typed language, using data as codes for types.