Document Open Access Logo

Lazy Intermediate Representations for Algebraic Effects

Authors Simon Castellan , Hugo Paquet

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.25.pdf
  • Filesize: 1.73 MB
  • 27 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
  • Theory of computation → Denotational semantics
  • Theory of computation → Probabilistic computation
Keywords
  • Categorical semantics
  • lazy evaluation
  • interpreter
  • probabilistic programming

Metrics

Abstract

A lazy program interpreter postpones computation until the result is actually needed. This is typically more efficient than an eager (or call-by-value) interpreter, but a concern is that the semantics is not generally preserved.
We propose a new semantic analysis of lazy evaluation that relies on a subtle combination of name generation and read-only state. Our perspective is that laziness arises from a hybrid evaluation strategy, in which only the name generation follows call-by-value. 
This semantic model suggests better intermediate representations of sum and product types in a lazy interpreter, along with equations that justify further optimizations. We illustrate this with an implementation in OCaml. Our motivation is practical: the origin of this work is a real-world application of discrete probabilistic programming, in which large algebraic data types cause significant performance issues with a call-by-value interpreter. Our lazy semantics justifies better optimized representations, and provides principled foundations for other methods involving laziness in probabilistic programming.

Cite As Get BibTex

Simon Castellan and Hugo Paquet. Lazy Intermediate Representations for Algebraic Effects. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 25:1-25:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.25

Author Details

Simon Castellan
  • Inria, Univ. Rennes, CNRS, IRISA, France
Hugo Paquet
  • Inria, École Normale Supérieure - PSL University, CNRS, Paris, France

Funding

We acknowledge support from the grant ANR Flores (ANR-23-SSAI-0001).

Acknowledgements

We thank Aurore Alcolei and Tom Hirschowitz for their deep involvement in this project, and for many helpful discussions. We are also grateful for conversations with John M. Li, Jack Czenszak, and Steven Holtzen: our paper shares many ideas with their work [Li et al., 2026], to appear at PLDI 2026; understanding their perspective has helped us improve the final version of this paper.

References

  1. Samson Abramsky and C-H Luke Ong. Full abstraction in the lazy lambda calculus. Information and Computation, 105(2):159-267, 1993. URL: https://doi.org/10.1006/inco.1993.1044.
  2. Zena M Ariola, John Maraist, Martin Odersky, Matthias Felleisen, and Philip Wadler. A call-by-need lambda calculus. In Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 233-246, 1995. URL: https://doi.org/10.1145/199448.199507.
  3. Jon Beck. Distributive laws. In B. Eckmann, editor, Seminar on Triples and Categorical Homology Theory, pages 119-140, Berlin, Heidelberg, 1969. Springer Berlin Heidelberg. Google Scholar
  4. Maddy Bowers, Alexander K. Lew, Joshua B. Tenenbaum, Armando Solar-Lezama, and Vikash K. Mansinghka. Stochastic lazy knowledge compilation for inference in discrete probabilistic programs. Proceedings of the ACM on Programming Languages, 9(PLDI):1863-1887, 2025. URL: https://doi.org/10.1145/3729325.
  5. Randal E Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys (CSUR), 24(3):293-318, 1992. URL: https://doi.org/10.1145/136035.136043.
  6. Marta Cavallo Bunge. Categories of set valued functors. University of Pennsylvania, 1966. Google Scholar
  7. Simon Castellan, Aurore Alcolei, Anne Atlan, Xavier Aubriot, Mathurin Bellot, Gurvan Cabot, Lysa Dahmani, Jos Käfer, Sophie Nadot, Sara Oort, Agnès Schermann-Legionnet, and Eric Tannier. Botascopia: a digital setup for generating low tech plant field guides. working paper or preprint, 2025. URL: https://hal.science/hal-05419216.
  8. Simon Castellan, Jos Käfer, and Eric Tannier. Back to the trees: Identifying plants with Human Intelligence. In LIMITS 2023 - Ninth Workshop on Computing within Limits, pages 1-11, Virtuel - Online, France, July 2023. LIMITS. URL: https://doi.org/10.21428/bf6fb269.265c52ce.
  9. Jack Czenszak, John M Li, and Steven Holtzen. Towards symbolic execution for probability and non-determinism, 2025. Google Scholar
  10. Ugo Dal Lago, Giulio Guerrieri, and Willem Heijltjes. Decomposing Probabilistic Lambda-Calculi. In FOSSACS 2020 - Foundations of Software Science and Computation Structures - 23rd International Conference, pages 136-156, Dublin, Ireland, April 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_8.
  11. Swaraj Dash, Younesse Kaddar, Hugo Paquet, and Sam Staton. Affine monads and lazy structures for bayesian programming, October 2022. URL: https://doi.org/10.5281/ZENODO.7150943.
  12. Marcelo P. Fiore and Alex K. Simpson. Lambda definability with sums via grothendieck logical relations. In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings, volume 1581 of Lecture Notes in Computer Science, pages 147-161. Springer, 1999. URL: https://doi.org/10.1007/3-540-48959-2_12.
  13. Steven Holtzen, Guy Van Den Broeck, and Todd Millstein. Artifact for scaling exact inference for discrete probabilistic programs. Zenodo, 2020. URL: https://doi.org/10.5281/ZENODO.4060132.
  14. Bart Jacobs. Semantics of weakening and contraction. Ann. Pure Appl. Log., 69(1):73-106, 1994. URL: https://doi.org/10.1016/0168-0072(94)90020-5.
  15. Bart Jacobs. Convexity, duality and effects. In IFIP International Conference on Theoretical Computer Science, pages 1-19. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15240-5_1.
  16. Younesse Kaddar and Sam Staton. A model of stochastic memoization and name generation in probabilistic programming: categorical semantics via monads on presheaf categories. Electronic Notes in Theoretical Informatics and Computer Science, 3, 2023. URL: https://doi.org/10.46298/entics.12291.
  17. Shin-ya Katsumata. A characterisation of lambda definability with sums via tt-closure operators. In Michael Kaminski and Simone Martini, editors, Computer Science Logic, 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, Bertinoro, Italy, September 16-19, 2008. Proceedings, volume 5213 of Lecture Notes in Computer Science, pages 278-292. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-87531-4_21.
  18. G. A. Kavvos. Adequacy for algebraic effects revisited. Proceedings of the ACM on Programming Languages, 9(OOPSLA1):927-955, April 2025. URL: https://doi.org/10.1145/3720457.
  19. Oleg Kiselyov and Chung-chieh Shan. Embedded probabilistic programming. In IFIP Working Conference on Domain-Specific Languages, pages 360-384. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03034-5_17.
  20. Anders Kock. Bilinearity and cartesian-closed monads. Mathematica Scandinavica, 29(2):161-174, 1971. URL: http://www.jstor.org/stable/24491025.
  21. Daphne Koller, David McAllester, and Avi Pfeffer. Effective bayesian inference for stochastic programs. In AAAI/IAAI, pages 740-747, 1997. URL: http://www.aaai.org/Library/AAAI/1997/aaai97-115.php.
  22. John Launchbury. A natural semantics for lazy evaluation. In Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 144-154, 1993. URL: https://doi.org/10.1145/158511.158618.
  23. F William Lawvere. Functorial semantics of algebraic theories. Proceedings of the National Academy of Sciences, 50(5):869-872, 1963. Google Scholar
  24. F William Lawvere. Some algebraic problems in the context of functorial semantics of algebraic theories. In Reports of the Midwest Category Seminar II, pages 41-61, 1968. Google Scholar
  25. Tom Leinster. Higher operads, higher categories. Number 298 in London Mathematical Society Lecture Note Series. Cambridge University Press, 2004. Google Scholar
  26. Paul Blain Levy. Call-By-Push-Value. Springer Netherlands, Dordrecht, 2003. URL: https://doi.org/10.1007/978-94-007-0954-6.
  27. Paul Blain Levy. Call-by-push-value: Decomposing call-by-value and call-by-name. Higher-Order and Symbolic Computation, 19(4):377-414, December 2006. URL: https://doi.org/10.1007/s10990-006-0480-6.
  28. PaulBlain 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.
  29. John Li, Jack Czenszak, and Steven Holtzen. Categorical semantics of probabilistic symbolic execution. In Proceedings of the 47th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '26), Boulder, CO, USA, 2026. ACM. URL: https://doi.org/10.1145/3808343.
  30. Sam Lindley and Ian Stark. Reducibility and ⊤⊤-lifting for computation types. In Paweł Urzyczyn, editor, Typed Lambda Calculi and Applications, pages 262-277, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/11417170_20.
  31. Fred EJ Linton. Coequalizers in categories of algebras. In Seminar on Triples and Categorical Homology Theory: ETH 1966/67, pages 75-90. Springer, 2006. Google Scholar
  32. Saunders Mac Lane. Categories for the working mathematician, volume 5. Springer Science & Business Media, 1998. Google Scholar
  33. Dylan McDermott and Alan Mycroft. Extended call-by-push-value: Reasoning about effectful programs and evaluation order. In ESOP, pages 235-262, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_9.
  34. Dylan McDermott and Alan Mycroft. Galois connecting call-by-value and call-by-name. Logical Methods in Computer Science, 20, 2024. URL: https://doi.org/10.46298/lmcs-20(1:13)2024.
  35. 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.
  36. Cameron Moy, Jack Czenszak, John M. Li, Brianna Marshall, and Steven Holtzen. Roulette: A language for expressive, exact, and efficient discrete probabilistic programming. Proc. ACM Program. Lang., 9(PLDI), June 2025. URL: https://doi.org/10.1145/3729334.
  37. Chris Okasaki, Peter Lee, and David Tarditi. Call-by-need and continuation-passing style. Lisp and Symbolic Computation, 7(1):57-81, 1994. Google Scholar
  38. Peter W O’Hearn and Robert D Tennent. Semantics of local variables. Applications of categories in computer science, 177:217-238, 1992. Google Scholar
  39. Andrew M Pitts and Ian DB Stark. Observable properties of higher order functions that dynamically create local names, or: What’s new? In International Symposium on Mathematical Foundations of Computer Science, pages 122-141. Springer, 1993. URL: https://doi.org/10.1007/3-540-57182-5_8.
  40. Gordon Plotkin and John Power. Notions of computation determine monads. In International Conference on Foundations of Software Science and Computation Structures, pages 342-356. Springer, 2002. URL: https://doi.org/10.1007/3-540-45931-6_24.
  41. Gordon Plotkin and John Power. Computational effects and operations: An overview. Electronic Notes in Theoretical Computer Science, 73:149-163, October 2004. URL: https://doi.org/10.1016/j.entcs.2004.08.008.
  42. Gordon D Plotkin and Matija Pretnar. Handling algebraic effects. Logical Methods in Computer Science, Volume 9, Issue 4, December 2013. URL: https://doi.org/10.2168/lmcs-9(4:23)2013.
  43. John C Reynolds. Definitional interpreters for higher-order programming languages. In Proceedings of the ACM annual conference-Volume 2, pages 717-740, 1972. URL: https://doi.org/10.1145/800194.805852.
  44. Glynn Winskel. The formal semantics of programming languages: an introduction. MIT press, 1993. Google Scholar
  45. Pierre Évariste Dagand, Lionel Rieg, and Gabriel Scherer. Dependent pearl: Normalization by realizability, 2020. URL: https://doi.org/10.48550/arXiv.1908.09123.
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