What Monads Can and Cannot Do with a Few Extra Pages

Basic Information

• Paper ID: 2311.15919
• Title: What Monads Can and Cannot Do with a Few Extra Pages
• Authors: Rasmus Ejlers Møgelberg, Maaike Zwart
• Classification: cs.LO (Logic in Computer Science)
• Publication Venue/Date: Logical Methods in Computer Science, Volume 21, Issue 4, 2025
• Paper Link: https://arxiv.org/abs/2311.15919

Abstract

The delay monad provides a method for introducing general recursion in type theory. To write programs directly in type theory that use a wide range of computational effects, we need to combine the delay monad with monads for these effects. This paper presents the first systematic study of such combinations. The article investigates both the coinductive delay monad and its guarded recursive variant, providing concrete examples of combining these monads with well-known computational effects. Additionally, it provides general theorems characterizing which algebraic effects distribute over the delay monad and which do not. Finally, some impossible cases are rescued by considering distributive laws under weak bisimulation.

Research Background and Motivation

1. Problem to be Solved: Martin-Löf type theory requires all programs to terminate to preserve the correctness of logical interpretation, yet practical programming requires general recursion. The delay monad addresses this through encapsulating recursion, but lacks a theory for systematically combining the delay monad with other computational effects.
2. Problem Significance: Modern functional programming languages must handle multiple computational effects (exceptions, state, nondeterminism, etc.). Direct programming and reasoning about these effects in type theory requires a mathematical theory describing the interaction between the delay monad and other monads.
3. Limitations of Existing Approaches:
   • Lack of systematic study of combining the delay monad with other monads
   • Related results from domain theory are too complex for type-theoretic settings
   • Certain combinations (e.g., finite powerset monad) are known to be infeasible, but lack general theory
   • No principled method to determine which combinations are possible
4. Research Motivation: Establish a complete mathematical theory of combining the delay monad with other computational effects, providing theoretical foundations for advanced functional programming in type theory.

Core Contributions

1. Systematic Study Framework: First systematic investigation of combining the delay monad with other monads, covering both coinductive and guarded recursive variants.
2. Concrete Combination Examples: Demonstrates concrete ways to combine the delay monad with standard computational effects (exceptions, reader, global state, continuations, choice).
3. General Theorems on Distributive Laws:
   • Proves that sequential distribution works for algebraic monads with balanced equations
   • Proves that monads with commutative idempotent operations admit no distributive law
   • Establishes correspondence between equation types and existence of distributive laws
4. Weak Bisimulation Theory: By working in the category of sets, proves that distributive laws can be constructed for algebraic monads without discarding equations under weak bisimulation.
5. Formal Verification: Partially formalizes results in Agda, providing verifiable implementations.

Detailed Methodology

Task Definition

Study the existence of distributive laws TD → DT, where T is an arbitrary monad and D is the delay monad. A distributive law distributes the operations of T over computational steps, giving the composite DT a monad structure.

Theoretical Framework

1. Two Forms of the Delay Monad

• Guarded Recursive Delay Monad D^κ: Defined as D^κX ≃ X + ▷^κ(D^κX)
• Coinductive Delay Monad D: Defined as DX ≝ ∀κ.D^κX

2. Two Strategies for Operation Lifting

Parallel Lifting (Definition 5.1):

op^par(now^κ x₁, ..., now^κ xₙ) = now^κ(op(x₁, ..., xₙ))
op^par(x₁, ..., xₙ) = step^κ(λα.op^par(x'₁, ..., x'ₙ))

Sequential Lifting (Definition 5.2):

op^seq(now^κ x₁, ..., now^κ xₙ) = now^κ(op(x₁, ..., xₙ))  
op^seq(now^κ x₁, ..., step^κ xᵢ, ..., xₙ) = step^κ(λα.op^seq(now^κ x₁, ..., xᵢ[α], ..., xₙ))

3. Equation Classification System (Definition 2.7)

• Linear Equations: Each variable appears exactly once on both sides
• Balanced Equations: Each variable appears the same number of times on both sides
• Duplicating Equations: Some variable appears ≥2 times
• Discarding Equations: Variable sets differ between sides

Technical Innovations

1. Guarded Recursive Encoding: Uses multi-clock guarded recursion to encode coinductive types as ∀κ.D^κX, avoiding continuity requirements.
2. Distributive Law Equivalence: Establishes a bijection between distributive laws and monad liftings in the Eilenberg-Moore category (Theorem 2.12).
3. Equation-Driven Analysis: Predicts existence of distributive laws through equation types of algebraic theories, providing a systematic analytical framework.
4. Weak Bisimulation Category: Works in the category of sets to handle quotient structures, overcoming technical difficulties of directly quotienting the delay monad.

Experimental Setup

Theoretical Verification Methods

1. Constructive Proofs: Explicit constructions for existence results
2. Counterexample Construction: Concrete counterexamples for impossibility results
3. Guarded Recursion: Uses guarded recursion for inductive proofs
4. Formal Verification: Implements partial results in Agda

Concrete Case Analysis

• Boom Hierarchy Monads: Binary trees, lists, multisets, powerset monad
• Probability Distribution Monad: Finite probability distribution monad
• Computational Effect Monads: Exception, reader, state, continuation, choice monads

Experimental Results

Main Results

1. Successful Sequential Distribution Cases (Theorem 5.7)

• Scope: Algebraic theories with only balanced equations
• Success Cases: Binary tree monad, list monad, multiset monad
• Mathematical Proof: Sequential lifting preserves balanced equations (Proposition 5.6)

2. Impossibility Results (Theorem 6.6)

• Core Theorem: Monads with commutative idempotent binary operations admit no distributive law TD^κ → D^κT
• Concrete Counterexamples:
  • Finite powerset monad (Proposition 6.3)
  • Finite probability distribution monad (Proposition 6.4)
• Technical Key: Constructs contradiction via guarded recursion, exploiting step-counting errors

3. Rescue via Weak Bisimulation (Theorem 7.7)

• Applicable Conditions: Algebraic theories without discarding equations
• Technical Means: Defines weak bisimulation relation ∼_R on the category of sets
• Theoretical Significance: Proves parallel lifting is always feasible in the weak sense

Ablation Studies

Impact of Equation Types

1. Linear Equations: Always permit distributive laws (known result)
2. Balanced Equations: Permit sequential distribution
3. Idempotent Equations: Prevent all distributive laws
4. Discarding Equations: Prevent parallel distribution, but feasible under weak bisimulation

Parallel vs. Sequential Lifting

• Parallel Lifting: Does not define distributive law (Theorem 5.5), but feasible under weak bisimulation
• Sequential Lifting: Defines distributive law for balanced equations, but inapplicable to idempotent operations

Case Studies

Examples of Successful Combinations

-- State monad with delay monad: (D^κ(S × −))^S
lookup^DS : ((D^κ(S × X))^S)^S → D^κ(S × X)^S
update^DS : D^κ(S × X)^S → (D^κ(S × X))^S
step^DS : ▷^κ((D^κ(S × X))^S) → (D^κ(S × X))^S

Technical Analysis of Failed Cases

The core of the powerset monad counterexample lies in:

step(x) ∪ step(x) = step(x ∪ x) = step(x) ≠ step²(x)

This leads to inconsistent step counting, violating the multiplicative axiom of distributive laws.

Related Work

Development Trajectory of the Field

1. Origins of Delay Monad: Capretta (2005) introduces coinductive delay monad
2. Guarded Recursion: Nakano (2000)'s fixed-point modality, Atkey & McBride (2013)'s encoding techniques
3. Monad Composition: Beck (1969)'s distributive law theory, Manes & Mulry (2007)'s systematic study
4. Interaction Trees: Xia et al. (2019)'s practical framework

Unique Contributions of This Paper

1. First Systematic Study: Combination of delay monad with other effects
2. Advantages of Guarded Recursion: Technical advantages over coinductive version
3. Equation-Driven Method: Predicts distributive law existence through algebraic equations
4. Weak Bisimulation Theory: Novel method to rescue impossible cases

Conclusions and Discussion

Main Conclusions

1. Classification Theorem: Establishes complete correspondence between equation types and distributive law existence
2. Construction Methods: Provides concrete distributive law construction (sequential lifting) and counterexample construction
3. Theoretical Boundaries: Clarifies which cases are possible and which are impossible
4. Practical Value: Provides theoretical foundations for effect programming in type theory

Limitations

1. Finite Arity: Only considers finite-arity operations; countable choice requires further study
2. Weak Bisimulation Complexity: Requires working in the category of sets, adding technical complexity
3. CCTT Dependency: Results proven in Clocked Cubical Type Theory; lifting to Set requires additional work

Future Directions

1. Countable Operations: Extend to countable-arity operations such as countable nondeterministic choice
2. Higher-Order Effects: Study more complex computational effects
3. Practical Libraries: Develop practical effect programming libraries based on theoretical results
4. Other Type Theories: Verify results in other type-theoretic settings

In-Depth Evaluation

Strengths

Technical Innovation

1. Theoretical Completeness: Establishes complete theoretical framework for delay monad composition
2. Novel Methods: Guarded recursion approach is simpler than traditional domain-theoretic methods
3. Precise Classification: Precisely predicts distributive law existence through equation types

Experimental Sufficiency

1. Rich Case Studies: Covers major computational effect monads
2. Rigorous Proofs: Both constructive proofs and counterexample constructions are rigorous
3. Formalization: Partial results formally verified in Agda

Result Convincingness

1. Theoretical Depth: Not only provides results but explains underlying mathematical reasons
2. Practical Value: Provides direct guidance for type-theoretic programming
3. Generality: Results apply to broad categories of algebraic theories

Weaknesses

Method Limitations

1. Technical Dependency: Heavily relies on special features of CCTT
2. Scope Restrictions: Only handles finite-arity operations
3. Complexity: Weak bisimulation method adds unnecessary complexity

Practical Issues

1. Theoretical Focus: Distance from practical programming applications
2. Tool Support: Lacks practical tools based on the theory
3. Learning Curve: Requires deep background in category theory and type theory

Impact

Academic Contributions

1. Fills Gap: First systematic study of an important but overlooked problem
2. Methodology: Provides analytical methods for similar problems
3. Theoretical Foundation: Establishes foundation for future effect programming research

Practical Value

1. Programming Guidance: Provides theoretical guidance for functional language design
2. Verification Tools: Provides mathematical foundation for program verification
3. Educational Value: Demonstrates application of category theory in computer science

Applicable Scenarios

1. Type Theory Research: Research requiring handling computational effects in type theory
2. Functional Programming: Designing functional languages supporting multiple effects
3. Program Verification: Formal verification of programs with effects
4. Theoretical Computer Science: Research on theoretical properties of computational effects

References

This paper cites 69 important references spanning multiple domains including type theory, category theory, and computational effects, particularly foundational works such as Beck (1969)'s distributive law theory, Capretta (2005)'s delay monad, and Nakano (2000)'s guarded recursion.