Publication
∂ for Data: Differentiating Data Structures
Authors:
Michael
Abbott
(Diamond Light Source)
,
Thorsten
Altenkirch
(The University of Nottingham)
,
Conor
Mcbride
(The University of Nottingham)
,
Neil
Ghani
(University of Leicester)
Co-authored by industrial partner:
No
Type:
Journal Paper
Journal:
Fundamenta Informaticae
, VOL 65
, PAGES 1-29
State:
Published (Approved)
Published:
January 2005
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.
Subject Areas:
Technique Development
Technical Areas:
Controls