在近日举行的2025年ACM国际函数式编程大会（ICFP 2025）上，北京大学计算机学院程序设计语言研究室的研究工作《Effectful Lenses: There and Back with Different Monads》荣获杰出论文奖（Distinguished Paper Award）。

ICFP (International Conference on Functional Programming) 由ACM SIGPLAN主办，是程序语言理论与函数式编程领域最高水平的国际学术会议之一，享有极高的学术声誉。该会议始于1996年，长期以来一直是推动函数式编程范式发展的核心学术论坛。

论文的第一作者为北京大学计算机学院博士生谢睿峰，其他作者包括导师胡振江教授和比利时荷语鲁汶大学的联合导师Tom Schrijvers教授。

双向变换描述在不同数据之间的同步，monad是描述纯函数式程序的副作用的模式，已有的双向变换理论不支持在程序的两个方向都使用不同monad描述的副作用。获奖论文针对这个问题，提出了一种描述使用副作用的双向变换程序的新理论。

论文信息：

Ruifeng Xie, Tom Schrijvers, and Zhenjiang Hu. 2025. Effectful Lenses: There and Back with Different Monads. Proc. ACM Program. Lang. 9, ICFP, Article 254 (August 2025), 26 pages. https://doi.org/10.1145/3747523

双向变换是一种被广泛采用的数据同步方法，其核心通常包含从源数据到视图数据以及从视图数据回写至源数据的两个函数。然而，传统双向变换框架存在一个关键限制：这两个函数必须是“无副作用”的纯函数，这极大地限制了其在复杂现实场景中的应用。

针对这一长期存在的局限，获奖论文提出了一个更为通用的描述支持副作用的透镜的理论框架。该框架的主要贡献在于：允许双向变换的两个方向拥有不同类型的副作用（如日志记录、状态更新等），并且这些效应无需满足“可取消”的严格条件，大大拓宽了应用范围；定义了新的“往返关系”，并在此基础上成功地将双向变换的两个往返性质推广至支持副作用的透镜，保证了同步行为的正确性；提供了一套丰富的组合子语言，并证明了各组合子能够保持上述优良性质。这使得使用副作用的复杂的透镜程序能够像搭积木一样，由简单的透镜组合而成，极大地提升了开发效率与代码的可复用性。

最后，论文通过案例研究展示了该框架在实践中的强大灵活性与表达力，标志着在为双向变换理论引入程序副作用描述方面取得了重要理论突破。