Quotients in monadic programming: Projective algebras are equivalent to coalgebras

TL;DR

This paper explores the relationship between projective algebras and coalgebras in monadic programming, offering a new perspective on implementing quotient types and their categorical properties.

Contribution

It characterizes projective algebras in monadic programming and establishes an equivalence with coalgebras, enabling practical implementation of quotient types.

Findings

Projective algebras are equivalent to coalgebras for the induced comonad.

This equivalence facilitates implementing polymorphic quotients as coalgebras.

The work reveals new applications for quotient types and their categorical properties.

Abstract

In monadic programming, datatypes are presented as free algebras, generated by data values, and by the algebraic operations and equations capturing some computational effects. These algebras are free in the sense that they satisfy just the equations imposed by their algebraic theory, and remain free of any additional equations. The consequence is that they do not admit quotient types. This is, of course, often inconvenient. Whenever a computation involves data with multiple representatives, and they need to be identified according to some equations that are not satisfied by all data, the monadic programmer has to leave the universe of free algebras, and resort to explicit destructors. We characterize the situation when these destructors are preserved under all operations, and the resulting quotients of free algebras are also their subalgebras. Such quotients are called *projective*. Although popular in universal algebra, projective algebras did not attract much attention in the monadic setting, where they turn out to have a surprising avatar: for any given monad, a suitable category of projective algebras is equivalent with the category of coalgebras for the comonad induced by any monad resolution. For a monadic programmer, this equivalence provides a convenient way to implement polymorphic quotients as coalgebras. The dual correspondence of injective coalgebras and all algebras leads to a different family of quotient types, which seems to have a different family of applications. Both equivalences also entail several general corollaries concerning monadicity and comonadicity.