Composing bidirectional programs monadically (with appendices)

TL;DR

This paper introduces a monadic framework for bidirectional programming in functional languages, enhancing composability, verification, and usability across various data transformation applications.

Contribution

It presents a novel monadic approach to bidirectional programming, making it more accessible and generalizable within familiar functional programming abstractions.

Findings

Framework applicable to parsers, printers, lenses, generators, and predicates

Enables compositional reasoning and verification of round-tripping properties

Demonstrates improved usability and generality in bidirectional programming

Abstract

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 unfamiliar programming idioms 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.