Define and Then the set N of natural numbers together with the function [zero,succ]: 1 + N → N is an initial F-algebra.
The set of finite lists of natural numbers is an initial algebra for this functor.
Dually, a final coalgebra is a terminal object in the category of F-coalgebras.
, consisting of the set of natural numbers extended with a new element ω, is the carrier of the final coalgebra, where
In this case the carrier of the final coalgebra consists of all lists of natural numbers, finite as well as infinite.
Various finite data structures used in programming, such as lists and trees, can be obtained as initial algebras of specific endofunctors.
[1] In a dual way, similar relationship exists between notions of greatest fixed point and terminal F-coalgebra, with applications to coinductive types.
These can be used for allowing potentially infinite objects while maintaining strong normalization property.
[1] In the strongly normalizing (each program terminates) Charity programming language, coinductive data types can be used for achieving surprising results, e.g. defining lookup constructs to implement such “strong” functions like the Ackermann function.