(Thanks Wikipedia)
In mathematics, specifically in category theory, F-algebras generalize the notion of algebraic structure. If C is a category, and F: C → C is an endofunctor of C, then an F-algebra is a tuple (A, α), where A is an object of C and α is a C-morphism F(A) → A. The object A is called the carrier of the algebra. When it is permissible from context, algebras are often referred to by their carrier only instead of the tuple.
F-algebras constitute a category, and the initial object of this category, namely the inital algebra, is the one with an unique morphism to all other algebras in the category. In other words we can evaluated the initial algebra to whichever carrier type we want.
Various finite data structures used in programming, such as lists and trees, can be obtained as initial algebras of specific endofunctors.
Let's define the following non recursive data type:
type ListF<E, A> = NilF | ConsF<E, A>
This type could be easily made a functor on A
, that is the carrier type, whereas E
is the type of the element contained in this weird list.
How does an algebra look like? If we choose number
for both A
and E
we can create an algebra that sums the values:
const SumAlgebra = (listF: ListF<number, number>) => {
if(listF is NilF) return 0
else return listF.A + listF.E
}
This algebra has the type ListF<number, number> => number
.
Using the encoding of Higher Kinded Types, made available by the fp-ts library, is possible to define the Fix
type constructor, which kind is (* -> *) -> *
, to then derive the least fixex point of an endofunctor. This fixed point is the initial algebra we are looking for.
Applying Fix
to ListF
we get its fixed point:
type List<E> = Fix2<ListF<E>>
Now we are able to create list of whichever length we want to, instead of being limited to only one value. Now let's say we have a List<number>
and we want to sum all the numbers into it. How would you do it? You could write a recursive function of course, but you don't know yet that the SumAlgebra
defined above is all you need.
It couls sound strange at first, because the SumAlgebra
is able to handle only one step.
The main point, that follows from the properties of F-algebras and their relation with the corresponding initial algebra, is that we can write one function, only one function, that is able to work with all the possible fixed points (data structures) and all the possible algebras (evaluation strategies), which given a fixed point and an algebra will evaluate the former, that could be arbitrarly deep, using the latter.
This magic function is called catamorphism, cata for friends.
- Programming with Categories - Lecture 9
- Programming with Categories - Lecture 10
- Programming with Categories - Lecture 11
It is only a proof of concept. It seems we can do this in TypeScript, but should we?
npm i
npx ts-node algebra/index.ts