Reversible Effects as Inverse Arrows
Publikation: Bidrag til tidsskrift › Konferenceartikel › Forskning › fagfællebedømt
Standard
Reversible Effects as Inverse Arrows. / Heunen, Chris; Kaarsgaard, Robin; Karvonen, Martti.
I: Electronic Notes in Theoretical Computer Science, Bind 341, 01.12.2018, s. 179-199.Publikation: Bidrag til tidsskrift › Konferenceartikel › Forskning › fagfællebedømt
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
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
VL - 341
SP - 179
EP - 199
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
SN - 1571-0661
T2 - 34th Conference on the Mathematical Foundations of Programming Semantics
Y2 - 6 June 2018 through 9 June 2018
ER -
ID: 211215598