A general framework for effectful bidirectional programming: There and back with different monads

This is the manuscript submitted to JFP for review. It is an extended version of the ICFP 2025 paper, Effectful Lenses: There and Back with Different Monads by the same three authors. Below is the abstract of the paper. 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, or allowing only some fixed effects. In this article, we propose a much more general framework for effectful bidirectional programming, with different user-selected effects in their two directions. Our bidirectional programs take the simple form of effectful isomorphisms, but effectful lenses are also supported as a special case of the framework by mixing in two special effects. We generalise the two well-known round-trip properties to the effectful setup by introducing the free compositions and pure-likeness properties. Moreover, we show that 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.