Reversible monadic computing

TL;DR

This paper extends categorical semantics to reversible monadic programming using dagger categories, demonstrating that Frobenius monads model reversible effectful computations and characterizing their algebraic structure.

Contribution

It introduces Frobenius monads in dagger categories to model reversibility in monadic programming, linking effectful computations with quantum measurement.

Findings

Reversible effectful computations are modeled by Frobenius monads.

Frobenius monads characterize reversible subcategories of Eilenberg-Moore algebras.

Quantum measurements are represented as Frobenius monads in the example.

Abstract

We extend categorical semantics of monadic programming to reversible computing, by considering monoidal closed dagger categories: the dagger gives reversibility, whereas closure gives higher-order expressivity. We demonstrate that Frobenius monads model the appropriate notion of coherence between the dagger and closure by reinforcing Cayley's theorem; by proving that effectful computations (Kleisli morphisms) are reversible precisely when the monad is Frobenius; by characterizing the largest reversible subcategory of Eilenberg-Moore algebras; and by identifying the latter algebras as measurements in our leading example of quantum computing. Strong Frobenius monads are characterized internally by Frobenius monoids.