# Categorical Semantics of Reversible Pattern-Matching

arXiv: https://arxiv.org/abs/2109.05837 · HTML: https://mlsanity.com/paper/2109.05837/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 6 of its 36 references that are in the map.
- First posted on arXiv 13 Sep 2021.

## Builds on (most cited first, 6 of 6)

- [Reversible effects as inverse arrows](https://mlsanity.com/paper/1805.08605/) (2018)
- [Reversible monadic computing](https://mlsanity.com/paper/1505.04330/) (2015)
- [A categorical foundation for structured reversible flowchart languages: Soundness and adequacy](https://mlsanity.com/paper/1710.03666/) (2017)
- [Inversion, Iteration, and the Art of Dual Wielding](https://mlsanity.com/paper/1904.01679/) (2019)
- [Condition/Decision Duality and the Internal Logic of Extensive Restriction Categories](https://mlsanity.com/paper/1905.09181/) (2019)
- [Join Inverse Rig Categories for Reversible Functional Programming, and Beyond](https://mlsanity.com/paper/2105.09929/) (2021)

## Abstract (arXiv)

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.