Approximation of Nested Fixpoints – A Coalgebraic View of Parametric Dataypes
The question addressed in this paper is how to correctly approximate infinite data given by systems of simultaneous corecursive definitions. We devise a categorical framework for reasoning about regular datatypes, that is, datatypes closed under products, coproducts and fixpoints. We argue that the right methodology is on one hand coalgebraic (to deal with possible nontermination and infinite data) and on the other hand 2-categorical (to deal with parameters in a disciplined manner). We prove a coalgebraic version of Bekic lemma that allows us to reduce simultaneous fixpoints to a single fix point. Thus a possibly infinite object of interest is regarded as a final coalgebra of a many-sorted polynomial functor and can be seen as a limit of finite approximants. As an application, we prove correctness of a generic function that calculates the approximants on a large class of data types.
coalgebra
Bekic lemma
infinite data
functional programming
type theory
205-220
Regular Paper
Alexander
Kurz
Alexander Kurz
Alberto
Pardo
Alberto Pardo
Daniela
Petrisan
Daniela Petrisan
Paula
Severi
Paula Severi
Fer-Jan
de Vries
Fer-Jan de Vries
10.4230/LIPIcs.CALCO.2015.205
R. Atkey and C. McBride. Productive coprogramming with guarded recursion. In ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25-27, 2013, pages 197-208, 2013.
R. C. Backhouse, M. Bijsterveld, R. van Geldrop, and J. van der Woude. Categorical fixed point calculus. In Category Theory and Computer Science, 1995.
M. Barr. Terminal coalgebras for endofunctors on sets. Theoretical Computer Science, 114(2):299-315, 1999.
R. S. Bird and O. de Moor. Algebra of programming. Prentice Hall, 1997.
R. S. Bird. Introduction to Functional Programming using Haskell (second edition). Prentice Hall, 1998.
R. S. Bird and R. Paterson. Generalised folds for nested datatypes. Formal Asp. Comput., 11(2), 1999.
S.L. Bloom, Z. Ésik, A. Labella, and E. G. Manes. Iteration 2-theories. Applied Categorical Structures, 9(2):173-216, 2001.
F. Borceux. Handbook of Categorical Algebra I. Cambridge University Press, 1994.
A. Cave, F. Ferreira, P. Panangaden, and B. Pientka. Fair reactive programming. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'14, San Diego, CA, USA, January 20-21, 2014, pages 361-372, 2014.
R. A. Eisenberg and S. Weirich. Dependently typed programming with singletons. In Proceedings of the 5th ACM SIGPLAN Symposium on Haskell, Copenhagen, pages 117-130, 2012.
Z. Ésik and A. Labella. Equational properties of iteration in algebraically complete categories. Theoretical Computer Science, 195(1):61-89, 1998.
M. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. PhD thesis, University of Edinburgh, 1994.
P. Freyd. Remarks on algebraically compact categories. In Applications of Categories in Computer Science, volume 77 of London Math. Soc. Lecture Notes Series, pages 95–-106. Cambridge University Press, 1992.
Haskell Chasing Bottoms Package: For testing partial and infinite values. http://hackage.haskell.org/package/ChasingBottoms. Online: accessed March 2015.
http://hackage.haskell.org/package/ChasingBottoms
G. Hutton and J. Gibbons. The generic approximation lemma. Inf. Process. Lett., 79(4):197-201, 2001.
C. B. Jones, editor. Programming Languages and Their Definition - Hans Bekic (1936-1982), LNCS 177. Springer, 1984.
G. M. Kelly and R. Street. Review of the elements of 2-categories. In Category Seminar (Proc. Sem. Sydney 1972/73), LNM 420, pages 75-103. Springer, 1974.
A. Kurz, D. Petrişan, A. Pardo, P. Severi, and F.-J. de Vries. Haskell code for this paper. http://www.cs.le.ac.uk/people/ps56/code.xml, 2015.
http://www.cs.le.ac.uk/people/ps56/code.xml
R. Lämmel and S. L. Peyton Jones. Scrap your boilerplate: a practical design pattern for generic programming. In TLDI'03, 2003.
D. J. Lehmann and M. B. Smyth. Algebraic specification of data types: A synthetic approach. Mathematical Systems Theory, 14:97-139, 1981.
C. E. Martin, J. Gibbons, and I. Bayley. Disciplined, efficient, generalised folds for nested datatypes. Formal Asp. Comput., 16(1):19-35, 2004.
A. Pitts. An elementary calculus of approximations. Unpublished note.
Haskell Regular: Generic programming library for regular datatypes. http://hackage.haskell.org/package/regular. Online accessed: March 2015.
http://hackage.haskell.org/package/regular
A. Rodriguez, S. Holdermans, A. Löh, and J. Jeuring. Generic programming with fixed points for mutually recursive datatypes. In ICFP, 2009.
T. van Noort, A. Rodriguez Yakushev, S. Holdermans, J. Jeuring, B. Heeren, and J.P. Magalhães. A lightweight approach to datatype-generic rewriting. J. Funct. Program., 20(3-4):375-413, 2010.
B. A. Yorgey, S. Weirich, J. Cretin, S. L. Peyton Jones, D. Vytiniotis, and J. P. Magalhães. Giving Haskell a promotion. In TLDI 2012, pages 53-66, 2012.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode