Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Tue 25 Sep 2018 15:45 - 16:07 at Stifel Theatre - Bidirectional Programming Chair(s): Wouter Swierstra

Quotient lenses are bidirectional transformations whose correctness laws are ``loosened'' by specified equivalence relations, allowing inessential details in concrete data formats to be suppressed. For example, a programmer could use a quotient lens to define a transformation that ignores the order of fields in XML data, so that two XML files with the same fields but in different orders would be considered the same, allowing a single, simple program to handle them both.

Building on a recently published algorithm for synthesizing plain bijective lenses from high-level specifications, we show how to synthesize bijective quotient lenses in three steps. First, we introduce quotient regular expressions} (QREs), annotated regular expressions that conveniently mark inessential aspects of string data formats; each QRE specifies, simulteneously, a regular language and an equivalence relation on it. Second, we introduce QRE lenses, i.e., lenses mapping between QREs. Our key technical result is a proof that every QRE lens can be transformed into a functionally equivalent lens that canonizes source and target data only once at the “edges” then uses a bijective lens to map between the respective canonical elements; no internal canonization occurs for a lens in this normal form. Third, we leverage this normalization theorem to synthesize QRE lenses from a pair of QREs and example input-output pairs, reusing earlier work on synthesizing plain bijective lenses. We have implemented QREs and QRE lens synthesis as an extension to the bidirectional programming language Boomerang. We evaluate the effectiveness of our approach by synthesizing QRE lenses between various real-world data formats in the Optician benchmark suite.

Tue 25 Sep

Displayed time zone: Guadalajara, Mexico City, Monterrey change

15:00 - 16:30
Bidirectional ProgrammingResearch Papers at Stifel Theatre
Chair(s): Wouter Swierstra Utrecht University, Netherlands
15:00
22m
Talk
What You Needa Know about Yoneda: Profunctor Optics and the Yoneda Lemma (Functional Pearl)
Research Papers
Guillaume Boisseau University of Oxford, Jeremy Gibbons Department of Computer Science, University of Oxford
DOI
15:22
22m
Talk
Incremental Relational Lenses
Research Papers
Rudi Horn University of Edinburgh, Roly Perera University of Glasgow, James Cheney University of Edinburgh, UK
DOI
15:45
22m
Talk
Synthesizing Quotient Lenses
Research Papers
Solomon Maina University of Pennsylvania, Anders Miltner Princeton University, Kathleen Fisher Tufts University, USA, Benjamin C. Pierce University of Pennsylvania, Dave Walker Princeton University, Steve Zdancewic University of Pennsylvania
DOI
16:07
22m
Talk
Generic Deriving of Generic Traversals
Research Papers
Csongor Kiss Imperial College London, Matthew Pickering University of Bristol, Nicolas Wu University of Bristol, UK
DOI