Leibniz and the Zipper
Conor McBride
University of Durham
Abstract:
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.
Back to schedule.
Marieke Huisman