一句话：提出一个更通用的带效应透镜框架，两个方向可使用不同 Monad，并保持往返性质与组合性。
双向变换通常由 source→view 和 view→source 两个函数构成，传统上要求它们无副作用。已有将 Monad 引入透镜的框架限制较强，例如只允许后向变换产生效应。本文提出更通用的带效应透镜框架：两个方向可以具有不同效应，且效应无需可取消。作者定义往返关系，并据此将两个经典往返性质推广到带效应情形；证明组合保持这些性质，并提供丰富的组合子语言以支持带效应透镜的组合式编程。最后通过案例研究展示该框架的灵活性与表达力。
Bidirectional transformations (BXs) are a widely adopted approach for data synchronisation that is usually based on two functions, one from the source to the view and one back. Traditionally, these functions must not have side effects. While a few frameworks aim to lift this restriction by introducing monads into lenses, they are still quite limited, e.g., allowing only side effects in the backwards transformation. In this paper, we propose a much more general framework for effectful lenses. Our effectful lenses can have different effects in their two directions, and the effects need not be cancellable. We also define the round-trip relations and use them to generalise the two well-known round-trip properties to effectful lenses. Moreover, composition preserves the two well-known round-trip properties, and we also provide a rich combinator language, which enables compositional programming for effectful lenses. Finally, we present a case study to illustrate the flexibility and expressivity of our framework.
@article{paperbot3046,
title = {Effectful Lenses: There and Back with Different Monads},
author = {Ruifeng Xie and Tom Schrijvers and Zhenjiang Hu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {ICFP},
year = {2025},
doi = {10.1145/3747523}
}