δ for Data: Differentiating Data Structures

• Autorzy: Abbott M. , Altenkirch T. , McBride C. , Ghani N.
• Języki publikacji: EN

Abstrakty

EN

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.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2005
• Tom: Vol. 65, nr 1,2
• Strony: 1--28
• Opis fizyczny: Bibliogr. 20 poz.

Twórcy

autor

Abbott M.

• Diamond Light Source Rutherford Appleton Laboratory, U.K.
• ---

autor

Altenkirch T.

• School of Computer Science & IT The University of Nottingham, U.K.

autor

McBride C.

• School of Computer Science & IT The University of Nottingham, U.K.

autor

Ghani N.

• Department of Mathematics and Computer Science University of Leicester, U.K.

Bibliografia

• [1]. M. Abbott. Categories of Containers. PhD thesis, University of Leicester, 2003.
• [2]. M. Abbott, T. Altenkirch, and N. Ghani. Categories of containers. In Proceedings of Foundations of Software Science and Computation Structures, 2003a.
• [3]. M. Abbott, T. Altenkirch, and N. Ghani. Containers - constructing strictly positive types. To appear in Journal of Theoretical Computer Science, 2005.
• [4]. M. Abbott, T. Altenkirch, N. Ghani, and C. McBride. Derivatives of containers. In Typed Lambda Calculi and Applications, TLCA, 2003b.
• [5]. P. Aczel. On relating type theories and set theories. Lecture Notes in Computer Science, 1657:1–20, 1999.
• [6]. T. Ehrhard and L. Regnier. The differential lambda-calculus. Theor. Comput. Sci., 309(1):1–41, 2003. doi: http://dx.doi.org/10.1016/S0304-3975(03)00392-X.
• [7]. M. Fiore. Generalised species of structures: Cartesian closed and differential structure. available online, 2004.
• [8]. M. Fiore, G. Plotkin, and D. Turi. Abstract syntax and variable binding. In Proc. 14th LICS Conf., pages 193–202. IEEE, Computer Society Press, 1999.
• [9]. R. Hasegawa. Two applications of analytic functors. Theoretical Comput. Sci., 272(1-2):112–175, 2002.
• [10]. M. Hofmann. On the interpretation of type theory in locally cartesian closed catetories. In Computer Science Logic, volume 933 of LNCS, 1994.
• [11]. M. Hofmann. Syntax and semantics of dependent types. In A. M. Pitts and P. Dybjer, editors, Semantics and Logics of Computation, volume 14, pages 79–130. Cambridge University Press, Cambridge, 1997.
• [12]. G. Huet. The zipper. Journal of Functional Programming, 7(5):549–554, 1997.
• [13]. B. Jay and J. R. B. Cockett. Shapely types and shape polymorphism. In D. Sannella, editor, Programming Languages and Systems - ESOP ’94: 5th European Symposium on Programming, U.K., April 1994, Proceedings, Lecture Notes in Computer Science, pages 302–316. Springer-Verlag, 1994.
• [14]. A.Joyal. Foncteurs analytiques et espéces de structures. In Combinatoire énumérative, number 1234 in LNM, pages 126 – 159. 1986.
• [15]. Z. Luo and R. Pollack. LEGO Proof Development System: User’s Manual. Technical Report ECSLFCS-92-211, Laboratory for Foundations of Computer Science, University of Edinburgh, 1992.
• [16]. C. McBride. The derivative of a regular type is its type of one-hole contexts. URL http://www.cs.nott.ac.ul/ćtm/diff.ps.gz. Available electronically, 2001.
• [17]. C. McBride. Epigram: Practical programming with dependent types. Lecture notes of the Advanced Functional Programming Summerschool in Tartu, Estonia, to appear in LNCS, 2005+.
• [18]. C.McBride and J.McKinna. The view from the left. Journal of Functional Programming, 14(1):16–111, 2004.
• [19]. Moerdijk and E. Palmgren. Wellfounded trees in categories. Annals of Pure and Applied Logic, 104: 189–218, 2000.
• [20]. D. S. Rajan. The adjoints to the derivative functor on species. J. Comb. Theory Ser. A, 62(1):93–106, 1993. doi: http://dx.doi.org/10.1016/0097-3165(93)90073-H.