Leibniz and the Zipper

Conor McBride

I shall present a universe construction for the regular datatypes (those generated by polynomial expressions and least fixed point) in type theory, giving us the means to develop their operations and properties generically. Because the `names of types' are just data, we can compute with them in the ordinary way, giving us a great deal more power than `generic programming' extensions of Haskell. A substantial example follows...

Gerard Huet's classic paper `The Zipper' shows us informally how to equip a recursive datatype with its associated type of one-hole contexts, with applications to structure-editing. In this talk, I shall give a formal presentation of this calculation for the regular datatypes: the rules will seem familiar---Leibniz discovered them several centuries ago. The operation which plugs a term into a one-hole context is developed generically for every regular type.