Document Open Access Logo

What Monads Can and Cannot Do with a Bit of Extra Time

Authors Rasmus Ejlers Møgelberg , Maaike Annebet Zwart

PDF
Thumbnail PDF

File

LIPIcs.CSL.2024.39.pdf
  • Filesize: 0.8 MB
  • 18 pages

Document Identifiers

Author Details

Rasmus Ejlers Møgelberg
  • IT University of Copenhagen, Denmark
Maaike Annebet Zwart
  • IT University of Copenhagen, Denmark

Funding

Independent Research Fund Denmark, grant number 2032-00134B.

Cite AsGet BibTex

Rasmus Ejlers Møgelberg and Maaike Annebet Zwart. What Monads Can and Cannot Do with a Bit of Extra Time. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 39:1-39:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CSL.2024.39

Abstract

The delay monad provides a way to introduce general recursion in type theory. To write programs that use a wide range of computational effects directly in type theory, we need to combine the delay monad with the monads of these effects. Here we present a first systematic study of such combinations. We study both the coinductive delay monad and its guarded recursive cousin, giving concrete examples of combining these with well-known computational effects. We also provide general theorems stating which algebraic effects distribute over the delay monad, and which do not. Lastly, we salvage some of the impossible cases by considering distributive laws up to weak bisimilarity.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program semantics
  • Theory of computation → Type structures
Keywords
  • Delay Monad
  • Monad Compositions
  • Distributive Laws
  • Guarded Recursion
  • Type Theory

Metrics

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

Related Versions

Supplementary Materials

References

  1. Thorsten Altenkirch, Nils Anders Danielsson, and Nicolai Kraus. Partiality, revisited. In International Conference on Foundations of Software Science and Computation Structures, pages 534-549. Springer, 2017. Google Scholar
  2. Robert Atkey and Conor McBride. Productive coprogramming with guarded recursion. ACM SIGPLAN Notices, 48(9):197-208, 2013. Google Scholar
  3. Patrick Bahr., Hans Bugge Grathwohl, and Rasmus Ejlers Møgelberg. The clocks are ticking: No more delays! In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12. IEEE, 2017. Google Scholar
  4. Patrick Bahr and Graham Hutton. Monadic compiler calculation (functional pearl). Proc. ACM Program. Lang., 6(ICFP), August 2022. URL: https://doi.org/10.1145/3547624.
  5. Magnus Baunsgaard Kristensen, Rasmus Ejlers Mogelberg, and Andrea Vezzosi. Greatest hits: Higher inductive types in coinductive definitions via induction under clocks. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 1-13, 2022. Google Scholar
  6. Jon Beck. Distributive laws. In B. Eckmann, editor, Seminar on Triples and Categorical Homology Theory, pages 119-140. Springer Berlin Heidelberg, 1969. Google Scholar
  7. Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, and Kristian Støvring. First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science, 8(4), 2012. Google Scholar
  8. Venanzio Capretta. General recursion via coinductive types. Logical Methods in Computer Science, 1, 2005. Google Scholar
  9. Evan Cavallo and Robert Harper. Higher inductive types in cubical computational type theory. Proceedings of the ACM on Programming Languages, 3(POPL):1-27, 2019. Google Scholar
  10. James Chapman, Tarmo Uustalu, and Niccolò Veltri. Quotienting the delay monad by weak bisimilarity. Mathematical Structures in Computer Science, 29(1):67-92, 2019. Google Scholar
  11. Ranald Clouston. Fitch-style modal lambda calculi. In International Conference on Foundations of Software Science and Computation Structures, pages 258-275. Springer, 2018. Google Scholar
  12. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical type theory: A constructive interpretation of the univalence axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2018. Google Scholar
  13. Fredrik Dahlqvist, Louis Parlant, and Alexandra Silva. Layer by layer - combining monads. In Theoretical Aspects of Computing - ICTAC 2018 - 15th International Colloquium, Stellenbosch, South Africa, October 16-19, 2018, Proceedings, pages 153-172, 2018. URL: https://doi.org/10.1007/978-3-030-02508-3_9.
  14. Nils Anders Danielsson. Operational semantics using the partiality monad. SIGPLAN Not., 47(9):127-138, September 2012. URL: https://doi.org/10.1145/2398856.2364546.
  15. Martín Escardó and Paulo Oliva. Selection functions, bar recursion and backward induction. Mathematical Structures in Computer Science, 20(2):127-168, 2010. URL: https://doi.org/10.1017/S0960129509990351.
  16. ND Gautam. The validity of equations of complex algebras. Archiv für mathematische Logik und Grundlagenforschung, 3(3):117-124, 1957. Google Scholar
  17. Daniel Gratzer, GA Kavvos, Andreas Nuyts, and Lars Birkedal. Multimodal dependent type theory. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 492-506, 2020. Google Scholar
  18. Jules Hedges. Monad transformers for backtracking search. In Paul Levy and Neel Krishnaswami, editors, Proceedings 5th Workshop on Mathematically Structured Functional Programming, Grenoble, France, 12 April 2014, volume 153 of Electronic Proceedings in Theoretical Computer Science, pages 31-50. Open Publishing Association, 2014. URL: https://doi.org/10.4204/EPTCS.153.3.
  19. Martin Hyland, Gordon Plotkin, and John Power. Combining effects: Sum and tensor. Theoretical Computer Science, 357(1):70-99, 2006. URL: https://doi.org/10.1016/j.tcs.2006.03.013.
  20. Martin Hyland and John Power. Discrete lawvere theories and computational effects. Theoretical Computer Science, 366(1-2):144-162, 2006. Google Scholar
  21. Bartek Klin and Julian Salamanca. Iterated covariant powerset is not a monad. In Proceedings 34th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2018, 2018. Google Scholar
  22. Anders Kock. Monads on symmetric monoidal closed categories. Archiv der Mathematik, 21(1):1-10, 1970. Google Scholar
  23. F. William Lawvere. Functorial semantics of algebraic theories. Proceedings of the National Academy of Sciences of the United States of America, 50(5):869-872, 1963. Google Scholar
  24. Fred EJ Linton. Some aspects of equational categories. In Proceedings of the Conference on Categorical Algebra, pages 84-94. Springer, 1966. Google Scholar
  25. Ernie Manes. Algebraic theories, volume 26. Springer, 1976. Google Scholar
  26. Ernie Manes and Philip Mulry. Monad compositions I: general constructions and recursive distributive laws. Theory and Applications of Categories, 18:172-208, April 2007. Google Scholar
  27. Ernie Manes and Philip Mulry. Monad compositions II: Kleisli strength. Mathematical Structures in Computer Science, 18(3):613-643, 2008. URL: https://doi.org/10.1017/S0960129508006695.
  28. Bassel Mannaa, Rasmus Ejlers Møgelberg, and Niccolò Veltri. Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory. Logical Methods in Computer Science, 16, 2020. Google Scholar
  29. Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984. Google Scholar
  30. Lambert Meertens. Algorithmics, towards programming as a mathematical activity. In J.W. De Bakker, M. Hazewinkel, and J.K. Lenstra, editors, Mathematics and Computer Science: Proceedings of the CWI Symposium, November 1983, CWI monographs, pages 289-334. North-Holland, 1986. Google Scholar
  31. Rasmus E Møgelberg and Marco Paviotti. Denotational semantics of recursive types in synthetic guarded domain theory. Mathematical Structures in Computer Science, 29(3):465-510, 2019. Google Scholar
  32. Rasmus Ejlers Møgelberg and Andrea Vezzosi. Two guarded recursive powerdomains for applicative simulation. In Ana Sokolova, editor, Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021, Hybrid: Salzburg, Austria and Online, 30th August - 2nd September, 2021, volume 351 of EPTCS, pages 200-217, 2021. URL: https://doi.org/10.4204/EPTCS.351.13.
  33. Hiroshi Nakano. A modality for recursion. In Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science, pages 255-266. IEEE, 2000. Google Scholar
  34. Louis Parlant. Monad Composition via Preservation of Algebras. PhD thesis, UCL (University College London), 2020. Google Scholar
  35. Louis Parlant, Jurriaan Rot, Alexandra Silva, and Bas Westerbaan. Preservation of equations by monoidal monads. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2020. Google Scholar
  36. Marco Paviotti, Rasmus Ejlers Møgelberg, and Lars Birkedal. A model of PCF in guarded type theory. Electronic Notes in Theoretical Computer Science, 319:333-349, 2015. Google Scholar
  37. 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. Google Scholar
  38. Jonathan Sterling, Daniel Gratzer, and Lars Birkedal. Denotational semantics of general store and polymorphism. Unpublished manuscript, July 2022. Google Scholar
  39. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  40. Daniele Varacca and Glynn Winskel. Distributing probability over non-determinism. Mathematical Structures in Computer Science, 16(1):87-113, 2006. Google Scholar
  41. Niccolò Veltri and Niels F. W. Voorneveld. Inductive and coinductive predicate liftings for effectful programs. In Ana Sokolova, editor, Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021, Hybrid: Salzburg, Austria and Online, 30th August - 2nd September, 2021, volume 351 of EPTCS, pages 260-277, 2021. URL: https://doi.org/10.4204/EPTCS.351.16.
  42. Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: Representing recursive and impure programs in Coq. Proc. ACM Program. Lang., 4(POPL), December 2019. URL: https://doi.org/10.1145/3371119.
  43. Maaike Zwart and Dan Marsden. No-go theorems for distributive laws. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LiCS), pages 1-13, 2019. URL: https://doi.org/10.1109/LICS.2019.8785707.
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