Initial F-algebras and free F-algebras over a type If F is a given functor, an
F-algebra is a type s and a morphism F s -> s. This generalizes constructions such as a monoid or a group.
For instance, a (type-level) monoid is a type m, a selected value "munit" of type m (the "unit" element), and a binary operation m * m -> m. We can rewrite this data as an algebra-like morphism "F m -> m" in three steps:
- replace the selected "unit" value of type m by a selected morphism 1 -> m, which is equivalent data,
- observe that now the data required for the F-algebra is a value of type (1 -> m)*(m*m -> m),
- observe that this data will be of the algebra-like form F m -> m if we define the functor F as F t = 1 + t*t (which, by the way, is a polynomial functor).
(The laws of the monoid, such as munit * m = m, are not covered by this description; we ignore this for now.)
Suppose we are given a functor F; we can then ask what are the possible types s for which an F-algebra morphism F s -> s can be constructed. A way of finding out is to construct the "free F-algebra".
We have already figured out some heuristics about how to construct free structures and what to expect of them. Our intuition is that we first define a new type by writing our requirements in the form of a representable functor and then putting a fixpoint over that functor. The fixpoint will be such that we could map it to any other structure. In our case, we will obtain a "free F-algebra" from which we could map to any other F-algebra. In the categorical language, this means that the "free F-algebra" will be the initial object in the category of F-algebras. Let us see how this works in practice.
The heuristic says that the "initial F-algebra" is written in "Haskell long form" as
data InitFA where
Alg:: F (InitFA) -> InitFA
In the short notation, this is just Fix
x F x, i.e. the type which is the fixpoint of the functor F. Note that Fix
x F x is not a functor (no type parameters are left) -- it's a order-0 type.
Now, we expect that the initial F-algebra can be mapped to any other F-algebra: If
b is another F-algebra then we will have a morphism FreeFA -> b. In order to implement this, we need a morphism of type (F b -> b) -> InitFA -> b. This morphism is called a
catamorphism and is defined by
cata :: (F b -> b) -> InitFA -> b
cata (f :: F b -> b) (g :: F InitFA) -> fmap
F (cata f) g
Another interpretation of the initial F-algebra is that the functor F describes the composition of a recursive data structure. In functional programming, a functor value "F t" is interpreted as a data structure that contains some values of type t. Then InitFA = Fix
x F x is a recursive type that represents the data structure recursively containing some values of InitFA; the pattern of these recursive values is given by F. An F-algebra morphism F b -> b is interpreted as an "evaluation" algorithm that computes a value of b out of that recursive data structure, assuming that the recursive instances of InitFA have been already converted to b. What the catamorphism does is to convert an F-algebra evaluator F b -> b, which is nonrecursive, to the recursive evaluator InitFA -> b.
Let us now consider a slightly different construction: a free F-algebra over a type s. The words "over a type s" mean that we should have a way of injecting values of type s into the free F-algebra, and that this property is in addition to the F-algebra property.
According to our heuristics, these requirements mean that we should have the morphisms
s -> FreeFA
and
F (FreeFA) -> FreeFA
It follows that FreeFA = Fix
x s + F x.
Now, this is exactly the same as the free monad over F (which is defined by FreeM F t = Fix
xt + F x) except that it is specialized to the type s:
FreeFA = FreeM F s.
The free F-algebra over s again has the "initial property": if b is any other F-algebra, and if we have a morphism s -> b, then we can produce a catamorphism that maps FreeFA -> b (and this mapping is a homomorphism of F-algebras). The required catamorphism is exactly the same as the general catamorphism "cata" of initial F-algebras, except that it is applied to the functor G x = s + F x instead of the functor F x.
Reading
https://www.schoolofhaskell.com/user/bartosz/understanding-algebras helped me understand these things.