Affiliations: Diamond Light Source, Rutherford Appleton Laboratory,
UK. [email protected] | School of Computer Science & IT, The University of
Nottingham, UK. [email protected]; [email protected] | Department of Mathematics and Computer Science,
University of Leicester, UK. [email protected]
Note: [] Address for correspondence: School of Computer Science & IT,
The University of Nottingham, UK
Abstract: This paper and our conference paper (Abbott, Altenkirch, Ghani, and
McBride, 2003b) explain and analyse the notion of the derivative of a data
structure as the type of its one-hole contexts based on the central observation
made by McBride (2001). To make the idea precise we need a generic notion of a
data type, which leads to the notion of a container, introduced in (Abbott,
Altenkirch, and Ghani, 2003a) and investigated extensively in (Abbott, 2003).
Using containers we can provide a notion of linear map which is the concept
missing from McBride's first analysis. We verify the usual laws of differential
calculus including the chain rule and establish laws for initial algebras and
terminal coalgebras.
