Composing Bidirectional Programs Monadically

Li-yao Xia; Dominic Orchard; Meng Wang

doi:10.1007/978-3-030-17184-1_6

Composing Bidirectional Programs Monadically

Li-yao Xia, Dominic Orchard, Meng Wang

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

Software frequently converts data from one representation to another and vice versa. Naïvely 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.

Original language	English
Title of host publication	Programming Languages and Systems
Editors	Luís Caires
Place of Publication	Cham
Publisher	Springer International Publishing Switzerland
Pages	147-175
Number of pages	29
ISBN (Electronic)	978-3-030-17184-1
ISBN (Print)	978-3-030-17183-4
DOIs	https://doi.org/10.1007/978-3-030-17184-1_6
Publication status	Published - 6 Apr 2019
Event	28th European Symposium on Programming - Prague, Czech Republic Duration: 8 Apr 2019 → 11 Apr 2019 Conference number: 28 https://conf.researchr.org/track/etaps-2019/esop-2019-papers

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Cham
Volume	11423
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Symposium

Symposium	28th European Symposium on Programming
Abbreviated title	ESOP 2019
Country/Territory	Czech Republic
City	Prague
Period	8/04/19 → 11/04/19
Internet address	https://conf.researchr.org/track/etaps-2019/esop-2019-papers

Access to Document

10.1007/978-3-030-17184-1_6Licence: Creative Commons: Attribution (CC-BY)

Composing Bidirectional_XIA_DOA25012019_VOR_CC-BYFinal published version, 1.16 MBLicence: Creative Commons: Attribution (CC-BY)

https://link.springer.com/chapter/10.1007/978-3-030-17184-1_6Licence: Creative Commons: Attribution (CC-BY)

Cite this

@inproceedings{0015697c9e0c45aba4027180e5f6966e,

title = "Composing Bidirectional Programs Monadically",

abstract = "Software frequently converts data from one representation to another and vice versa. Na{\"i}vely 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.",

author = "Li-yao Xia and Dominic Orchard and Meng Wang",

year = "2019",

month = apr,

day = "6",

doi = "10.1007/978-3-030-17184-1_6",

language = "English",

isbn = "978-3-030-17183-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer International Publishing Switzerland",

pages = "147--175",

editor = "Lu{\'i}s Caires",

booktitle = "Programming Languages and Systems",

note = "28th European Symposium on Programming, ESOP 2019 ; Conference date: 08-04-2019 Through 11-04-2019",

url = "https://conf.researchr.org/track/etaps-2019/esop-2019-papers",

}

TY - GEN

T1 - Composing Bidirectional Programs Monadically

AU - Xia, Li-yao

AU - Orchard, Dominic

AU - Wang, Meng

N1 - Conference code: 28

PY - 2019/4/6

Y1 - 2019/4/6

N2 - Software frequently converts data from one representation to another and vice versa. Naïvely 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.

AB - Software frequently converts data from one representation to another and vice versa. Naïvely 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.

U2 - 10.1007/978-3-030-17184-1_6

DO - 10.1007/978-3-030-17184-1_6

M3 - Conference contribution

SN - 978-3-030-17183-4

T3 - Lecture Notes in Computer Science

SP - 147

EP - 175

BT - Programming Languages and Systems

A2 - Caires, Luís

PB - Springer International Publishing Switzerland

CY - Cham

T2 - 28th European Symposium on Programming

Y2 - 8 April 2019 through 11 April 2019

ER -

Composing Bidirectional Programs Monadically

Abstract

Publication series

Symposium

Access to Document

Fingerprint

Cite this