Document Open Access Logo

Mendler Dialgebras and Recursion Schemes of Mixed Variance

Author Stephan Alexander Spahn

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2025.15.pdf
  • Filesize: 0.87 MB
  • 24 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Semantics and reasoning
Keywords
  • Mendler Algebra
  • Dinatural Transformation
  • Structured Recursion Scheme
  • Grothendieck Fibration
  • Higher-Order Abstract Syntax

Metrics

Abstract

We introduce the notion of Mendler dialgebra and provide a categorical semantics of recursion schemes of mixed variance in its terms. The Mendler-style approach - which employs second-order inference rules - to recursion schemes of mixed variance was championed by Uustalu and Vene in [Uustalu and Vene, 1999] using dinatural transformations, and we generalize their methods to include a variety of new recursion schemes including those presented by Ahn-Sheard in [Ahn and Sheard, 2011], and Stump et al. in [Aaron Stump et al., 2020]. We give sufficient criteria for reducibility of Mendler dialgebras to Lambek algebras [Joachim Lambek, 1968] which correspond to first-order inference rules. A similar reduction in elementary terms for the special case of the systems studied in [Uustalu and Vene, 1999] had been given by the authors, but our approach differs in that we use the language of two-sided fibrations [Street, 1974] to express the reduction for our generalization. This reveals that the "diagonal" of every two-sided fibration with a fibered initial object is isomorphic to a category of Lambek algebras; a dual version concerning reduction to Lambek coalgebras, as well as to bialgebras (inserters), [Joachim Lambek, 1970] is given. We also discuss various properties and examples of Mendler dialgebras, including higher-order abstract syntax which is paradigmatic for definitions of mixed variance. Generally, we regard the paper as a contribution to a more systematic understanding of the relation between higher-order and first-order inference rules.

Cite As Get BibTex

Stephan Alexander Spahn. Mendler Dialgebras and Recursion Schemes of Mixed Variance. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 15:1-15:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.TYPES.2025.15

Author Details

Stephan Alexander Spahn
  • Department of Computer Science, Tallinn University of Technology, Estonia

Acknowledgements

I would like to thank Aaron Stump, Christopher Jenkins, Fredrik Nordvall Forsberg, Tarmo Uustalu, and Pawel Sobocinski for discussions about Mendler algebras as well as comments on the draft.

References

  1. Michael Gordon Abbott, Thorsten Altenkirch, and Neil Ghani. Containers: Constructing strictly positive types. Theor. Comput. Sci., 342(1):3-27, 2005. URL: https://doi.org/10.1016/j.tcs.2005.06.002.
  2. Andreas Abel, Ralph Matthes, and Tarmo Uustalu. Iteration and coiteration schemes for higher-order and nested datatypes. Theor. Comput. Sci., 333(1-2):3-66, 2005. URL: https://doi.org/10.1016/j.tcs.2004.10.017.
  3. Ki Yung Ahn and Tim Sheard. A hierarchy of mendler style recursion combinators: Taming inductive datatypes with negative occurrences. SIGPLAN Not., 46(9):234-246, September 2011. URL: https://doi.org/10.1145/2034574.2034807.
  4. E. S. Bainbridge, Peter J. Freyd, Andre Scedrov, and Philip J. Scott. Functorial polymorphism. Theoretical Computer Science, 70(1):35-64, 1990. URL: https://doi.org/10.1016/0304-3975(90)90151-7.
  5. Jon Beck. Distributive laws. In B. Eckmann, editor, Seminar on Triples and Categorical Homology Theory, pages 119-140. Springer Berlin Heidelberg, 1969. Google Scholar
  6. Richard Bird and Lambert Meertens. Nested datatypes. In Johan Jeuring, editor, Mathematics of Program Construction, pages 52-67. Springer Berlin Heidelberg, 1998. URL: https://doi.org/10.1007/BFB0054285.
  7. Nicolas Blanco and Noam Zeilberger. Bifibrations of polycategories and classical linear logic. In 36th International Conference on Mathematical Foundations of Programming Semantics - MFPS 2020, 2020. Google Scholar
  8. Joachim de Lataillade. Dinatural terms in system F. In Proceedings of the 2009 24th Annual IEEE Symposium on Logic in Computer Science, pages 267-276. IEEE Computer Society, 2009. URL: https://doi.org/10.1109/LICS.2009.30.
  9. Eduardo Dubuc and Ross Street. Dinatural transformations. In S. MacLane, H. Applegate, M. Barr, B. Day, E. Dubuc, Phreilambud, A. Pultr, R. Street, M. Tierney, and S. Swierczkowski, editors, Reports of the Midwest Category Seminar IV, pages 126-137. Springer Berlin Heidelberg, 1970. Google Scholar
  10. Adam Eppendahl. Parametricity and Mulry’s strong dinaturality. Technical Report 768, Department of Computer Science, Queen Mary and Westfield College, University of London, 1999. Google Scholar
  11. Adam Eppendahl. Cospan diparametricity, (unpublished manuscript), 2005. Google Scholar
  12. Leonidas Fegaras and Tim Sheard. Revisiting catamorphisms over datatypes with embedded functions (or, programs from outer space). In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’96, pages 284-294, New York, NY, USA, 1996. Association for Computing Machinery. URL: https://doi.org/10.1145/237721.237792.
  13. Marcelo P. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. Cambridge University Press, USA, 1996. Google Scholar
  14. Peter Freyd. Recursive types reduced to inductive types. In Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, pages 498-507, Los Alamitos, CA, USA, June 1990. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.1990.113772.
  15. Neil Ghani, Lorenzo Malatesta, and Fredrik Nordvall Forsberg. Positive inductive-recursive definitions. Log. Methods Comput. Sci., 11(1), 2015. URL: https://doi.org/10.2168/LMCS-11(1:13)2015.
  16. Neil Ghani, Tarmo Uustalu, and Varmo Vene. Build, augment and destroy, universally. In Wei-Ngan Chin, editor, Programming Languages and Systems, pages 327-347. Springer Berlin Heidelberg, 2004. URL: https://doi.org/10.1007/978-3-540-30477-7_22.
  17. John W. Gray. The integration of logical and algebraic types. In H. Ehrig, H. Herrlich, H. J. Kreowski, and G. Preuß, editors, Categorical Methods in Computer Science With Aspects from Topology, pages 16-35. Springer Berlin Heidelberg, 1989. Google Scholar
  18. Tatsuya Hagino. A Categorical Programming Language. PhD thesis, University of Edinburgh, 1987. Google Scholar
  19. Claudio Hermida and Paulo Mateus. Paracategories I: internal paracategories and saturated partial algebras. Theor. Comput. Sci., 309(1-3):125-156, 2003. URL: https://doi.org/10.1016/S0304-3975(03)00135-X.
  20. Claudio Hermida and Paulo Mateus. Paracategories II: adjunctions, fibrations and examples from probabilistic automata theory. Theor. Comput. Sci., 311(1-3):71-103, 2004. URL: https://doi.org/10.1016/S0304-3975(03)00317-7.
  21. Bart Jacobs. Categorical Logic and Type Theory. Studies in logic and the foundations of mathematics. Elsevier Science, 1999. Google Scholar
  22. Bart Jacobs. A bialgebraic review of deterministic automata, regular expressions and languages. In Kokichi Futatsugi, Jean-Pierre Jouannaud, and José Meseguer, editors, Algebra, Meaning, and Computation: Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday, pages 375-404. Springer Berlin Heidelberg, 2006. URL: https://doi.org/10.1007/11780274_20.
  23. Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge tracts in theoretical computer science. Cambridge University Press, 2016. URL: https://doi.org/10.1017/CBO9781316823187.
  24. Patricia Johann and Neil Ghani. Initial algebra semantics is enough! In Simona Ronchi Della Rocca, editor, Typed Lambda Calculi and Applications, pages 207-222. Springer Berlin Heidelberg, 2007. URL: https://doi.org/10.1007/978-3-540-73228-0_16.
  25. G. M. Kelly. Basic concepts of enriched category theory. Reprints in Theory and Applications of Categories, 10:vi+137, 2005. Reprint of the 1982 original. Google Scholar
  26. G.M. Kelly. A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on. Bulletin of the Australian Mathematical Society, 22(1):1-83, 1980. URL: https://doi.org/10.1017/S0004972700006353.
  27. Joachim Lambek. A fixpoint theorem for complete categories. Mathematische Zeitschrift, 103:151-161, 1968. Google Scholar
  28. Joachim Lambek. Subequalizers. J-Can-Math-Bull, 13:337-350, 1970. URL: https://doi.org/10.4153/CMB-1970-065-6.
  29. Fosco Loregian and Emily Riehl. Categorical notions of fibration. Expositiones Mathematicae, 38(4):496-514, 2020. URL: https://doi.org/10.1016/j.exmath.2019.02.004.
  30. Saunders MacLane. The Yoneda lemma. Mathematica Japonicae, 47:156, 1998. Google Scholar
  31. Jean-Pierre Marquis. From a Geometrical Point of View: A Study of the History and Philosophy of Category Theory. Philosophia Mathematica, 18(2):227-234, March 2010. URL: https://doi.org/10.1093/philmat/nkq006.
  32. Guy McCusker and Alessio Santamaria. On compositionality of dinatural transformations. In Dan R. Ghica and Achim Jung, editors, 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK, volume 119 of LIPIcs, pages 33:1-33:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CSL.2018.33.
  33. Erik Meijer and Graham Hutton. Bananas in space: Extending fold and unfold to exponential types. In Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture, FPCA ’95, pages 324-333, New York, NY, USA, 1995. Association for Computing Machinery. URL: https://doi.org/10.1145/224164.224225.
  34. N. P. Mendler. Recursive types and type constraints in second-order lambda calculus. In LICS, 1987. Google Scholar
  35. Nax Paul Mendler. Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic, 51(1):159-172, 1991. URL: https://doi.org/10.1016/0168-0072(91)90069-X.
  36. Yiannis N. Moschovakis. Elementary Induction on Abstract Structures. Dover Publications, 1974. Google Scholar
  37. Fredrik Nordvall Forsberg. Inductive-inductive definitions. PhD thesis, Swansea University, 2013. URL: https://personal.cis.strath.ac.uk/fredrik.nordvall-forsberg/thesis/thesis.pdf.
  38. Robert Paré and Leopoldo Román. Dinatural numbers. Journal of Pure and Applied Algebra, 128:33-92, June 1998. URL: https://doi.org/10.1016/S0022-4049(97)00036-4.
  39. Gordon D. Plotkin and Martín Abadi. A logic for parametric polymorphism. In Marc Bezem and Jan Friso Groote, editors, Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA '93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings, volume 664 of Lecture Notes in Computer Science, pages 361-375. Springer, 1993. URL: https://doi.org/10.1007/BFb0037118.
  40. Wolfram Pohlers. Proof theory. The first step into impredicativity. 2nd printing. Springer, January 2009. URL: https://doi.org/10.1007/978-3-540-69319-2.
  41. Emily Riehl. Category theory in context. Dover Modern Math Originals, Courier Dover Publications, 2017. Google Scholar
  42. Alessio Santamaria. Towards a Godement Calculus for Dinatural Transformations. PhD thesis, University of Bath, 2019. Google Scholar
  43. Ross Street. Fibrations and Yoneda’s lemma in a 2-category. In Gregory M. Kelly, editor, Category Seminar, pages 104-133. Springer Berlin Heidelberg, 1974. Google Scholar
  44. Thomas Streicher. Fibred Categories à la Jean Bénabou. arXiv e-prints, January 2018. URL: https://arxiv.org/abs/1801.02927.
  45. Aaron Stump, Christopher Jenkins, Stephan Spahn, and Colin McDonald. Strong functional pearl: Harper’s regular-expression matcher in Cedille. In 25th ACM SIGPLAN International Conference on Functional Programming - ICFP, 2020. Google Scholar
  46. Tarmo Uustalu. Strong dinaturality and initial algebras. Presented at the 12th Nordic Workshop on Programming Theory, October 11–13, 2000, Bergen, Norway, 2000. Google Scholar
  47. Tarmo Uustalu. A note on strong dinaturality, initial algebras and uniform parameterized fixpoint operators. In Luigi Santocanale, editor, 7th Workshop on Fixed Points in Computer Science, FICS 2010, Brno, Czech Republic, August 21-22, 2010, pages 77-82. Laboratoire d'Informatique Fondamentale de Marseille, 2010. URL: https://hal.archives-ouvertes.fr/hal-00512377/document#page=78.
  48. Tarmo Uustalu and Varmo Vene. Mendler-style inductive types, categorically. Nordic J. of Computing, 6(3):343-361, September 1999. Google Scholar
  49. Tarmo Uustalu and Varmo Vene. Primitive (co)recursion and course-of-value (co)iteration, categorically. Informatica, 10(1):5-26, 1999. URL: https://doi.org/10.3233/INF-1999-10102.
  50. Tarmo Uustalu and Varmo Vene. Coding recursion a la Mendler (extended abstract). Technical report, Department Of Computer Science, Utrecht University, 2000. Google Scholar
  51. Tarmo Uustalu and Varmo Vene. The recursion scheme from the cofree recursive comonad. Electron. Notes Theor. Comput. Sci., 229(5):135-157, 2011. URL: https://doi.org/10.1016/j.entcs.2011.02.020.
  52. Geoffrey Washburn and Stephanie Weirich. Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism. J. Funct. Program., 18(1):87-140, 2008. URL: https://doi.org/10.1017/S0956796807006557.
  53. Mark Weber. Yoneda structures from 2-toposes. Applied Categorical Structures, 15:259-323, 2007. URL: https://doi.org/10.1007/S10485-007-9079-2.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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