Reversible Effects as Inverse Arrows

Chris Heunen; Robin Kaarsgaard; Martti Karvonen

doi:10.1016/j.entcs.2018.11.009

Reversible Effects as Inverse Arrows

Chris Heunen, Robin Kaarsgaard, Martti Karvonen

2 Citations (Scopus)

46 Downloads (Pure)

Abstract

Reversible computing models settings in which all processes can be reversed. Applications include low-power computing, quantum computing, and robotics. It is unclear how to represent side-effects in this setting, because conventional methods need not respect reversibility. We model reversible effects by adapting Hughes' arrows to dagger arrows and inverse arrows. This captures several fundamental reversible effects, including serialization and mutable store computations. Whereas arrows are monoids in the category of profunctors, dagger arrows are involutive monoids in the category of profunctors, and inverse arrows satisfy certain additional properties. These semantics inform the design of functional reversible programs supporting side-effects.

Original language	English
Journal	Electronic Notes in Theoretical Computer Science
Volume	341
Pages (from-to)	179-199
ISSN	1571-0661
DOIs	https://doi.org/10.1016/j.entcs.2018.11.009
Publication status	Published - 1 Dec 2018
Event	34th Conference on the Mathematical Foundations of Programming Semantics - Dalhousie University, Halifax, Canada Duration: 6 Jun 2018 → 9 Jun 2018 Conference number: 34 https://www.mathstat.dal.ca/mfps2018/

Conference

Conference	34th Conference on the Mathematical Foundations of Programming Semantics
Number	34
Location	Dalhousie University
Country/Territory	Canada
City	Halifax
Period	06/06/2018 → 09/06/2018
Internet address	https://www.mathstat.dal.ca/mfps2018/

Keywords

Arrow
Inverse Category
Involutive Monoid
Reversible Effect

Access to Document

10.1016/j.entcs.2018.11.009Licence: CC BY

ArticleKaarsgaardFinal published version, 288 KBLicence: CC BY

Cite this

@inproceedings{4df5fb2916c34c37b13bb772b1ae7ccf,

title = "Reversible Effects as Inverse Arrows",

abstract = "Reversible computing models settings in which all processes can be reversed. Applications include low-power computing, quantum computing, and robotics. It is unclear how to represent side-effects in this setting, because conventional methods need not respect reversibility. We model reversible effects by adapting Hughes' arrows to dagger arrows and inverse arrows. This captures several fundamental reversible effects, including serialization and mutable store computations. Whereas arrows are monoids in the category of profunctors, dagger arrows are involutive monoids in the category of profunctors, and inverse arrows satisfy certain additional properties. These semantics inform the design of functional reversible programs supporting side-effects.",

keywords = "Arrow, Inverse Category, Involutive Monoid, Reversible Effect",

author = "Chris Heunen and Robin Kaarsgaard and Martti Karvonen",

year = "2018",

month = dec,

day = "1",

doi = "10.1016/j.entcs.2018.11.009",

language = "English",

volume = "341",

pages = "179--199",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier",

note = "34th Conference on the Mathematical Foundations of Programming Semantics, MFPS ; Conference date: 06-06-2018 Through 09-06-2018",

url = "https://www.mathstat.dal.ca/mfps2018/",

}

TY - GEN

T1 - Reversible Effects as Inverse Arrows

AU - Heunen, Chris

AU - Kaarsgaard, Robin

AU - Karvonen, Martti

N1 - Conference code: 34

PY - 2018/12/1

Y1 - 2018/12/1

N2 - Reversible computing models settings in which all processes can be reversed. Applications include low-power computing, quantum computing, and robotics. It is unclear how to represent side-effects in this setting, because conventional methods need not respect reversibility. We model reversible effects by adapting Hughes' arrows to dagger arrows and inverse arrows. This captures several fundamental reversible effects, including serialization and mutable store computations. Whereas arrows are monoids in the category of profunctors, dagger arrows are involutive monoids in the category of profunctors, and inverse arrows satisfy certain additional properties. These semantics inform the design of functional reversible programs supporting side-effects.

AB - Reversible computing models settings in which all processes can be reversed. Applications include low-power computing, quantum computing, and robotics. It is unclear how to represent side-effects in this setting, because conventional methods need not respect reversibility. We model reversible effects by adapting Hughes' arrows to dagger arrows and inverse arrows. This captures several fundamental reversible effects, including serialization and mutable store computations. Whereas arrows are monoids in the category of profunctors, dagger arrows are involutive monoids in the category of profunctors, and inverse arrows satisfy certain additional properties. These semantics inform the design of functional reversible programs supporting side-effects.

KW - Arrow

KW - Inverse Category

KW - Involutive Monoid

KW - Reversible Effect

UR - http://www.scopus.com/inward/record.url?scp=85058019859&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2018.11.009

DO - 10.1016/j.entcs.2018.11.009

M3 - Conference article

SN - 1571-0661

VL - 341

SP - 179

EP - 199

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

T2 - 34th Conference on the Mathematical Foundations of Programming Semantics

Y2 - 6 June 2018 through 9 June 2018

ER -

Reversible Effects as Inverse Arrows

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this