Effectful Lenses: There and Back with Different MonadsDistinguished 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.
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.
Mon 13 OctDisplayed time zone: Perth change
13:40 - 15:20 | |||
13:40 25mTalk | Call-Guarded Abstract Definitional InterpretersDistinguished Paper ICFP Papers Kimball Germane Brigham Young University DOI | ||
14:05 25mTalk | Effectful Lenses: There and Back with Different MonadsDistinguished Paper ICFP Papers DOI | ||
14:30 25mTalk | First-Order LazinessDistinguished Paper ICFP Papers Anton Lorenzen University of Edinburgh, Daan Leijen Microsoft Research, Wouter Swierstra Utrecht University, Netherlands, Sam Lindley University of Edinburgh DOI Pre-print | ||
14:55 25mTalk | Multi-stage Programming with Splice VariablesDistinguished Paper ICFP Papers DOI | ||