Invertible Syntax without the Tuples (Functional Pearl)
Mathieu Boespflug, Arnaud Spiwack
TL;DR
The paper revisits Olivier Danvy’s insight on invertible syntax via continuation-passing style and extends it beyond the original unary setting to handle inductive data through three approaches. It first offers an applicative CPS-based solution using string transformers and the K7 cassette to construct dual parsing/printing descriptors without tuple-driven impedance, then presents an alternative by introducing leads and prisms for modular, vertically composable descriptors. A monadic solution follows, employing stacked and indexed monads to capture context-sensitive grammars and effects, with continuations and stack manipulation enabling more expressive formatting pipelines. The work analyzes the trade-offs between symmetry and expressivity, highlights limitations such as partiality and error reporting, and points toward future directions including connections to delimited control and broader bidirectional programming frameworks. Overall, the paper demonstrates that continuation-passing style remains a unifying, practical tool for building invertible syntax across increasingly expressive data structures.
Abstract
In the seminal paper Functional unparsing, Olivier Danvy used continuation passing to reanalyse printf-like format strings as combinators. In the intervening decades, the conversation shifted towards a concurrent line of work -- applicative, monadic or arrow-based combinator libraries -- in an effort to find combinators for invertible syntax descriptions that simultaneously determine a parser as well as a printer, and with more expressive power, able to handle inductive structures such as lists and trees. Along the way, continuation passing got lost. This paper argues that Danvy's insight remains as relevant to the general setting as it was to the restricted setting of his original paper. Like him, we present three solutions that exploit continuation-passing style as an alternative to both dependent types and monoidal aggregation via nested pairs, in our case to parse and print structured data with increasing expressive power.