Software frequently converts data from one representation to another and vice versa. Naively specifying both conversion directions separately is error prone and introduces conceptual duplication. Instead, bidirectional programming techniques allow programs to be written which can be interpreted in both directions. However, these techniques often employ programming idioms that are alien to non-experts, via restricted, specialised combinator libraries. Instead, we introduce a framework for composing bidirectional programs monadically, enabling bidirectional programming with familiar abstractions in functional languages such as Haskell. We demonstrate the generality of our approach applied to parsers/printers, lenses, and generators/predicates. We show how to leverage compositionality and equational reasoning for the verification of round-tripping properties for such monadic bidirectional programs.
Mon 8 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 16:00 | |||
14:00 30mTalk | Codata in Action ESOP Paul Downen University of Oregon, USA, Zachary Sullivan , Zena M. Ariola University of Oregon, USA, Simon Peyton Jones Microsoft, UK Link to publication | ||
14:30 30mTalk | Composing bidirectional programs monadically ESOP Li-yao Xia University of Pennsylvania, Dominic Orchard University of Kent, UK, Meng Wang University of Bristol, UK Link to publication | ||
15:00 30mTalk | Counters in Kappa: Semantics, Simulation, and Static Analysis ESOP Link to publication | ||
15:30 30mTalk | One Step at a Time ESOP Link to publication |