F-Algebras and Free Monads

For an endofunctor , an -algebra is a morphism , where is the carrier and encodes the operations’ arities. Algebra homomorphisms are the maps commuting with the structure. The computation lives in the extremal algebras, the initial -algebra and the terminal -coalgebra, which coincide once types are read with a domain-theoretic semantics.

Definition. Initial algebra, catamorphism; terminal coalgebra, anamorphism

The initial -algebra is the least fixed point of . It presents the inductive datatype describes, and the unique map out of it to any other algebra is a catamorphism, a fold. Dually, the terminal -coalgebra is the greatest fixed point, the type of possibly-infinite behaviours, and the unique map into it is an anamorphism, an unfold. Folds consume finite structure, whereas unfolds generate it.

From magmas to monads

The gap between “operations” and “operations that obey laws” is exactly the gap between a magma and a monad.

Definition. F-magma versus monad

An -magma has operations with declared arities but no equations relating them, so it is pure syntax. A monad adds the laws. It is a monoid in the category of endofunctors, with unit and multiplication satisfying associativity and unit coherence. Passing from the underlying functor to the monad is precisely the act of imposing laws on the free-floating operations.

An equation between programs is a 2-cell. Two composites with the same boundary are related by a cell one dimension up, so that “these two programs are equal” is data rather than an afterthought.

Remark. The free monad is syntax before quotient

The free monad on is the datatype of finite terms built from ‘s operations with variables, the abstract syntax trees, taken before any equations are imposed. Quotienting it by a set of 2-cells (the laws) recovers the monad they present. In this sense the free monad is the term language, and a monad is a free monad modulo its equations. The datatypes actually expressible by such are pinned down by container/polynomial functors, and this algebra-of-programs is the recursion-scheme layer of an algorithm-as-morphism.

References

• Meijer, Fokkinga & Paterson, “Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire”, FPCA (1991), catamorphism/anamorphism, recursion schemes
• Goguen, Thatcher, Wagner & Wright (ADJ), “Initial Algebra Semantics and Continuous Algebras”, J. ACM (1977), initial-algebra semantics of datatypes
• Abbott, Altenkirch & Ghani, “Containers: Constructing Strictly Positive Types”, TCS (2005), container/polynomial functors expressible as F