Join inverse categories and reversible recursion

Robin Kaarsgaard, Holger Bock Axelsen, Robert Glück

12 Citations (Scopus)

Abstract

Recently, a number of reversible functional programming languages have been proposed. Common to several of these is the assumption of totality, a property that is not necessarily desirable, and certainly not required in order to guarantee reversibility. In a categorical setting, however, faithfully capturing partiality requires handling it as additional structure. Recently, Giles studied inverse categories as a model of partial reversible (functional) programming. In this paper, we show how additionally assuming the existence of countable joins on such inverse categories leads to a number of properties that are desirable when modeling reversible functional programming, notably morphism schemes for reversible recursion, a †-trace, and algebraic ω-compactness. This gives a categorical account of reversible recursion, and, for the latter, provides an answer to the problem posed by Giles regarding the formulation of recursive data types at the inverse category level.

Original languageEnglish
JournalJournal of Logical and Algebraic Methods in Programming
Volume87
Pages (from-to)33-50
Number of pages18
ISSN2352-2208
DOIs
Publication statusPublished - 1 Feb 2017

Fingerprint

Dive into the research topics of 'Join inverse categories and reversible recursion'. Together they form a unique fingerprint.

Cite this