Chapter 3.8 - F-Algebras

This commit is contained in:
Igal Tabachnik 2017-09-26 22:09:32 +03:00
parent ccc974aaa4
commit 7836fc1177
2 changed files with 163 additions and 152 deletions

View File

@ -1,12 +1,4 @@
\begin{quote} \lettrine[lhang=0.17]{W}{e've seen several} formulations of a monoid: as a set, as a
This is part 24 of Categories for Programmers. Previously:
\href{https://bartoszmilewski.com/2017/01/02/comonads/}{Comonads}. See
the
\href{https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/}{Table
of Contents}.
\end{quote}
We've seen several formulations of a monoid: as a set, as a
single-object category, as an object in a monoidal category. How much single-object category, as an object in a monoidal category. How much
more juice can we squeeze out of this simple concept? more juice can we squeeze out of this simple concept?
@ -14,9 +6,9 @@ Let's try. Take this definition of a monoid as a set \code{m} with a
pair of functions: pair of functions:
\begin{verbatim} \begin{verbatim}
μ :: m × m -> m η :: 1 -> m μ :: m × m -> m
η :: 1 -> m
\end{verbatim} \end{verbatim}
Here, 1 is the terminal object in \textbf{Set} --- the singleton set. Here, 1 is the terminal object in \textbf{Set} --- the singleton set.
The first function defines multiplication (it takes a pair of elements The first function defines multiplication (it takes a pair of elements
and returns their product), the second selects the unit element from and returns their product), the second selects the unit element from
@ -27,23 +19,21 @@ and just consider ``potential monoids.'' A pair of functions is an
element of a cartesian product of two sets of functions. We know that element of a cartesian product of two sets of functions. We know that
these sets may be represented as exponential objects: these sets may be represented as exponential objects:
\begin{verbatim} \begin{Verbatim}[commandchars=\\\{\}]
μ ∈ m m×m η ∈ m1 μ \ensuremath{\in} m \textsuperscript{m×m}
\end{verbatim} η \ensuremath{\in} m\textsuperscript{1}
\end{Verbatim}
The cartesian product of these two sets is: The cartesian product of these two sets is:
\begin{verbatim} \begin{Verbatim}[commandchars=\\\{\}]
m m×m × m1 m m×m × m\textsuperscript{1}
\end{verbatim} \end{Verbatim}
Using some high-school algebra (which works in every cartesian closed Using some high-school algebra (which works in every cartesian closed
category), we can rewrite it as: category), we can rewrite it as:
\begin{verbatim} \begin{Verbatim}[commandchars=\\\{\}]
m m×m + 1 m \textsuperscript{m×m + 1}
\end{verbatim} \end{Verbatim}
The plus sign stands for the coproduct in \textbf{Set}. We have just The plus sign stands for the coproduct in \textbf{Set}. We have just
replaced a pair of functions with a single function --- an element of replaced a pair of functions with a single function --- an element of
the set: the set:
@ -51,7 +41,6 @@ the set:
\begin{verbatim} \begin{verbatim}
m × m + 1 -> m m × m + 1 -> m
\end{verbatim} \end{verbatim}
Any element of this set of functions is a potential monoid. Any element of this set of functions is a potential monoid.
The beauty of this formulation is that it leads to interesting The beauty of this formulation is that it leads to interesting
@ -63,15 +52,15 @@ addition as a binary operation, zero as the unit, and negation as the
inverse. To define a group we would start with a triple of functions: inverse. To define a group we would start with a triple of functions:
\begin{verbatim} \begin{verbatim}
m × m -> m m -> m 1 -> m m × m -> m
m -> m
1 -> m
\end{verbatim} \end{verbatim}
As before, we can combine all these triples into one set of functions: As before, we can combine all these triples into one set of functions:
\begin{verbatim} \begin{verbatim}
m × m + m + 1 -> m m × m + m + 1 -> m
\end{verbatim} \end{verbatim}
We started with one binary operator (addition), one unary operator We started with one binary operator (addition), one unary operator
(negation), and one nullary operator (identity --- here zero). We (negation), and one nullary operator (identity --- here zero). We
combined them into one function. All functions with this signature combined them into one function. All functions with this signature
@ -105,7 +94,6 @@ object \code{a}, and a morphism
\begin{verbatim} \begin{verbatim}
F a -> a F a -> a
\end{verbatim} \end{verbatim}
The object is often called the carrier, an underlying object or, in the The object is often called the carrier, an underlying object or, in the
context of programming, the carrier \newterm{type}. The morphism is often context of programming, the carrier \newterm{type}. The morphism is often
called the evaluation function or the structure map. Think of the called the evaluation function or the structure map. Think of the
@ -117,7 +105,6 @@ Here's the Haskell definition of an F-algebra:
\begin{verbatim} \begin{verbatim}
type Algebra f a = f a -> a type Algebra f a = f a -> a
\end{verbatim} \end{verbatim}
It identifies the algebra with its evaluation function. It identifies the algebra with its evaluation function.
In the monoid example, the functor in question is: In the monoid example, the functor in question is:
@ -125,27 +112,33 @@ In the monoid example, the functor in question is:
\begin{verbatim} \begin{verbatim}
data MonF a = MEmpty | MAppend a a data MonF a = MEmpty | MAppend a a
\end{verbatim} \end{verbatim}
This is Haskell for \code{1 + a × a} (remember
This is Haskell for \code{1\ +\ a\ ×\ a} (remember \hyperref[simple-algebraic-data-types]{algebraic
\href{https://bartoszmilewski.com/2015/01/13/simple-algebraic-data-types/}{algebraic
data structures}). data structures}).
A ring would be defined using the following functor: A ring would be defined using the following functor:
\begin{verbatim} \begin{verbatim}
data RingF a = RZero | ROne | RAdd a a | RMul a a | RNeg a data RingF a = RZero
| ROne
| RAdd a a
| RMul a a
| RNeg a
\end{verbatim} \end{verbatim}
which is Haskell for \code{1 + 1 + a × a + a × a + a}.
which is Haskell for \code{1\ +\ 1\ +\ a\ ×\ a\ +\ a\ ×\ a\ +\ a}.
An example of a ring is the set of integers. We can choose An example of a ring is the set of integers. We can choose
\code{Integer} as the carrier type and define the evaluation function \code{Integer} as the carrier type and define the evaluation function
as: as:
\begin{verbatim} \begin{Verbatim}[commandchars=\\\{\}]
evalZ :: Algebra RingF Integer evalZ RZero = 0 evalZ ROne = 1 evalZ (RAdd m n) = m + n evalZ (RMul m n) = m * n evalZ (RNeg n) = -n evalZ :: \textbf{Algebra} RingF Integer
\end{verbatim} evalZ RZero = 0
evalZ ROne = 1
evalZ (RAdd m n) = m + n
evalZ (RMul m n) = m * n
evalZ (RNeg n) = -n
\end{Verbatim}
There are more F-algebras based on the same functor \code{RingF}. For There are more F-algebras based on the same functor \code{RingF}. For
instance, polynomials form a ring and so do square matrices. instance, polynomials form a ring and so do square matrices.
@ -162,15 +155,22 @@ instance, an arbitrary expression in a ring is generated by this
tree-like data structure: tree-like data structure:
\begin{verbatim} \begin{verbatim}
data Expr = RZero | ROne | RAdd Expr Expr | RMul Expr Expr | RNeg Expr data Expr = RZero
| ROne
| RAdd Expr Expr
| RMul Expr Expr
| RNeg Expr
\end{verbatim} \end{verbatim}
We can replace the original ring evaluator with its recursive version: We can replace the original ring evaluator with its recursive version:
\begin{verbatim} \begin{verbatim}
evalZ :: Expr -> Integer evalZ RZero = 0 evalZ ROne = 1 evalZ (RAdd e1 e2) = evalZ e1 + evalZ e2 evalZ (RMul e1 e2) = evalZ e1 * evalZ e2 evalZ (RNeg e) = -(evalZ e) evalZ :: Expr -> Integer
evalZ RZero = 0
evalZ ROne = 1
evalZ (RAdd e1 e2) = evalZ e1 + evalZ e2
evalZ (RMul e1 e2) = evalZ e1 * evalZ e2
evalZ (RNeg e) = -(evalZ e)
\end{verbatim} \end{verbatim}
This is still not very practical, since we are forced to represent all This is still not very practical, since we are forced to represent all
integers as sums of ones, but it will do in a pinch. integers as sums of ones, but it will do in a pinch.
@ -183,7 +183,6 @@ define a depth-one tree as:
\begin{verbatim} \begin{verbatim}
type RingF1 a = RingF (RingF a) type RingF1 a = RingF (RingF a)
\end{verbatim} \end{verbatim}
We are filling the holes in the definition of \code{RingF} with We are filling the holes in the definition of \code{RingF} with
depth-zero trees generated by \code{RingF\ a}. Depth-2 trees are depth-zero trees generated by \code{RingF\ a}. Depth-2 trees are
similarly obtained as: similarly obtained as:
@ -191,19 +190,16 @@ similarly obtained as:
\begin{verbatim} \begin{verbatim}
type RingF2 a = RingF (RingF (RingF a)) type RingF2 a = RingF (RingF (RingF a))
\end{verbatim} \end{verbatim}
which we can also write as: which we can also write as:
\begin{verbatim} \begin{verbatim}
type RingF2 a = RingF (RingF1 a) type RingF2 a = RingF (RingF1 a)
\end{verbatim} \end{verbatim}
Continuing this process, we can write a symbolic equation: Continuing this process, we can write a symbolic equation:
\begin{verbatim} \begin{Verbatim}[commandchars=\\\{\}]
type RingFn+1 a = RingF (RingFn a) type RingF\textsubscript{n+1} a = RingF (RingF\textsubscript{n} a)
\end{verbatim} \end{Verbatim}
Conceptually, after repeating this process infinitely many times, we end Conceptually, after repeating this process infinitely many times, we end
up with our \code{Expr}. Notice that \code{Expr} does not depend on up with our \code{Expr}. Notice that \code{Expr} does not depend on
\code{a}. The starting point of our journey doesn't matter, we always \code{a}. The starting point of our journey doesn't matter, we always
@ -220,37 +216,33 @@ point}, an object defined as:
\begin{verbatim} \begin{verbatim}
Fix f = f (Fix f) Fix f = f (Fix f)
\end{verbatim} \end{verbatim}
The intuition behind this definition is that, since we applied The intuition behind this definition is that, since we applied
\code{f} infinitely many times to get \code{Fix\ f}, applying it one \code{f} infinitely many times to get \code{Fix f}, applying it one
more time doesn't change anything. In Haskell, the definition of a fixed more time doesn't change anything. In Haskell, the definition of a fixed
point is: point is:
\begin{verbatim} \begin{verbatim}
newtype Fix f = Fix (f (Fix f)) newtype Fix f = Fix (f (Fix f))
\end{verbatim} \end{verbatim}
Arguably, this would be more readable if the constructor's name were Arguably, this would be more readable if the constructor's name were
different than the name of the type being defined, as in: different than the name of the type being defined, as in:
\begin{verbatim} \begin{verbatim}
newtype Fix f = In (f (Fix f)) newtype Fix f = In (f (Fix f))
\end{verbatim} \end{verbatim}
but I'll stick with the accepted notation. The constructor \code{Fix} but I'll stick with the accepted notation. The constructor \code{Fix}
(or \code{In}, if you prefer) can be seen as a function: (or \code{In}, if you prefer) can be seen as a function:
\begin{verbatim} \begin{verbatim}
Fix :: f (Fix f) -> Fix f Fix :: f (Fix f) -> Fix f
\end{verbatim} \end{verbatim}
There is also a function that peels off one level of functor There is also a function that peels off one level of functor
application: application:
\begin{verbatim} \begin{verbatim}
unFix :: Fix f -> f (Fix f) unFix (Fix x) = x unFix :: Fix f -> f (Fix f)
unFix (Fix x) = x
\end{verbatim} \end{verbatim}
The two functions are the inverse of each other. We'll use these The two functions are the inverse of each other. We'll use these
functions later. functions later.
@ -261,12 +253,12 @@ constructing some new objects, see if they form a category. Not
surprisingly, algebras over a given endofunctor \code{F} form a surprisingly, algebras over a given endofunctor \code{F} form a
category. Objects in that category are algebras --- pairs consisting of category. Objects in that category are algebras --- pairs consisting of
a carrier object \code{a} and a morphism a carrier object \code{a} and a morphism
\code{F\ a\ ->\ a}, both from the original category \code{F a -> a}, both from the original category
\emph{C}. \emph{C}.
To complete the picture, we have to define morphisms in the category of To complete the picture, we have to define morphisms in the category of
F-algebras. A morphism must map one algebra \code{(a,\ f)} to another F-algebras. A morphism must map one algebra \code{(a, f)} to another
algebra \code{(b,\ g)}. We'll define it as a morphism \code{m} that algebra \code{(b, g)}. We'll define it as a morphism \code{m} that
maps the carriers --- it goes from \code{a} to \code{b} in the maps the carriers --- it goes from \code{a} to \code{b} in the
original category. Not any morphism will do: we want it to be compatible original category. Not any morphism will do: we want it to be compatible
with the two evaluators. (We call such a structure-preserving morphism a with the two evaluators. (We call such a structure-preserving morphism a
@ -276,18 +268,21 @@ F-algebras. First, notice that we can lift \code{m} to the mapping:
\begin{verbatim} \begin{verbatim}
F m :: F a -> F b F m :: F a -> F b
\end{verbatim} \end{verbatim}
we can then follow it with \code{g} to get to \code{b}. we can then follow it with \code{g} to get to \code{b}.
Equivalently, we can use \code{f} to go from \code{F\ a} to Equivalently, we can use \code{f} to go from \code{F a} to
\code{a} and then follow it with \code{m}. We want the two paths to \code{a} and then follow it with \code{m}. We want the two paths to
be equal: be equal:
\begin{verbatim} \begin{verbatim}
g ∘ F m = m ∘ f g ◦ F m = m ◦ f
\end{verbatim} \end{verbatim}
\includegraphics[width=2.09375in]{images/alg.png} \begin{figure}[H]
\centering
\includegraphics[width=50mm]{images/alg.png}
\end{figure}
\noindent
It's easy to convince yourself that this is indeed a category (hint: It's easy to convince yourself that this is indeed a category (hint:
identity morphisms from \emph{C} work just fine, and a composition of identity morphisms from \emph{C} work just fine, and a composition of
homomorphisms is a homomorphism). homomorphisms is a homomorphism).
@ -295,108 +290,124 @@ homomorphisms is a homomorphism).
An initial object in the category of F-algebras, if it exists, is called An initial object in the category of F-algebras, if it exists, is called
the \newterm{initial algebra}. Let's call the carrier of this initial the \newterm{initial algebra}. Let's call the carrier of this initial
algebra \code{i} and its evaluator algebra \code{i} and its evaluator
\code{j\ ::\ F\ i\ ->\ i}. It turns out that \code{j}, \code{j :: F i -> i}. It turns out that \code{j},
the evaluator of the initial algebra, is an isomorphism. This result is the evaluator of the initial algebra, is an isomorphism. This result is
known as Lambek's theorem. The proof relies on the definition of the known as Lambek's theorem. The proof relies on the definition of the
initial object, which requires that there be a unique homomorphism initial object, which requires that there be a unique homomorphism
\code{m} from it to any other F-algebra. Since \code{m} is a \code{m} from it to any other F-algebra. Since \code{m} is a
homomorphism, the following diagram must commute: homomorphism, the following diagram must commute:
\includegraphics{images/alg2.png} \begin{figure}[H]
\centering
\includegraphics[width=50mm]{images/alg2.png}
\end{figure}
Now let's construct an algebra whose carrier is \code{F\ i}. The \noindent
evaluator of such an algebra must be a morphism from \code{F\ (F\ i)} Now let's construct an algebra whose carrier is \code{F i}. The
to \code{F\ i}. We can easily construct such an evaluator simply by evaluator of such an algebra must be a morphism from \code{F (F i)}
to \code{F i}. We can easily construct such an evaluator simply by
lifting \code{j}: lifting \code{j}:
\begin{verbatim} \begin{verbatim}
F j :: F (F i) -> F i F j :: F (F i) -> F i
\end{verbatim} \end{verbatim}
Because \code{(i, j)} is the initial algebra, there must be a unique
Because \code{(i,\ j)} is the initial algebra, there must be a unique homomorphism \code{m} from it to \code{(F i, F j)}. The following
homomorphism \code{m} from it to \code{(F\ i,\ F\ j)}. The following
diagram must commute: diagram must commute:
\includegraphics{images/alg3a.png} \begin{figure}[H]
\centering
\includegraphics[width=50mm]{images/alg3a.png}
\end{figure}
\noindent
But we also have this trivially commuting diagram (both paths are the But we also have this trivially commuting diagram (both paths are the
same!): same!):
\includegraphics{images/alg3.png} \begin{figure}[H]
\centering
\includegraphics[width=50mm]{images/alg3.png}
\end{figure}
\noindent
which can be interpreted as showing that \code{j} is a homomorphism of which can be interpreted as showing that \code{j} is a homomorphism of
algebras, mapping \code{(F\ i,\ F\ j)} to \code{(i,\ j)}. We can algebras, mapping \code{(F i, F j)} to \code{(i, j)}. We can
glue these two diagrams together to get: glue these two diagrams together to get:
\includegraphics[width=3.12500in]{images/alg4.png} \begin{figure}[H]
\centering
\includegraphics[width=80mm]{images/alg4.png}
\end{figure}
\noindent
This diagram may, in turn, be interpreted as showing that This diagram may, in turn, be interpreted as showing that
\code{j\ \ m} is a homomorphism of algebras. Only in this case the \code{jm} is a homomorphism of algebras. Only in this case the
two algebras are the same. Moreover, because \code{(i,\ j)} is two algebras are the same. Moreover, because \code{(i, j)} is
initial, there can only be one homomorphism from it to itself, and initial, there can only be one homomorphism from it to itself, and
that's the identity morphism \code{idi} --- which we know is a that's the identity morphism \code{id\textsubscript{i}} --- which we know is a
homomorphism of algebras. Therefore \code{j\ \ m\ =\ idi}. Using this homomorphism of algebras. Therefore \code{j ◦ m = id\textsubscript{i}}. Using this
fact and the commuting property of the left diagram we can prove that fact and the commuting property of the left diagram we can prove that
\code{m\ \ j\ =\ idFi}. This shows that \code{m} is the inverse of \code{m ◦ j = id\textsubscript{Fi}}. This shows that \code{m} is the inverse of
\code{j} and therefore \code{j} is an isomorphism between \code{j} and therefore \code{j} is an isomorphism between
\code{F\ i} and \code{i}: \code{F i} and \code{i}:
\begin{verbatim}
F i ≅ i
\end{verbatim}
\begin{Verbatim}[commandchars=\\\{\}]
F i \ensuremath{\cong} i
\end{Verbatim}
But that is just saying that \code{i} is a fixed point of \code{F}. But that is just saying that \code{i} is a fixed point of \code{F}.
That's the formal proof behind the original hand-waving argument. That's the formal proof behind the original hand-waving argument.
Back to Haskell: We recognize \code{i} as our \code{Fix\ f}, Back to Haskell: We recognize \code{i} as our \code{Fix f},
\code{j} as our constructor \code{Fix}, and its inverse as \code{j} as our constructor \code{Fix}, and its inverse as
\code{unFix}. The isomorphism in Lambek's theorem tells us that, in \code{unFix}. The isomorphism in Lambek's theorem tells us that, in
order to get the initial algebra, we take the functor \code{f} and order to get the initial algebra, we take the functor \code{f} and
replace its argument \code{a} with \code{Fix\ f}. We also see why replace its argument \code{a} with \code{Fix f}. We also see why
the fixed point does not depend on \code{a}. the fixed point does not depend on \code{a}.
\subsection{Natural Numbers}\label{natural-numbers} \section{Natural Numbers}\label{natural-numbers}
Natural numbers can also be defined as an F-algebra. The starting point Natural numbers can also be defined as an F-algebra. The starting point
is the pair of morphisms: is the pair of morphisms:
\begin{verbatim} \begin{verbatim}
zero :: 1 -> N succ :: N -> N zero :: 1 -> N
succ :: N -> N
\end{verbatim} \end{verbatim}
The first one picks the zero, and the second one maps all numbers to The first one picks the zero, and the second one maps all numbers to
their successors. As before, we can combine the two into one: their successors. As before, we can combine the two into one:
\begin{verbatim} \begin{verbatim}
1 + N -> N 1 + N -> N
\end{verbatim} \end{verbatim}
The left hand side defines a functor which, in Haskell, can be written The left hand side defines a functor which, in Haskell, can be written
like this: like this:
\begin{verbatim} \begin{verbatim}
data NatF a = ZeroF | SuccF a data NatF a = ZeroF | SuccF a
\end{verbatim} \end{verbatim}
The fixed point of this functor (the initial algebra that it generates) The fixed point of this functor (the initial algebra that it generates)
can be encoded in Haskell as: can be encoded in Haskell as:
\begin{verbatim} \begin{verbatim}
data Nat = Zero | Succ Nat data Nat = Zero | Succ Nat
\end{verbatim} \end{verbatim}
A natural number is either zero or a successor of another number. This A natural number is either zero or a successor of another number. This
is known as the Peano representation for natural numbers. is known as the Peano representation for natural numbers.
\section{Catamorphisms}\label{catamorphisms} \section{Catamorphisms}\label{catamorphisms}
Let's rewrite the initiality condition using Haskell notation. We call Let's rewrite the initiality condition using Haskell notation. We call
the initial algebra \code{Fix\ f}. Its evaluator is the contructor the initial algebra \code{Fix f}. Its evaluator is the contructor
\code{Fix}. There is a unique morphism \code{m} from the initial \code{Fix}. There is a unique morphism \code{m} from the initial
algebra to any other algebra over the same functor. Let's pick an algebra to any other algebra over the same functor. Let's pick an
algebra whose carrier is \code{a} and the evaluator is \code{alg}. algebra whose carrier is \code{a} and the evaluator is \code{alg}.
\includegraphics{images/alg5.png}\\ \begin{figure}[H]
\centering
\includegraphics[width=60mm]{images/alg5.png}
\end{figure}
\noindent
By the way, notice what \code{m} is: It's an evaluator for the fixed By the way, notice what \code{m} is: It's an evaluator for the fixed
point, an evaluator for the whole recursive expression tree. Let's find point, an evaluator for the whole recursive expression tree. Let's find
a general way of implementing it. a general way of implementing it.
@ -405,18 +416,21 @@ Lambek's theorem tells us that the constructor \code{Fix} is an
isomorphism. We called its inverse \code{unFix}. We can therefore flip isomorphism. We called its inverse \code{unFix}. We can therefore flip
one arrow in this diagram to get: one arrow in this diagram to get:
\includegraphics{images/alg6.png} \begin{figure}[H]
\centering
\includegraphics[width=60mm]{images/alg6.png}
\end{figure}
\noindent
Let's write down the commutation condition for this diagram: Let's write down the commutation condition for this diagram:
\begin{verbatim} \begin{verbatim}
m = alg . fmap m . unFix m = alg . fmap m . unFix
\end{verbatim} \end{verbatim}
We can interpret this equation as a recursive definition of \code{m}. We can interpret this equation as a recursive definition of \code{m}.
The recursion is bound to terminate for any finite tree created using The recursion is bound to terminate for any finite tree created using
the functor \code{f}. We can see that by noticing that the functor \code{f}. We can see that by noticing that
\code{fmap\ m} operates underneath the top layer of the functor \code{fmap m} operates underneath the top layer of the functor
\code{f}. In other words, it works on the children of the original \code{f}. In other words, it works on the children of the original
tree. The children are always one level shallower than the original tree. The children are always one level shallower than the original
tree. tree.
@ -435,25 +449,25 @@ gives us the function we called \code{m}. This higher order function
is called a catamorphism: is called a catamorphism:
\begin{verbatim} \begin{verbatim}
cata :: Functor f => (f a -> a) -> Fix f -> a cata alg = alg . fmap (cata alg) . unFix cata :: Functor f => (f a -> a) -> Fix f -> a
cata alg = alg . fmap (cata alg) . unFix
\end{verbatim} \end{verbatim}
Let's see an example of that. Take the functor that defines natural Let's see an example of that. Take the functor that defines natural
numbers: numbers:
\begin{verbatim} \begin{verbatim}
data NatF a = ZeroF | SuccF a data NatF a = ZeroF | SuccF a
\end{verbatim} \end{verbatim}
Let's pick \code{(Int, Int)} as the carrier type and define our
Let's pick \code{(Int,\ Int)} as the carrier type and define our
algebra as: algebra as:
\begin{verbatim} \begin{verbatim}
fib :: NatF (Int, Int) -> (Int, Int) fib ZeroF = (1, 1) fib (SuccF (m, n)) = (n, m + n) fib :: NatF (Int, Int) -> (Int, Int)
fib ZeroF = (1, 1)
fib (SuccF (m, n)) = (n, m + n)
\end{verbatim} \end{verbatim}
You can easily convince yourself that the catamorphism for this algebra, You can easily convince yourself that the catamorphism for this algebra,
\code{cata\ fib}, calculates Fibonacci numbers. \code{cata fib}, calculates Fibonacci numbers.
In general, an algebra for \code{NatF} defines a recurrence relation: In general, an algebra for \code{NatF} defines a recurrence relation:
the value of the current element in terms of the previous element. A the value of the current element in terms of the previous element. A
@ -466,14 +480,12 @@ A list of \code{e} is the initial algebra of the following functor:
\begin{verbatim} \begin{verbatim}
data ListF e a = NilF | ConsF e a data ListF e a = NilF | ConsF e a
\end{verbatim} \end{verbatim}
Indeed, replacing the variable \code{a} with the result of recursion, Indeed, replacing the variable \code{a} with the result of recursion,
which we'll call \code{List\ e}, we get: which we'll call \code{List e}, we get:
\begin{verbatim} \begin{verbatim}
data List e = Nil | Cons e (List e) data List e = Nil | Cons e (List e)
\end{verbatim} \end{verbatim}
An algebra for a list functor picks a particular carrier type and An algebra for a list functor picks a particular carrier type and
defines a function that does pattern matching on the two constructors. defines a function that does pattern matching on the two constructors.
Its value for \code{NilF} tells us how to evaluate an empty list, and Its value for \code{NilF} tells us how to evaluate an empty list, and
@ -484,10 +496,11 @@ For instance, here's an algebra that can be used to calculate the length
of a list (the carrier type is \code{Int}): of a list (the carrier type is \code{Int}):
\begin{verbatim} \begin{verbatim}
lenAlg :: ListF e Int -> Int lenAlg (ConsF e n) = n + 1 lenAlg NilF = 0 lenAlg :: ListF e Int -> Int
lenAlg (ConsF e n) = n + 1
lenAlg NilF = 0
\end{verbatim} \end{verbatim}
Indeed, the resulting catamorphism \code{cata lenAlg} calculates the
Indeed, the resulting catamorphism \code{cata\ lenAlg} calculates the
length of a list. Notice that the evaluator is a combination of (1) a length of a list. Notice that the evaluator is a combination of (1) a
function that takes a list element and an accumulator and returns a new function that takes a list element and an accumulator and returns a new
accumulator, and (2) a starting value, here zero. The type of the value accumulator, and (2) a starting value, here zero. The type of the value
@ -498,22 +511,21 @@ Compare this to the traditional Haskell definition:
\begin{verbatim} \begin{verbatim}
length = foldr (\e n -> n + 1) 0 length = foldr (\e n -> n + 1) 0
\end{verbatim} \end{verbatim}
The two arguments to \code{foldr} are exactly the two components of The two arguments to \code{foldr} are exactly the two components of
the algebra. the algebra.
Let's try another example: Let's try another example:
\begin{verbatim} \begin{verbatim}
sumAlg :: ListF Double Double -> Double sumAlg (ConsF e s) = e + s sumAlg NilF = 0.0 sumAlg :: ListF Double Double -> Double
sumAlg (ConsF e s) = e + s
sumAlg NilF = 0.0
\end{verbatim} \end{verbatim}
Again, compare this with: Again, compare this with:
\begin{verbatim} \begin{verbatim}
sum = foldr (\e s -> e + s) 0.0 sum = foldr (\e s -> e + s) 0.0
\end{verbatim} \end{verbatim}
As you can see, \code{foldr} is just a convenient specialization of a As you can see, \code{foldr} is just a convenient specialization of a
catamorphism to lists. catamorphism to lists.
@ -525,23 +537,25 @@ direction of the morphism is reversed:
\begin{verbatim} \begin{verbatim}
a -> F a a -> F a
\end{verbatim} \end{verbatim}
Coalgebras for a given functor also form a category, with homomorphisms Coalgebras for a given functor also form a category, with homomorphisms
preserving the coalgebraic structure. The terminal object preserving the coalgebraic structure. The terminal object
\code{(t,\ u)} in that category is called the terminal (or final) \code{(t, u)} in that category is called the terminal (or final)
coalgebra. For every other algebra \code{(a,\ f)} there is a unique coalgebra. For every other algebra \code{(a, f)} there is a unique
homomorphism \code{m} that makes the following diagram commute: homomorphism \code{m} that makes the following diagram commute:
\includegraphics{images/alg7.png} \begin{figure}[H]
\centering
\includegraphics[width=50mm]{images/alg7.png}
\end{figure}
\noindent
A terminal colagebra is a fixed point of the functor, in the sense that A terminal colagebra is a fixed point of the functor, in the sense that
the morphism \code{u\ ::\ t\ ->\ F\ t} is an isomorphism the morphism \code{u :: t -> F t} is an isomorphism
(Lambek's theorem for coalgebras): (Lambek's theorem for coalgebras):
\begin{verbatim} \begin{Verbatim}[commandchars=\\\{\}]
F t ≅ t F t \ensuremath{\cong} t
\end{verbatim} \end{Verbatim}
A terminal coalgebra is usually interpreted in programming as a recipe A terminal coalgebra is usually interpreted in programming as a recipe
for generating (possibly infinite) data structures or transition for generating (possibly infinite) data structures or transition
systems. systems.
@ -550,24 +564,23 @@ Just like a catamorphism can be used to evaluate an initial algebra, an
anamorphism can be used to coevaluate a terminal coalgebra: anamorphism can be used to coevaluate a terminal coalgebra:
\begin{verbatim} \begin{verbatim}
ana :: Functor f => (a -> f a) -> a -> Fix f ana coalg = Fix . fmap (ana coalg) . coalg ana :: Functor f => (a -> f a) -> a -> Fix f
ana coalg = Fix . fmap (ana coalg) . coalg
\end{verbatim} \end{verbatim}
A canonical example of a coalgebra is based on a functor whose fixed A canonical example of a coalgebra is based on a functor whose fixed
point is an infinite stream of elements of type \code{e}. This is the point is an infinite stream of elements of type \code{e}. This is the
functor: functor:
\begin{verbatim} \begin{verbatim}
data StreamF e a = StreamF e a deriving Functor data StreamF e a = StreamF e a
deriving Functor
\end{verbatim} \end{verbatim}
and this is its fixed point: and this is its fixed point:
\begin{verbatim} \begin{verbatim}
data Stream e = Stream e (Stream e) data Stream e = Stream e (Stream e)
\end{verbatim} \end{verbatim}
A coalgebra for \code{StreamF e} is a function that takes the seed of
A coalgebra for \code{StreamF\ e} is a function that takes the seed of
type \code{a} and produces a pair (\code{StreamF} is a fancy name type \code{a} and produces a pair (\code{StreamF} is a fancy name
for a pair) consisting of an element and the next seed. for a pair) consisting of an element and the next seed.
@ -584,24 +597,26 @@ the sieve of Eratosthenes. This coalgebra is implemented by the
following function: following function:
\begin{verbatim} \begin{verbatim}
era :: [Int] -> StreamF Int [Int] era (p : ns) = StreamF p (filter (notdiv p) ns) where notdiv p n = n `mod` p /= 0 era :: [Int] -> StreamF Int [Int]
era (p : ns) = StreamF p (filter (notdiv p) ns)
where notdiv p n = n `mod` p /= 0
\end{verbatim} \end{verbatim}
The anamorphism for this coalgebra generates the list of primes: The anamorphism for this coalgebra generates the list of primes:
\begin{verbatim} \begin{verbatim}
primes = ana era [2..] primes = ana era [2..]
\end{verbatim} \end{verbatim}
A stream is an infinite list, so it should be possible to convert it to A stream is an infinite list, so it should be possible to convert it to
a Haskell list. To do that, we can use the same functor \code{StreamF} a Haskell list. To do that, we can use the same functor \code{StreamF}
to form an algebra, and we can run a catamorphism over it. For instance, to form an algebra, and we can run a catamorphism over it. For instance,
this is a catamorphism that converts a stream to a list: this is a catamorphism that converts a stream to a list:
\begin{verbatim} \begin{verbatim}
toListC :: Fix (StreamF e) -> [e] toListC = cata al where al :: StreamF e [e] -> [e] al (StreamF e a) = e : a toListC :: Fix (StreamF e) -> [e]
toListC = cata al
where al :: StreamF e [e] -> [e]
al (StreamF e a) = e : a
\end{verbatim} \end{verbatim}
Here, the same fixed point is simultaneously an initial algebra and a Here, the same fixed point is simultaneously an initial algebra and a
terminal coalgebra for the same endofunctor. It's not always like this, terminal coalgebra for the same endofunctor. It's not always like this,
in an arbitrary category. In general, an endofunctor may have many (or in an arbitrary category. In general, an endofunctor may have many (or
@ -616,16 +631,15 @@ functor is modified to produce a \code{Maybe} pair:
\begin{verbatim} \begin{verbatim}
unfoldr :: (b -> Maybe (a, b)) -> b -> [a] unfoldr :: (b -> Maybe (a, b)) -> b -> [a]
\end{verbatim} \end{verbatim}
The value of \code{Nothing} will terminate the generation of the list. The value of \code{Nothing} will terminate the generation of the list.
An interesting case of a coalgebra is related to lenses. A lens can be An interesting case of a coalgebra is related to lenses. A lens can be
represented as a pair of a getter and a setter: represented as a pair of a getter and a setter:
\begin{verbatim} \begin{verbatim}
set :: a -> s -> a get :: a -> s set :: a -> s -> a
get :: a -> s
\end{verbatim} \end{verbatim}
Here, \code{a} is usually some product data type with a field of type Here, \code{a} is usually some product data type with a field of type
\code{s}. The getter retrieves the value of that field and the setter \code{s}. The getter retrieves the value of that field and the setter
replaces this field with a new value. These two functions can be replaces this field with a new value. These two functions can be
@ -634,24 +648,21 @@ combined into one:
\begin{verbatim} \begin{verbatim}
a -> (s, s -> a) a -> (s, s -> a)
\end{verbatim} \end{verbatim}
We can rewrite this function further as: We can rewrite this function further as:
\begin{verbatim} \begin{verbatim}
a -> Store s a a -> Store s a
\end{verbatim} \end{verbatim}
where we have defined a functor: where we have defined a functor:
\begin{verbatim} \begin{verbatim}
data Store s a = Store (s -> a) s data Store s a = Store (s -> a) s
\end{verbatim} \end{verbatim}
Notice that this is not a simple algebraic functor constructed from sums Notice that this is not a simple algebraic functor constructed from sums
of products. It involves an exponential \code{as}. of products. It involves an exponential \code{as}.
A lens is a coalgebra for this functor with the carrier type \code{a}. A lens is a coalgebra for this functor with the carrier type \code{a}.
We've seen before that \code{Store\ s} is also a comonad. It turns out We've seen before that \code{Store s} is also a comonad. It turns out
that a well-behaved lens corresponds to a coalgebra that is compatible that a well-behaved lens corresponds to a coalgebra that is compatible
with the comonad structure. We'll talk about this in the next section. with the comonad structure. We'll talk about this in the next section.
@ -662,12 +673,12 @@ with the comonad structure. We'll talk about this in the next section.
\item \item
Implement the evaluation function for a ring of polynomials of one Implement the evaluation function for a ring of polynomials of one
variable. You can represent a polynomial as a list of coefficients in variable. You can represent a polynomial as a list of coefficients in
front of powers of \code{x}. For instance, \code{4x2-1} would be front of powers of \code{x}. For instance, \code{4x\textsuperscript{2}-1} would be
represented as (starting with the zero'th power) represented as (starting with the zero'th power)
\code{{[}-1,\ 0,\ 4{]}}. \code{{[}-1, 0, 4{]}}.
\item \item
Generalize the previous construction to polynomials of many Generalize the previous construction to polynomials of many
independent variables, like \code{x2y-3y3z}. independent variables, like \code{x\textsuperscript{2}y-3y\textsuperscript{3}z}.
\item \item
Implement the algebra for the ring of 2×2 matrices. Implement the algebra for the ring of 2×2 matrices.
\item \item
@ -676,8 +687,4 @@ with the comonad structure. We'll talk about this in the next section.
\item \item
Use \code{unfoldr} to generate a list of the first \code{n} Use \code{unfoldr} to generate a list of the first \code{n}
primes. primes.
\end{enumerate} \end{enumerate}
Next:
\href{https://bartoszmilewski.com/2017/03/14/algebras-for-monads/}{Algebras
for Monads}.

View File

@ -95,7 +95,7 @@ PDF compiled by @url{https://github.com/hmemcpy/milewski-ctfp-pdf, Igal Tabachni
\chapter{Products and Coproducts}\label{products-and-coproducts} \chapter{Products and Coproducts}\label{products-and-coproducts}
\subfile{content/1.5/Products and Coproducts} \subfile{content/1.5/Products and Coproducts}
\chapter{Simple Algebraic Data Types} \chapter{Simple Algebraic Data Types}\label{simple-algebraic-data-types}
\subfile{content/1.6/Simple Algebraic Data Types} \subfile{content/1.6/Simple Algebraic Data Types}
\chapter{Functors} \chapter{Functors}
@ -135,6 +135,10 @@ PDF compiled by @url{https://github.com/hmemcpy/milewski-ctfp-pdf, Igal Tabachni
\chapter{Comonads}\label{comonads} \chapter{Comonads}\label{comonads}
\subfile{content/3.7/Comonads} \subfile{content/3.7/Comonads}
\chapter{F-Algebras}\label{f-algebras}
\subfile{content/3.8/F-Algebras}
\backmatter \backmatter
@unnumbered Acknowledgments @unnumbered Acknowledgments