Document Open Access Logo

From Partial to Monadic: Combinatory Algebra with Effects

Authors Liron Cohen , Ariel Grunfeld , Dominik Kirst , Étienne Miquey

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2025.14.pdf
  • Filesize: 1.27 MB
  • 22 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • Combinatory algebras
  • Monads
  • Effects
  • Realizability
  • Evidenced frames

Metrics

Abstract

Partial Combinatory Algebras (PCAs) provide a foundational model of the untyped λ-calculus and serve as the basis for many notions of computability, such as realizability theory. However, PCAs support a very limited notion of computation by only incorporating non-termination as a computational effect. To provide a framework that better internalizes a wide range of computational effects, this paper puts forward the notion of Monadic Combinatory Algebras (MCAs). MCAs generalize the notion of PCAs by structuring the combinatory algebra over an underlying computational effect, embodied by a monad. We show that MCAs can support various side effects through the underlying monad, such as non-determinism, stateful computation and continuations. We further obtain a categorical characterization of MCAs within Freyd Categories, following a similar connection for PCAs. Moreover, we explore the application of MCAs in realizability theory, presenting constructions of effectful realizability triposes and assemblies derived through evidenced frames, thereby generalizing traditional PCA-based realizability semantics. The monadic generalization of the foundational notion of PCAs provides a comprehensive and powerful framework for internally reasoning about effectful computations, paving the path to a more encompassing study of computation and its relationship with realizability models and programming languages.

Cite As Get BibTex

Liron Cohen, Ariel Grunfeld, Dominik Kirst, and Étienne Miquey. From Partial to Monadic: Combinatory Algebra with Effects. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 14:1-14:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSCD.2025.14

Author Details

Liron Cohen
  • Ben-Gurion University, Beer-Sheva, Israel
Ariel Grunfeld
  • Ben-Gurion University, Beer-Sheva, Israel
Dominik Kirst
  • Ben-Gurion University, Beer-Sheva, Israel
  • Inria Paris, France
Étienne Miquey
  • Aix Marseille University, CNRS, I2M, Marseille, France

Funding

This work was partially supported by Grant No. 2020145 from the United States-Israel Binational Science Foundation (BSF).
  • Kirst, Dominik: Received funding from the European Union’s Horizon research and innovation programme under the Marie Skłodowska-Curie grant agreement No.101152583 and a Minerva Fellowship of the Minerva Stiftung Gesellschaft für die Forschung mbH.

Acknowledgements

We are deeply grateful to Ross Tate for his valuable ideas and insights, which significantly shaped the direction of this work.

Supplementary Materials

References

  1. Andrej Bauer and James E. Hanson. The Countable Reals, 2024. URL: https://arxiv.org/abs/2404.01256.
  2. Stefano Berardi, Marc Bezem, and Thierry Coquand. On the Computational Content of the Axiom of Choice. The Journal of Symbolic Logic, 63(2):600-622, 1998. URL: https://doi.org/10.2307/2586854.
  3. Simon Boulier, Pierre-Marie Pédrot, and Nicolas Tabareau. The Next 700 Syntactical Models of Type Theory. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 182-194, New York, NY, USA, 2017. Association for Computing Machinery. URL: https://doi.org/10.1145/3018610.3018620.
  4. Aurelio Carboni, Peter J. Freyd, and Andre Scedrov. A Categorical Approach to Realizability and Polymorphic Types. In M. Main, A. Melton, M. Mislove, and D. Schmidt, editors, Mathematical Foundations of Programming Language Semantics, pages 23-42, Berlin, Heidelberg, 1988. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-19020-1_2.
  5. Félix Castro, Alexandre Miquel, and Krzysztof Worytkiewicz. Implicative Assemblies, 2023. URL: https://arxiv.org/abs/2304.10429.
  6. J.R.B. Cockett and P.J.W. Hofstra. Introduction to Turing Categories. Annals of Pure and Applied Logic, 156(2):183-209, 2008. URL: https://doi.org/10.1016/j.apal.2008.04.005.
  7. Robin Cockett and Stephen Lack. Restriction Categories III: Colimits, Partial Limits and Extensivity. Mathematical Structures in Computer Science, 17(4):775-817, 2007. URL: https://doi.org/10.1017/S0960129507006056.
  8. Liron Cohen, Sofia Abreu Faro, and Ross Tate. The Effects of Effects on Constructivism. Electronic Notes in Theoretical Computer Science, 347:87-120, 2019. URL: https://doi.org/10.1016/j.entcs.2019.09.006.
  9. Liron Cohen, Ariel Grunfeld, Dominik Kirst, Étienne Miquey, and Ross Tate. Coq Formalization, https://github.com/dominik-kirst/mca. Supplementary Material, 2025.
  10. Liron Cohen, Étienne Miquey, and Ross Tate. Evidenced Frames: A Unifying Framework Broadening Realizability Models. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470514.
  11. Olivier Danvy. On Evaluation Contexts, Continuations, and the Rest of the Computation. In Proceedings of the Fourth ACM SIGPLAN Workshop on Continuations, Technical report CSR-04-1, Department of Computer Science, Queen Mary’s College, pages 13-23, 2004. Google Scholar
  12. Solomon Feferman. A Language and Axioms for Explicit Mathematics. In Algebra and logic, pages 87-139. Springer, 1975. URL: https://doi.org/10.1007/BFb0062852.
  13. Jonas Frey. Characterizing Partitioned Assemblies and Realizability Toposes. Journal of Pure and Applied Algebra, 223(5):2000-2014, 2019. URL: https://doi.org/10.1016/j.jpaa.2018.08.012.
  14. Samuel Gardelle and Étienne Miquey. Do CPS Translations Also Translate Realizers? In Timothy Bourke and Delphine Demange, editors, JFLA 2023 - 34èmes Journées Francophones des Langages Applicatifs, pages 103-120, Praz-sur-Arly, France, January 2023. URL: https://hal.inria.fr/hal-03910311.
  15. Michele Giry. A Categorical Approach to Probability Theory. In Categorical Aspects of Topology and Analysis: Proceedings of an International Conference Held at Carleton University, Ottawa, August 11-15, 1981, pages 68-85. Springer, 2006. URL: https://doi.org/10.1007/BFb0092872.
  16. Kurt Gödel. On Intuitionistic Arithmetic and Number Theory. Collected Works, 1:287-295, 1933. Google Scholar
  17. Mayer Goldberg. Ellipses and Lambda Definability. Logical Methods in Computer Science, Volume 11, Issue 3, October 2015. URL: https://doi.org/10.2168/lmcs-11(3:25)2015.
  18. Pieter J. W. Hofstra. All Realizability is Relative. Mathematical Proceedings of the Cambridge Philosophical Society, 141:239-264, 2006. URL: https://doi.org/10.1017/S0305004106009352.
  19. Pieter JW Hofstra. Partial Combinatory Algebras and Realizability Toposes. University of Ottowa, 2004. Google Scholar
  20. J. M. E. Hyland, P. T. Johnstone, and A. M. Pitts. Tripos theory. Mathematical Proceedings of the Cambridge Philosophical Society, 88(2):205-232, 1980. URL: https://doi.org/10.1017/S0305004100057534.
  21. Stephen Cole Kleene. On the Interpretation of Intuitionistic Number Theory. The journal of symbolic logic, 10(4):109-124, 1945. URL: https://doi.org/10.2307/2269016.
  22. Jean-Louis Krivine. Realizability in Classical Logic. In Interactive Models of Computation and Program Behaviour. Panoramas et synthèses, 27, 2009. URL: https://hal.science/hal-00154500.
  23. Jean-Louis Krivine. Realizability Algebras: A Program to Well Order R. Logical methods in computer science, 7, 2011. URL: https://doi.org/10.2168/LMCS-7(3:2)2011.
  24. Paul Blain Levy, John Power, and Hayo Thielecke. Modelling Environments in Call-by-Value Programming Languages. Information and Computation, 185(2):182-210, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00088-9.
  25. Giuseppe Longo and Eugenio Moggi. A Category-theoretic Characterization of Functional Completeness. Theoretical Computer Science, 70(2):193-211, 1990. URL: https://doi.org/10.1016/0304-3975(90)90122-X.
  26. M. Menni. Exact Completions and Toposes. PhD thesis, University of Edinburgh, 2000. Google Scholar
  27. Eugenio Moggi. Computational Lambda-calculus and Monads. [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pages 14-23, 1989. URL: https://doi.org/10.1109/LICS.1989.39155.
  28. Eugenio Moggi. Notions of Computation and Monads. Information and computation, 93(1):55-92, 1991. URL: https://doi.org/10.1016/0890-5401(91)90052-4.
  29. Guillaume Munch-Maccagnoni. Focalisation and Classical Realisability. In Erich Grädel and Reinhard Kahle, editors, Computer Science Logic '09, volume 5771 of Lecture Notes in Computer Science, pages 409-423. Springer, Heidelberg, 2009. URL: https://doi.org/10.1007/978-3-642-04027-6_30.
  30. P. Oliva and T. Streicher. On Krivine’s Realizability Interpretation of Classical Second-Order Arithmetic. Fundam. Inform., 84(2):207-220, 2008. URL: https://doi.org/10.5555/1402673.1402677.
  31. Pierre-Marie Pédrot. Russian Constructivism in a Prefascist Theory. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, pages 782-794. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394740.
  32. Pierre-Marie Pédrot and Nicolas Tabareau. Failure is Not an Option - An Exceptional Type Theory. In 27th European Symposium on Programming, volume 10801 of LNCS, pages 245-271, Thessaloniki, Greece, April 2018. Springer. URL: https://doi.org/10.1007/978-3-319-89884-1_9.
  33. Pierre-Marie Pédrot and Nicolas Tabareau. The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects. Proc. ACM Program. Lang., 4(POPL):58:1-58:28, 2020. URL: https://doi.org/10.1145/3371126.
  34. Pierre-Marie Pédrot, Nicolas Tabareau, Hans Jacob Fehrmann, and Éric Tanter. A Reasonably Exceptional Type Theory. Proc. ACM Program. Lang., 3(ICFP):108:1-108:29, 2019. URL: https://doi.org/10.1145/3341712.
  35. Andrew M Pitts. Evaluation logic. In IV Higher Order Workshop, Banff 1990: Proceedings of the IV Higher Order Workshop, Banff, Alberta, Canada 10-14 September 1990, pages 162-189. Springer, 1991. URL: https://doi.org/10.1007/978-1-4471-3182-3_11.
  36. Andrew M Pitts. Tripos Theory in Retrospect. Mathematical structures in computer science, 12(3):265-279, 2002. URL: https://doi.org/10.1016/S1571-0661(04)00107-0.
  37. John Power. Premonoidal Categories as Categories with Algebraic Structure. Theoretical Computer Science, 278(1):303-321, 2002. Mathematical Foundations of Programming Semantics 1996. URL: https://doi.org/10.1016/S0304-3975(00)00340-6.
  38. John Power and Edmund Robinson. Premonoidal Categories and Notions of Computation. Mathematical structures in computer science, 7(5):453-468, 1997. URL: https://doi.org/10.1017/S0960129597002375.
  39. John Power and Hayo Thielecke. Environments, Continuation Semantics and Indexed Categories. In Martín Abadi and Takayasu Ito, editors, Theoretical Aspects of Computer Software, pages 391-414, Berlin, Heidelberg, 1997. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFb0014560.
  40. Edmund Robinson and Giuseppe Rosolini. Colimit Completions and the Effective Topos. Journal of Symbolic Logic, 55(2):678-699, 1990. URL: https://doi.org/10.2307/2274658.
  41. Walter Ferrer Santos, Jonas Frey, Mauricio Guillermo, Octavio Malherbe, and Alexandre Miquel. Ordered Combinatory Algebras and Realizability. Mathematical Structures in Computer Science, 27(3):428-458, 2017. URL: https://doi.org/10.1017/S0960129515000432.
  42. Samuel L. Speight. Groupoidal Realizability for Intensional Type Theory. Mathematical Structures in Computer Science, pages 1-34, 2024. URL: https://doi.org/10.1017/S0960129524000343.
  43. Thomas Streicher. Krivine’s Classical Realisability from a Categorical Perspective. Mathematical Structures in Computer Science, 23(6):1234-1256, 2013. URL: https://doi.org/10.1017/S0960129512000989.
  44. Jaap Van Oosten. Realizability: an Introduction to its Categorical Side, volume 152. Elsevier, Amsterdam, 2008. URL: https://doi.org/10.1017/S1079898600000858.
  45. Philip Wadler. Comprehending Monads. In Proceedings of the 1990 ACM Conference on LISP and Functional Programming, pages 61-78, 1990. URL: https://doi.org/10.1145/91556.91592.
  46. Philip Wadler. Monads for FunctionalDOI:10.1017/S0960129597002375 Programming. In International School on Advanced Functional Programming, pages 24-52. Springer, 1995. URL: https://doi.org/10.1007/3-540-59451-5_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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact