Categorical Semantics of Reversible Pattern-Matching

TL;DR

This paper develops a categorical framework for modeling reversible pattern-matching in a typed functional language, extending existing structures to accurately represent core constructs of Theseus.

Contribution

It introduces a new categorical structure that captures pattern-matching in reversible computation, addressing limitations of existing models.

Findings

Proposes a categorical structure for reversible pattern-matching.

Demonstrates the structure as an adequate model for Theseus.

Extends join inverse rig categories to include pattern-matching capabilities.

Abstract

This paper is concerned with categorical structures for reversible computation. In particular, we focus on a typed, functional reversible language based on Theseus. We discuss how join inverse rig categories do not in general capture pattern-matching, the core construct Theseus uses to enforce reversibility. We then derive a categorical structure to add to join inverse rig categories in order to capture pattern-matching. We show how such a structure makes an adequate model for reversible pattern-matching.