Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

What Monads Can and Cannot Do with a Few Extra Pages

Rasmus Ejlers Møgelberg, Maaike Zwart

TL;DR

This work systematically analyzes how the delay monad, both coinductive $D$ and guarded $D^{\kappa}$, can be combined with standard algebraic effects via distributive laws $T D \to D T$. It characterises when sequential versus parallel lifting yields valid distributive laws, showing that sequential lifting works for monads presented by algebraic theories with balanced equations, while parallel lifting often fails (notably for the finite powerset and finite distributions). The guarded-delay setting allows robust interaction with many effects and enables weak-bisimilarity-based remedies, yielding a Semi-Go result: distributive laws exist up to weak bisimilarity for theories with no drop equations. The paper also develops a formal framework in Clocked Cubical Type Theory to encode these constructions and proves that free-model monads commute with clock quantification, facilitating clock-irrelevant encodings of coinductive types. Overall, it delineates what monads can and cannot do with a bit of extra time, clarifying the algebraic structure required for compositional effects in type-theoretic settings.

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.

What Monads Can and Cannot Do with a Few Extra Pages

TL;DR

This work systematically analyzes how the delay monad, both coinductive and guarded , can be combined with standard algebraic effects via distributive laws . It characterises when sequential versus parallel lifting yields valid distributive laws, showing that sequential lifting works for monads presented by algebraic theories with balanced equations, while parallel lifting often fails (notably for the finite powerset and finite distributions). The guarded-delay setting allows robust interaction with many effects and enables weak-bisimilarity-based remedies, yielding a Semi-Go result: distributive laws exist up to weak bisimilarity for theories with no drop equations. The paper also develops a formal framework in Clocked Cubical Type Theory to encode these constructions and proves that free-model monads commute with clock quantification, facilitating clock-irrelevant encodings of coinductive types. Overall, it delineates what monads can and cannot do with a bit of extra time, clarifying the algebraic structure required for compositional effects in type-theoretic settings.

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.
Paper Structure (17 sections, 24 theorems, 110 equations, 2 figures)

This paper contains 17 sections, 24 theorems, 110 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Monads and Algebraic Theories
  3. Distributive Laws
  4. Guarded Recursion and the Delay Monad
  5. Algebraic Theories in Cubical Type Theory
  6. Multi-Clocked Guarded Recursion
  7. Guarded Recursive Types
  8. Encoding Coinductive Types
  9. Specific Combinations with Delay
  10. Parallel and Sequential Distribution of Operations
  11. Preservation of Equations
  12. Idempotent Equations
  13. Semi-Go Theorem: Up to Weak Bisimilarity
  14. Related Work
  15. Conclusion and Future Work
  16. ...and 2 more sections

Key Result

Theorem 2.11

Let $\mathcal{C}$ be a category, and $\langle S, \eta^S, \mu^S \rangle$ and $\langle T, \eta^T, \mu^T \rangle$ two monads on $\mathcal{C}$. If $\zeta: ST \rightarrow TS$ is a distributive law, then the functor $TS$ carries a monad structure with unit $\eta^T\eta^S$ and multiplication $\mu^T\mu^S \ci

Figures (2)

  • Figure 1: Selected typing rules for Clocked Cubical Type Theory CubicalCloTT. The telescope ${\mathsf{TimeLess}(\Gamma')}$ is composed of the timeless assumptions in $\Gamma$, i.e. interval variables and faces (as in Cubical Type Theory) as well as clock variables.
  • Figure 2: The principle of induction under clocks for $T(X)$. We omit the hypotheses concerning set truncation, which are standard CubicalCloTT. We assume given an algebraic signature and an $X : \forall\kappa . \mathsf{Set}$ both in context $\Gamma$. Note that the equalities are judgemental (denoted $\equiv$)

Theorems & Definitions (66)

  • Definition 2.1: Algebraic Theory
  • Example 2.2: Monoids
  • Example 2.3: Convex algebras
  • Definition 2.4: Category of Models
  • Example 2.5: Boom Hierarchy Monads Meertens1986
  • Example 2.6
  • Definition 2.7
  • Remark 2.8
  • Definition 2.9: Distributive Law
  • Example 2.10: Lists and Multisets
  • ...and 56 more