2025-11-18T09:28:13.006832

What Monads Can and Cannot Do with a Few Extra Pages

Møgelberg, 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.
academic

What Monads Can and Cannot Do with a Few Extra Pages

基本信息

  • 论文ID: 2311.15919
  • 标题: What Monads Can and Cannot Do with a Few Extra Pages
  • 作者: Rasmus Ejlers Møgelberg, Maaike Zwart
  • 分类: cs.LO (Logic in Computer Science)
  • 发表时间/会议: Logical Methods in Computer Science, Volume 21, Issue 4, 2025
  • 论文链接: https://arxiv.org/abs/2311.15919

摘要

延迟单子(delay monad)提供了一种在类型理论中引入一般递归的方法。为了在类型理论中直接编写使用广泛计算效应的程序，我们需要将延迟单子与这些效应的单子结合起来。本文首次系统性地研究了这种结合。文章研究了余归纳延迟单子及其保护递归变体，给出了将这些单子与知名计算效应结合的具体例子。同时提供了一般性定理，说明哪些代数效应在延迟单子上分布，哪些不分布。最后，通过考虑弱双模拟下的分布律来挽救一些不可能的情况。

研究背景与动机

  1. 要解决的问题: Martin-Löf类型理论要求所有程序终止以保持逻辑解释的正确性，但实际编程中需要一般递归。延迟单子通过封装递归解决了这个问题，但缺乏将延迟单子与其他计算效应系统结合的理论。
  2. 问题的重要性: 现代函数式编程语言需要处理多种计算效应(异常、状态、非确定性等)。在类型理论中直接编程和推理这些效应需要一个数学理论来描述延迟单子与其他单子的交互。
  3. 现有方法的局限性:
    • 缺乏延迟单子与其他单子结合的系统性研究
    • 域理论中的相关结果过于复杂，不适用于类型理论设置
    • 已知某些结合(如有限幂集单子)不可行，但缺乏一般性理论
  4. 研究动机: 建立延迟单子与其他计算效应结合的完整数学理论，为在类型理论中进行高级函数式编程提供理论基础。

核心贡献

  1. 系统性研究框架: 首次对延迟单子与其他单子的结合进行系统性研究，涵盖余归纳和保护递归两种变体。
  2. 具体结合示例: 展示了延迟单子与标准计算效应(异常、读取器、全局状态、延续、选择)的具体结合方式。
  3. 分布律的一般性定理:
    • 证明了顺序分布对平衡方程的代数单子成立
    • 证明了交换幂等操作的单子不存在分布律
    • 建立了方程类型与分布律存在性的对应关系
  4. 弱双模拟理论: 通过在集合范畴上工作，证明了在弱双模拟意义下可以为无丢弃方程的代数单子构造分布律。
  5. 形式化验证: 部分结果在Agda中形式化，提供了可验证的实现。

方法详解

任务定义

研究分布律 TD → DT 的存在性，其中 T 是任意单子，D 是延迟单子。分布律将 T 的操作分布到计算步骤上，使复合 DT 具有单子结构。

理论框架

1. 延迟单子的两种形式

  • 保护递归延迟单子 D^κ: 定义为 D^κX ≃ X + ▷^κ(D^κX)
  • 余归纳延迟单子 D: 定义为 DX ≝ ∀κ.D^κX

2. 操作提升的两种策略

并行提升 (Definition 5.1):

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

顺序提升 (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. 方程分类系统 (Definition 2.7)

  • 线性方程: 每个变量在等式两边恰好出现一次
  • 平衡方程: 每个变量在等式两边出现次数相同
  • 复制方程: 存在变量出现≥2次
  • 丢弃方程: 等式两边变量集合不同

技术创新点

  1. 保护递归编码: 利用多时钟保护递归将余归纳类型编码为 ∀κ.D^κX，避免了连续性要求。
  2. 分布律等价性: 建立了分布律与Eilenberg-Moore范畴中单子提升的双射对应(Theorem 2.12)。
  3. 方程驱动分析: 通过代数理论的方程类型预测分布律的存在性，提供了系统性的分析框架。
  4. 弱双模拟范畴: 在集合范畴上工作以处理商结构，克服了直接商化延迟单子的技术困难。

实验设置

理论验证方法

  1. 构造性证明: 对存在性结果给出显式构造
  2. 反例构造: 对不可能性结果构造具体反例
  3. 保护递归: 使用保护递归进行归纳证明
  4. 形式化验证: 在Agda中实现部分结果

具体案例分析

  • Boom层次单子: 二元树、列表、多重集合、幂集单子
  • 概率分布单子: 有限概率分布单子
  • 计算效应单子: 异常、读取器、状态、延续、选择单子

实验结果

主要结果

1. 顺序分布律的成功案例 (Theorem 5.7)

  • 适用范围: 仅含平衡方程的代数理论
  • 成功案例: 二元树单子、列表单子、多重集合单子
  • 数学证明: 顺序提升保持平衡方程 (Proposition 5.6)

2. 不可能性结果 (Theorem 6.6)

  • 核心定理: 具有交换幂等二元操作的单子不存在分布律 TD^κ → D^κT
  • 具体反例:
    • 有限幂集单子 (Proposition 6.3)
    • 有限概率分布单子 (Proposition 6.4)
  • 技术关键: 通过保护递归构造矛盾，利用步数计算错误

3. 弱双模拟下的挽救 (Theorem 7.7)

  • 适用条件: 无丢弃方程的代数理论
  • 技术手段: 在集合范畴上定义弱双模拟关系 ∼_R
  • 理论意义: 证明了并行提升在弱意义下总是可行的

消融实验

方程类型的影响

  1. 线性方程: 总是允许分布律(已知结果)
  2. 平衡方程: 允许顺序分布律
  3. 幂等方程: 阻止所有分布律
  4. 丢弃方程: 阻止并行分布律，但在弱双模拟下可行

并行vs顺序提升

  • 并行提升: 不定义分布律(Theorem 5.5)，但在弱双模拟下可行
  • 顺序提升: 对平衡方程定义分布律，但不适用于幂等操作

案例分析

成功结合的例子

-- 状态单子与延迟单子: (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

失败案例的技术分析

幂集单子的反例核心在于：

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

这导致步数计算不一致，违反了分布律的乘法公理。

相关工作

领域发展脉络

  1. 延迟单子起源: Capretta (2005) 引入余归纳延迟单子
  2. 保护递归: Nakano (2000) 的固定点模态，Atkey & McBride (2013) 的编码技术
  3. 单子组合: Beck (1969) 的分布律理论，Manes & Mulry (2007) 的系统研究
  4. 交互树: Xia et al. (2019) 的实用框架

本文的独特贡献

  1. 首次系统研究: 延迟单子与其他效应的结合
  2. 保护递归优势: 相比余归纳版本的技术优势
  3. 方程驱动方法: 通过代数方程预测分布律存在性
  4. 弱双模拟理论: 挽救不可能情况的新方法

结论与讨论

主要结论

  1. 分类定理: 建立了方程类型与分布律存在性的完整对应关系
  2. 构造方法: 提供了具体的分布律构造(顺序提升)和反例构造
  3. 理论边界: 明确了哪些情况可能，哪些不可能
  4. 实用价值: 为类型理论中的效应编程提供理论基础

局限性

  1. 有限元数: 仅考虑有限元数操作，可数选择等需要进一步研究
  2. 弱双模拟复杂性: 需要在集合范畴中工作，增加了技术复杂度
  3. CCTT依赖: 结果在Clocked Cubical Type Theory中证明，向Set的提升需要额外工作

未来方向

  1. 可数操作: 扩展到可数元数操作如可数非确定性选择
  2. 高阶效应: 研究更复杂的计算效应
  3. 实用库: 基于理论结果开发实用的效应编程库
  4. 其他类型理论: 在其他类型理论设置中验证结果

深度评价

优点

技术创新性

  1. 理论完整性: 建立了延迟单子组合的完整理论框架
  2. 方法新颖: 保护递归方法相比传统域理论方法更简洁
  3. 分类精确: 通过方程类型精确预测分布律存在性

实验充分性

  1. 案例丰富: 涵盖了主要的计算效应单子
  2. 证明严格: 构造性证明和反例构造都很严格
  3. 形式化: 部分结果在Agda中形式化验证

结果说服力

  1. 理论深度: 不仅给出结果，还解释了背后的数学原因
  2. 实用价值: 为类型理论编程提供直接指导
  3. 一般性: 结果适用于广泛的代数理论类别

不足

方法局限性

  1. 技术依赖: 重度依赖CCTT的特殊特性
  2. 范围限制: 仅处理有限元数操作
  3. 复杂度: 弱双模拟方法增加了不必要的复杂性

实用性问题

  1. 理论性强: 距离实际编程应用还有距离
  2. 工具支持: 缺乏基于理论的实用工具
  3. 学习曲线: 需要深厚的范畴论和类型理论背景

影响力

学术贡献

  1. 填补空白: 首次系统研究重要但被忽视的问题
  2. 方法论: 为类似问题提供了分析方法
  3. 理论基础: 为未来的效应编程研究奠定基础

实用价值

  1. 编程指导: 为函数式编程语言设计提供理论指导
  2. 验证工具: 为程序验证提供数学基础
  3. 教育价值: 展示了范畴论在计算机科学中的应用

适用场景

  1. 类型理论研究: 需要在类型理论中处理计算效应的研究
  2. 函数式编程: 设计支持多种效应的函数式语言
  3. 程序验证: 需要对带效应程序进行形式验证的场景
  4. 理论计算机科学: 研究计算效应的理论性质

参考文献

本文引用了69篇重要文献，涵盖了类型理论、范畴论、计算效应等多个领域的经典工作，特别是Beck (1969)的分布律理论、Capretta (2005)的延迟单子、以及Nakano (2000)的保护递归等奠基性工作。