Rasmus Ejlers Møgelberg ; Maaike Zwart - What Monads Can and Cannot Do with a Few Extra Pages

lmcs:14660 - Logical Methods in Computer Science, October 8, 2025, Volume 21, Issue 4 - https://doi.org/10.46298/lmcs-21(4:5)2025
What Monads Can and Cannot Do with a Few Extra PagesArticle

Authors: Rasmus Ejlers Møgelberg ; Maaike Zwart

    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.


    Volume: Volume 21, Issue 4
    Published on: October 8, 2025
    Accepted on: May 12, 2025
    Submitted on: November 4, 2024
    Keywords: Logic in Computer Science

    Consultation statistics

    This page has been seen 439 times.
    This article's PDF has been downloaded 372 times.