Bibliography

• Constructing Universes for Generic Programming - PhD Thesis

  Peter Morris

  My thesis, which revisits all of the work from the papers below, spelled out with more detail. The second chapter also serves as a nice introduction to the Epigram system. (pdf)

• A Universe of Strictly Positive Families

  Peter Morris, Thorsten Altenkirch, Neil Ghani

  International Journal of Foundations of Computer Science - Volume 20

  A slightly different presentation of the first half of Constructing Strictly Positive Families with more detail on generic programming. (pdf)

• Constructing Strictly Positive Families

  Peter Morris, Thorsten Altenkirch, Neil Ghani

  Theory of Computing 2007 - ISBN:1-920-68246-5

  Revisiting earlier work we consider a telescopic universe for strictly positive types and extend the scope of the techniques to include strictly positive families. Some generic programs defined for families include equality, modalities, map and find. We also consider a translation to Indexed Containers. (pdf)

• Exploring the Regular Tree Types

  Peter Morris, Thorsten Altenkirch, Conor McBride

  Types for Proofs and Programs (TYPES 2004) - ISBN:3-540-31428-8

  In this paper we use the Epigram language to define the universe of regular tree types---closed under empty, unit, sum, product and least fixpoint. We then present a generic decision procedure for Epigram's in-built equality at each type. We also give a generic definition of map, taking our inspiration from PolyP. Finally, we equip the regular universe with the partial derivative which can be interpreted functionally as Huet's notion of `zipper', as suggested by McBride and implemented (without the fixpoint case) in Generic Haskell. We aim to show through these examples that generic programming can be ordinary programming in a dependently typed language. (pdf)