Document Open Access Logo

Approximation of Nested Fixpoints – A Coalgebraic View of Parametric Dataypes

Authors Alexander Kurz, Alberto Pardo, Daniela Petrisan, Paula Severi, Fer-Jan de Vries

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2015.205.pdf
  • Filesize: 0.56 MB
  • 16 pages

Document Identifiers

Author Details

Alexander Kurz
Alberto Pardo
Daniela Petrisan
Paula Severi
Fer-Jan de Vries

Cite AsGet BibTex

Alexander Kurz, Alberto Pardo, Daniela Petrisan, Paula Severi, and Fer-Jan de Vries. Approximation of Nested Fixpoints – A Coalgebraic View of Parametric Dataypes. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 205-220, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.CALCO.2015.205

Abstract

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.
Keywords
  • coalgebra
  • Bekic lemma
  • infinite data
  • functional programming
  • type theory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. 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. Google Scholar
  2. R. C. Backhouse, M. Bijsterveld, R. van Geldrop, and J. van der Woude. Categorical fixed point calculus. In Category Theory and Computer Science, 1995. Google Scholar
  3. M. Barr. Terminal coalgebras for endofunctors on sets. Theoretical Computer Science, 114(2):299-315, 1999. Google Scholar
  4. R. S. Bird and O. de Moor. Algebra of programming. Prentice Hall, 1997. Google Scholar
  5. R. S. Bird. Introduction to Functional Programming using Haskell (second edition). Prentice Hall, 1998. Google Scholar
  6. R. S. Bird and R. Paterson. Generalised folds for nested datatypes. Formal Asp. Comput., 11(2), 1999. Google Scholar
  7. S.L. Bloom, Z. Ésik, A. Labella, and E. G. Manes. Iteration 2-theories. Applied Categorical Structures, 9(2):173-216, 2001. Google Scholar
  8. F. Borceux. Handbook of Categorical Algebra I. Cambridge University Press, 1994. Google Scholar
  9. 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. Google Scholar
  10. 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. Google Scholar
  11. Z. Ésik and A. Labella. Equational properties of iteration in algebraically complete categories. Theoretical Computer Science, 195(1):61-89, 1998. Google Scholar
  12. M. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. PhD thesis, University of Edinburgh, 1994. Google Scholar
  13. 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. Google Scholar
  14. Haskell Chasing Bottoms Package: For testing partial and infinite values. http://hackage.haskell.org/package/ChasingBottoms. Online: accessed March 2015.
  15. G. Hutton and J. Gibbons. The generic approximation lemma. Inf. Process. Lett., 79(4):197-201, 2001. Google Scholar
  16. C. B. Jones, editor. Programming Languages and Their Definition - Hans Bekic (1936-1982), LNCS 177. Springer, 1984. Google Scholar
  17. 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. Google Scholar
  18. 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.
  19. R. Lämmel and S. L. Peyton Jones. Scrap your boilerplate: a practical design pattern for generic programming. In TLDI'03, 2003. Google Scholar
  20. D. J. Lehmann and M. B. Smyth. Algebraic specification of data types: A synthetic approach. Mathematical Systems Theory, 14:97-139, 1981. Google Scholar
  21. C. E. Martin, J. Gibbons, and I. Bayley. Disciplined, efficient, generalised folds for nested datatypes. Formal Asp. Comput., 16(1):19-35, 2004. Google Scholar
  22. A. Pitts. An elementary calculus of approximations. Unpublished note. Google Scholar
  23. Haskell Regular: Generic programming library for regular datatypes. http://hackage.haskell.org/package/regular. Online accessed: March 2015.
  24. A. Rodriguez, S. Holdermans, A. Löh, and J. Jeuring. Generic programming with fixed points for mutually recursive datatypes. In ICFP, 2009. Google Scholar
  25. 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. Google Scholar
  26. 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. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact