Title: Quotients in monadic programming: Projective algebras are equivalent to coalgebras,
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.