∂ 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