hmemcpy/milewski-ctfp-pdf
1
1
Fork 0
mirror of https://github.com/hmemcpy/milewski-ctfp-pdf.git synced 2024-11-22 11:32:00 +03:00
Code Issues Projects Releases Wiki Activity

More tweaks (subsection -> section)

Browse Source
This commit is contained in:
Igal Tabachnik 2017-09-23 23:32:46 +03:00
parent 45d8536ffa
commit 2662dd8b6e
32 changed files with 216 additions and 220 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

BIN
ctfp.pdf
View File

Binary file not shown.

8
src/content/1.1/Category - The Essence of Composition.tex
View File

@ -16,7 +16,7 @@ object B to object C, then there must be an arrow --- their composition
\caption{In a category, if there is an arrow going from A to B and an arrow going from B to C then there must also be a direct arrow from A to C that is their composition. This diagram is not a full category because it’s missing identity morphisms (see later).}
\end{figure}
\subsection{Arrows as Functions}\label{arrows-as-functions}
\section{Arrows as Functions}\label{arrows-as-functions}
Is this already too much abstract nonsense? Do not despair. Let's talk
concretes. Think of arrows, which are also called \newterm{morphisms}, as
@ -96,7 +96,7 @@ of\ldots{}'' A function type is created by inserting an arrow between
two types. You compose two functions by inserting a period between them
(or a Unicode circle).
\subsection{Properties of Composition}\label{properties-of-composition}
\section{Properties of Composition}\label{properties-of-composition}
There are two extremely important properties that the composition in any
category must satisfy.
@ -203,7 +203,7 @@ To summarize: A category consists of objects and arrows (morphisms).
Arrows can be composed, and the composition is associative. Every object
has an identity arrow that serves as a unit under composition.
\subsection{Composition is the Essence of
\section{Composition is the Essence of
Programming}\label{composition-is-the-essence-of-programming}
Functional programmers have a peculiar way of approaching problems. They
@ -268,7 +268,7 @@ you have to dig into the implementation of the object in order to
understand how to compose it with other objects, you've lost the
advantages of your programming paradigm.
\subsection{Challenges}\label{challenges}
\section{Challenges}\label{challenges}
\begin{enumerate}
\tightlist

14
src/content/1.10/Natural Transformations.tex
View File

@ -125,7 +125,7 @@ like saying they are the same. \newterm{Natural isomorphism} is defined as
a natural transformation whose components are all isomorphisms
(invertible morphisms).
\subsection{Polymorphic Functions}\label{polymorphic-functions}
\section{Polymorphic Functions}\label{polymorphic-functions}
We talked about the role of functors (or, more specifically,
endofunctors) in programming. They correspond to type constructors that
@ -391,7 +391,7 @@ two elements of the \code{Maybe\ ()} type, which are \code{Nothing}
and \code{Just\ ()}. We'll come back to the Yoneda lemma later ---
this was just a little teaser.
\subsection{Beyond Naturality}\label{beyond-naturality}
\section{Beyond Naturality}\label{beyond-naturality}
A parametrically polymorphic function between two functors (including
the edge case of the \code{Const} functor) is always a natural
@ -467,7 +467,7 @@ transformation. Interestingly, there is a generalization of natural
transformations, called dinatural transformations, that deals with such
cases. We'll get to them when we discuss ends.
\subsection{Functor Category}\label{functor-category}
\section{Functor Category}\label{functor-category}
Now that we have mappings between functors --- natural transformations
--- it's only natural to ask the question whether functors form a
@ -586,7 +586,7 @@ And by ``object'' in \textbf{Cat} I mean a category, so
D\textsuperscript{C} is a category, which we can identify with the
functor category between C and D.
\subsection{2-Categories}\label{categories}
\section{2-Categories}\label{categories}
With that out of the way, let's have a closer look at \textbf{Cat}. By
definition, any Hom-set in \textbf{Cat} is a set of functors. But, as we
@ -779,7 +779,7 @@ Similarly:
is a horizontal composition of α after 1\textsubscript{F}.
\subsection{Conclusion}\label{conclusion}
\section{Conclusion}\label{conclusion}
This concludes the first part of the book. We've learned the basic
vocabulary of category theory. You may think of objects and categories
@ -805,7 +805,7 @@ Functors may be looked upon as objects in the functor category. As such,
they become sources and targets of morphisms: natural transformations. A
natural transformation is a special type of polymorphic function.
\subsection{Challenges}\label{challenges}
\section{Challenges}\label{challenges}
\begin{enumerate}
\item
@ -847,7 +847,7 @@ Next:
\href{https://bartoszmilewski.com/2015/04/15/category-theory-and-declarative-programming/}{Declarative
Programming}.
\subsection{Acknowledgments}\label{acknowledgments}
\section{Acknowledgments}\label{acknowledgments}
I'd like to thank Gershom Bazerman for checking my math and logic, and
André van Meulebrouck, who has been volunteering his editing help.\\

86
src/content/1.2/Types and Functions.tex
View File

@ -1,7 +1,7 @@
\lettrine[lhang=0.17]{T}{he category of types and functions} plays an important role in
programming, so let's talk about what types are and why we need them.
\subsection{Who Needs Types?}\label{who-needs-types}
\section{Who Needs Types?}\label{who-needs-types}
There seems to be some controversy about the advantages of static vs.
dynamic and strong vs. weak typing. Let me illustrate these choices with
@ -35,7 +35,7 @@ The analog of a type checker would go even further by making sure that,
once Romeo is declared a human being, he doesn't sprout leaves or trap
photons in his powerful gravitational field.
\subsection{Types Are About
\section{Types Are About
Composability}\label{types-are-about-composability}
Category theory is about composing arrows. But not any two arrows can be
@ -95,7 +95,7 @@ sites. Unit testing may catch some of the mismatches, but testing is
almost always a probabilistic rather than a deterministic process.
Testing is a poor substitute for proof.
\subsection{What Are Types?}\label{what-are-types}
\section{What Are Types?}\label{what-are-types}
The simplest intuition for types is that they are sets of values. The
type \code{Bool} (remember, concrete types start with a capital letter
@ -189,7 +189,7 @@ okay to ignore non-terminating functions and bottoms, and treat
John Hughes, Patrik Jansson, Jeremy Gibbons, \href{http://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf}{
Fast and Loose Reasoning is Morally Correct}. This paper provides justification for ignoring bottoms in most contexts.}
\subsection{Why Do We Need a Mathematical
\section{Why Do We Need a Mathematical
Model?}\label{why-do-we-need-a-mathematical-model}
As a programmer you are intimately familiar with the syntax and grammar
@ -239,14 +239,15 @@ usually quite simple, if not trivial.
Consider the definition of a factorial function in Haskell, which is a
language quite amenable to denotational semantics:
\mint{haskell}|fact n = product [1..n]|
\begin{verbatim}
fact n = product [1..n]
\end{verbatim}
The expression \code{{[}1..n{]}} is a list of integers from \code{1} to \code{n}.
The function \code{product} multiplies all elements of a list. That's
just like a definition of factorial taken from a math text. Compare this
with C:
\begin{minted}{c}
\begin{verbatim}
int fact(int n) {
int i;
int result = 1;
@ -254,8 +255,7 @@ int fact(int n) {
result *= i;
return result;
}
\end{minted}
\end{verbatim}
Need I say more?
Okay, I'll be the first to admit that this was a cheap shot! A factorial
@ -283,7 +283,7 @@ even when writing web applications for the health system, you may
appreciate the thought that functions and algorithms from the Haskell
standard library come with proofs of correctness.
\subsection{Pure and Dirty Functions}\label{pure-and-dirty-functions}
\section{Pure and Dirty Functions}\label{pure-and-dirty-functions}
The things we call functions in C++ or any other imperative language,
are not the same things mathematicians call functions. A mathematical
@ -311,7 +311,7 @@ about side effects separately. Later we'll see how monads let us model
all kinds of effects using only pure functions. So we really don't lose
anything by restricting ourselves to mathematical functions.
\subsection{Examples of Types}\label{examples-of-types}
\section{Examples of Types}\label{examples-of-types}
Once you realize that types are sets, you can think of some rather
exotic types. For instance, what's the type corresponding to an empty
@ -325,8 +325,9 @@ return, there are no restrictions whatsoever. It can return any type
it's a function that's polymorphic in the return type. Haskellers have a
name for it:
\mint{haskell}|absurd :: Void -> a|
\begin{verbatim}
absurd :: Void -> a
\end{verbatim}
(Remember, \code{a} is a type variable that can stand for any type.)
The name is not coincidental. There is deeper interpretation of types
and functions in terms of logic called the Curry-Howard isomorphism. The
@ -341,8 +342,9 @@ Think of functions from and to this type. A function from \code{void}
can always be called. If it's a pure function, it will always return the
same result. Here's an example of such a function:
\mint{c}|int f44() { return 44; }|
\begin{verbatim}
int f44() { return 44; }
\end{verbatim}
You might think of this function as taking ``nothing'', but as we've
just seen, a function that takes ``nothing'' can never be called because
there is no value representing ``nothing.'' So what does this function
@ -355,19 +357,19 @@ because of the Haskell's love of terseness, the same symbol \code{()}
is used for the type, the constructor, and the only value corresponding
to a singleton set. So here's this function in Haskell:
\begin{minted}{haskell}
\begin{verbatim}
f44 :: () -> Integer
f44 () = 44
\end{minted}
\end{verbatim}
The first line declares that \code{f44} takes the type \code{()},
pronounced ``unit,'' into the type \code{Integer}. The second line
defines \code{f44} by pattern matching the only constructor for unit,
namely \code{()}, and producing the number 44. You call this function
by providing the unit value \code{()}:
\mint{haskell}|f44 ()|
\begin{verbatim}
f44 ()
\end{verbatim}
Notice that every function of unit is equivalent to picking a single
element from the target type (here, picking the \code{Integer} 44). In
fact you could think of \code{f44} as a different representation for
@ -387,21 +389,19 @@ element of A to the single element of that singleton set. For every A
there is exactly one such function. Here's this function for
\code{Integer}:
\begin{minted}{haskell}
\begin{verbatim}
fInt :: Integer -> ()
fInt x = ()
\end{minted}
\end{verbatim}
You give it any integer, and it gives you back a unit. In the spirit of
terseness, Haskell lets you use the wildcard pattern, the underscore,
for an argument that is discarded. This way you don't have to invent a
name for it. So the above can be rewritten as:
\begin{minted}{haskell}
\begin{verbatim}
fInt :: Integer -> ()
fInt _ = ()
\end{minted}
\end{verbatim}
Notice that the implementation of this function not only doesn't depend
on the value passed to it, but it doesn't even depend on the type of the
argument.
@ -412,38 +412,34 @@ such functions with one equation using a type parameter instead of a
concrete type. What should we call a polymorphic function from any type
to unit type? Of course we'll call it \code{unit}:
\begin{minted}{haskell}
\begin{verbatim}
unit :: a -> ()
unit _ = ()
\end{minted}
\end{verbatim}
In C++ you would write this function as:
\begin{minted}{c++}
\begin{verbatim}
template<class T>
void unit(T) {}
\end{minted}
\end{verbatim}
Next in the typology of types is a two-element set. In C++ it's called
\code{bool} and in Haskell, predictably, \code{Bool}. The difference
is that in C++ \code{bool} is a built-in type, whereas in Haskell it
can be defined as follows:
\begin{minted}{haskell}
\begin{verbatim}
data Bool = True | False
\end{minted}
\end{verbatim}
(The way to read this definition is that \code{Bool} is either
\code{True} or \code{False}.) In principle, one should also be able
to define a Boolean type in C++ as an enumeration:
\begin{minted}{c++}
\begin{verbatim}
enum bool {
true,
false
};
\end{minted}
\end{verbatim}
but C++ \code{enum} is secretly an integer. The C++11
``\code{enum class}'' could have been used instead, but then you
would have to qualify its values with the class name, as in
@ -462,7 +458,7 @@ Boolean. The actual predicates are defined in \code{std::ctype} and
have the form \code{ctype::is(alpha,\ c)},
\code{ctype::is(digit,\ c)}, etc.
\subsection{Challenges}\label{challenges}
\section{Challenges}\label{challenges}
\begin{enumerate}
\tightlist
@ -495,25 +491,25 @@ have the form \code{ctype::is(alpha,\ c)},
\item
The factorial function from the example in the text.
\item
\begin{minted}{c++}
\begin{verbatim}
std::getchar()
\end{minted}
\end{verbatim}
\item
\begin{minted}{c++}
\begin{verbatim}
bool f() {
std::cout << "Hello!" << std::endl;
return true;
}
\end{minted}
\end{verbatim}
\item
\begin{minted}{c++}
\begin{verbatim}
int f(int x)
{
static int y = 0;
y += x;
return y;
}
\end{minted}
\end{verbatim}
\end{enumerate}
\item
How many different functions are there from \code{Bool} to

14
src/content/1.3/Categories Great and Small.tex
View File

@ -2,7 +2,7 @@
examples. Categories come in all shapes and sizes and often pop up in
unexpected places. We'll start with something really simple.
\subsection{No Objects}\label{no-objects}
\section{No Objects}\label{no-objects}
The most trivial category is one with zero objects and, consequently,
zero morphisms. It's a very sad category by itself, but it may be
@ -10,7 +10,7 @@ important in the context of other categories, for instance, in the
category of all categories (yes, there is one). If you think that an
empty set makes sense, then why not an empty category?
\subsection{Simple Graphs}\label{simple-graphs}
\section{Simple Graphs}\label{simple-graphs}
You can build categories just by connecting objects with arrows. You can
imagine starting with any directed graph and making it into a category
@ -34,7 +34,7 @@ given structure by extending it with a minimum number of items to
satisfy its laws (here, the laws of a category). We'll see more examples
of it in the future.
\subsection{Orders}\label{orders}
\section{Orders}\label{orders}
And now for something completely different! A category where a morphism
is a relation between objects: the relation of being less than or equal.
@ -71,7 +71,7 @@ and total orders because of sorting. Sorting algorithms, such as
quicksort, bubble sort, merge sort, etc., can only work correctly on
total orders. Partial orders can be sorted using topological sort.
\subsection{Monoid as Set}\label{monoid-as-set}
\section{Monoid as Set}\label{monoid-as-set}
Monoid is an embarrassingly simple but amazingly powerful concept. It's
the concept behind basic arithmetics: Both addition and multiplication
@ -243,7 +243,7 @@ std::string mappend(std::string s1, std::string s2) {
}
\end{minted}
\subsection{Monoid as Category}\label{monoid-as-category}
\section{Monoid as Category}\label{monoid-as-category}
That was the ``familiar'' definition of the monoid in terms of elements
of a set. But as you know, in category theory we try to get away from
@ -333,12 +333,12 @@ follow the rules of composition, and as points in a set. Here,
composition of morphisms in M translates into monoidal product in the
set \code{M(m, m)}.
\subsection{Acknowledgments}\label{acknowledgments}
\section{Acknowledgments}\label{acknowledgments}
I'd like to thank Andrew Sutton for rewriting my C++ monoid concept code
according to his and Bjarne Stroustrup's latest proposal.
\subsection{Challenges}\label{challenges}
\section{Challenges}\label{challenges}
\begin{enumerate}
\item

10
src/content/1.4/Kleisli Categories.tex
View File

@ -169,7 +169,7 @@ composition} itself. But composition is the essence of category theory,
so before we write more code, let's analyze the problem from the
categorical point of view.
\subsection{The Writer Category}\label{the-writer-category}
\section{The Writer Category}\label{the-writer-category}
The idea of embellishing the return types of a bunch of functions in
order to piggyback some additional functionality turns out to be very
@ -319,7 +319,7 @@ writer should be able to identify the bare minimum of constraints that
make the library work --- here the logging library's only requirement is
that the log have monoidal properties.
\subsection{Writer in Haskell}\label{writer-in-haskell}
\section{Writer in Haskell}\label{writer-in-haskell}
The same thing in Haskell is a little more terse, and we also get a lot
more help from the compiler. Let's start by defining the \code{Writer}
@ -420,7 +420,7 @@ process :: String -> Writer [String]
process = upCase >=> toWords
\end{minted}
\subsection{Kleisli Categories}\label{kleisli-categories}
\section{Kleisli Categories}\label{kleisli-categories}
You might have guessed that I haven't invented this category on the
spot. It's an example of the so called Kleisli category --- a category
@ -449,7 +449,7 @@ freedom which makes it possible to give simple denotational semantics to
programs that in imperative languages are traditionally implemented
using side effects.
\subsection{Challenge}\label{challenge}
\section{Challenge}\label{challenge}
A function that is not defined for all possible values of its argument
is called a partial function. It's not really a function in the
@ -496,7 +496,7 @@ Here's the challenge:
whenever possible.
\end{enumerate}
\subsection{Acknowledgments}\label{acknowledgments}
\section{Acknowledgments}\label{acknowledgments}
I'm grateful to Eric Niebler for reading the draft and providing the
clever implementation of \code{compose} that uses advanced features of

20
src/content/1.5/Products and Coproducts.tex
View File

@ -21,7 +21,7 @@ hits, you refine your query. That increases its \emph{precision}.
Finally, the search engine will rank the hits and, hopefully, the one
result that you're interested in will be at the top of the list.
\subsection{Initial Object}\label{initial-object}
\section{Initial Object}\label{initial-object}
The simplest shape is a single object. Obviously, there are as many
instances of this shape as there are objects in a given category. That's
@ -77,7 +77,7 @@ absurd :: Void -> a
It's this family of morphisms that makes \code{Void} the initial
object in the category of types.
\subsection{Terminal Object}\label{terminal-object}
\section{Terminal Object}\label{terminal-object}
Let's continue with the single-object pattern, but let's change the way
we rank the objects. We'll say that object \emph{a} is ``more terminal''
@ -135,7 +135,7 @@ no _ = False
Insisting on uniqueness gives us just the right precision to narrow down
the definition of the terminal object to just one type.
\subsection{Duality}\label{duality}
\section{Duality}\label{duality}
You can't help but to notice the symmetry between the way we defined the
initial object and the terminal object. The only difference between the
@ -163,7 +163,7 @@ the arrows twice gets us back to the original state.
It follows then that a terminal object is the initial object in the
opposite category.
\subsection{Isomorphisms}\label{isomorphisms}
\section{Isomorphisms}\label{isomorphisms}
As programmers, we are well aware that defining equality is a nontrivial
task. What does it mean for two objects to be equal? Do they have to
@ -235,7 +235,7 @@ there could be more than one isomorphism between two objects, but that's
not the case here. This ``uniqueness up to unique isomorphism'' is the
important property of all universal constructions.
\subsection{Products}\label{products}
\section{Products}\label{products}
The next universal construction is that of a product. We know what a
cartesian product of two sets is: it's a set of pairs. But what's the
@ -472,7 +472,7 @@ factorizer :: (c -> a) -> (c -> b) -> (c -> (a, b))
factorizer p q = \x -> (p x, q x)
\end{verbatim}
\subsection{Coproduct}\label{coproduct}
\section{Coproduct}\label{coproduct}
Like every construction in category theory, the product has a dual,
which is called the coproduct. When we reverse the arrows in the product
@ -607,7 +607,7 @@ factorizer i j (Left a) = i a
factorizer i j (Right b) = j b
\end{verbatim}
\subsection{Asymmetry}\label{asymmetry}
\section{Asymmetry}\label{asymmetry}
We've seen two set of dual definitions: The definition of a terminal
object can be obtained from the definition of the initial object by
@ -704,7 +704,7 @@ collapsing. They are called \newterm{bijections} and they are truly
symmetric, because they are invertible. In the category of sets, an
isomorphism is the same as a bijection.
\subsection{Challenges}\label{challenges}
\section{Challenges}\label{challenges}
\begin{enumerate}
\tightlist
@ -755,7 +755,7 @@ int j(bool b) { return b? 0: 1; }
allows multiple acceptable morphisms from it to \code{Either}.
\end{enumerate}
\subsection{Bibliography}\label{bibliography}
\section{Bibliography}\label{bibliography}
\begin{enumerate}
\tightlist
@ -765,7 +765,7 @@ int j(bool b) { return b? 0: 1; }
Coproducts} video.
\end{enumerate}
\subsection{Acknowledments}\label{acknowledments}
\section{Acknowledments}\label{acknowledments}
I'm grateful to Gershom Bazerman for reviewing this post before
publication and for stimulating discussions.

12
src/content/1.6/Simple Algebraic Data Types.tex
View File

@ -12,7 +12,7 @@ large subset of composite types.
Let's have a closer look at product and sum types as they appear in
programming.
\subsection{Product Types}\label{product-types}
\section{Product Types}\label{product-types}
The canonical implementation of a product of two types in a programming
language is a pair. In Haskell, a pair is a primitive type constructor;
@ -192,7 +192,7 @@ and error prone --- keeping track of which component represents what.
It's often preferable to give names to components. A product type with
named fields is called a record in Haskell, and a \code{struct} in C.
\subsection{Records}\label{records}
\section{Records}\label{records}
Let's have a look at a simple example. We want to describe chemical
elements by combining two strings, name and symbol; and an integer, the
@ -264,7 +264,7 @@ startsWithSymbol e = symbol e `isPrefixOf` name e
The parentheses could be omitted in this case, because an infix operator
has lower precedence than a function call.
\subsection{Sum Types}\label{sum-types}
\section{Sum Types}\label{sum-types}
Just as the product in the category of sets gives rise to product types,
the coproduct gives rise to sum types. The canonical implementation of a
@ -457,7 +457,7 @@ You will rarely see \code{union} used as a sum type in C++ because of
severe limitations on what can go into a union. You can't even put a
\code{std::string} into a union because it has a copy constructor.
\subsection{Algebra of Types}\label{algebra-of-types}
\section{Algebra of Types}\label{algebra-of-types}
Taken separately, product and sum types can be used to define a variety
of useful data structures, but the real strength comes from combining
@ -649,7 +649,7 @@ This analogy goes deeper, and is the basis of the Curry-Howard
isomorphism between logic and type theory. We'll come back to it when we
talk about function types.
\subsection{Challenges}\label{challenges}
\section{Challenges}\label{challenges}
\begin{enumerate}
\tightlist
@ -700,7 +700,7 @@ circ (Rect d h) = 2.0 * (d + h)
according to our translation table.
\end{enumerate}
\subsection{Acknowledments}\label{acknowledments}
\section{Acknowledments}\label{acknowledments}
Thanks go to Gershom Bazerman for reviewing this post and helpful
comments.

10
src/content/1.7/Functors.tex
View File

@ -84,7 +84,7 @@ maps every morphism in the source category to the identity morphism
everything into one singularity. We'll see more of this functor when we
discuss limits and colimits.
\subsection{Functors in Programming}\label{functors-in-programming}
\section{Functors in Programming}\label{functors-in-programming}
Let's get down to earth and talk about programming. We have our category
of types and functions. We can talk about functors that map this
@ -549,7 +549,7 @@ This combination of the type constructor \code{(-\textgreater{})\ r}
with the above implementation of \code{fmap} is called the reader
functor.
\subsection{Functors as Containers}\label{functors-as-containers}
\section{Functors as Containers}\label{functors-as-containers}
We've seen some examples of functors in programming languages that
define general-purpose containers, or at least objects that contain some
@ -646,7 +646,7 @@ role in many constructions. In category theory, it's a special case of
the Δ\textsubscript{c} functor I mentioned earlier --- the endo-functor
case of a black hole. We'll be seeing more of it it in the future.
\subsection{Functor Composition}\label{functor-composition}
\section{Functor Composition}\label{functor-composition}
It's not hard to convince yourself that functors between categories
compose, just like functions between sets compose. A composition of two
@ -739,7 +739,7 @@ these things because I find it pretty amazing that we can recognize the
same structures repeating themselves at many levels of abstraction.
We'll see later that functors form categories as well.
\subsection{Challenges}\label{challenges}
\section{Challenges}\label{challenges}
\begin{enumerate}
\item
@ -762,7 +762,7 @@ fmap _ _ = Nothing
words, use \newterm{induction}).
\end{enumerate}
\subsection{Acknowledgments}\label{acknowledgments}
\section{Acknowledgments}\label{acknowledgments}
Gershom Bazerman is kind enough to keep reviewing these posts. I'm
grateful for his patience and insight.

18
src/content/1.8/Functoriality.tex
View File

@ -11,7 +11,7 @@ it's interesting to see which type constructors (which correspond to
mappings between objects in a category) can be extended to functors
(which include mappings between morphisms).
\subsection{Bifunctors}\label{bifunctors}
\section{Bifunctors}\label{bifunctors}
Since functors are morphisms in \newterm{Cat} (the category of categories),
a lot of intuitions about morphisms --- and functions in particular ---
@ -107,7 +107,7 @@ and \code{second} and accepting the default for \code{bimap} (of
course, you may implement all three of them, but then it's up to you to
make sure they are related to each other in this manner).
\subsection{Product and Coproduct
\section{Product and Coproduct
Bifunctors}\label{product-and-coproduct-bifunctors}
An important example of a bifunctor is the categorical product --- a
@ -162,7 +162,7 @@ morphisms. We are now one step closer to the full definition of a
monoidal category (we still need to learn about naturality, before we
can get there).
\subsection{Functorial Algebraic Data
\section{Functorial Algebraic Data
Types}\label{functorial-algebraic-data-types}
We've seen several examples of parameterized data types that turned out
@ -327,7 +327,7 @@ own typeclasses, but that's a bit more advanced. The idea though is the
same: You provide the behavior for the basic building blocks and sums
and products, and let the compiler figure out the rest.
\subsection{Functors in C++}\label{functors-in-c}
\section{Functors in C++}\label{functors-in-c}
If you are a C++ programmer, you obviously are on your own as far as
implementing functors goes. However, you should be able to recognize
@ -397,7 +397,7 @@ instance Functor Tree where fmap f (Leaf a) = Leaf (f a) fmap f (Node t t&apos;)
This implementation can also be automatically derived by the compiler.
\subsection{The Writer Functor}\label{the-writer-functor}
\section{The Writer Functor}\label{the-writer-functor}
I promised that I would come back to the
\href{https://bartoszmilewski.com/2014/12/23/kleisli-categories/}{Kleisli
@ -472,7 +472,7 @@ the way Haskell implements polymorphic functions. It's called
an implementation of \code{fmap} for a given type constructor, one
that preserves identity, then it must be unique.
\subsection{Covariant and Contravariant
\section{Covariant and Contravariant
Functors}\label{covariant-and-contravariant-functors}
Now that we've reviewed the writer functor, let's go back to the reader
@ -591,7 +591,7 @@ With it, we get:
contramap = flip (.)
\end{verbatim}
\subsection{Profunctors}\label{profunctors}
\section{Profunctors}\label{profunctors}
We've seen that the function-arrow operator is contravariant in its
first argument and covariant in the second. Is there a name for such a
@ -633,7 +633,7 @@ instance Profunctor (->) where dimap ab cd bc = cd . bc . ab lmap = flip (.) rma
Profunctors have their application in the Haskell lens library. We'll
see them again when we talk about ends and coends.
\subsection{Challenges}\label{challenges}
\section{Challenges}\label{challenges}
\begin{enumerate}
\item
@ -704,7 +704,7 @@ Next:
\href{https://bartoszmilewski.com/2015/03/13/function-types/}{Function
Types}.
\subsection{Acknowledgment}\label{acknowledgment}
\section{Acknowledgment}\label{acknowledgment}
As usual, big thanks go to Gershom Bazerman for reviewing this
article.\\

16
src/content/1.9/Function Types.tex
View File

@ -35,7 +35,7 @@ function types special. But there is a way, at least in some categories,
to construct objects that represent hom-sets. Such objects are called
\newterm{internal} hom-sets.
\subsection{Universal Construction}\label{universal-construction}
\section{Universal Construction}\label{universal-construction}
Let's forget for a moment that function types are sets and try to
construct a function type, or more generally, an internal hom-set, from
@ -213,7 +213,7 @@ This is why, in Haskell, we interpret the function type
\code{a-\textgreater{}b} as the categorical function object
\code{a⇒b}.
\subsection{Currying}\label{currying}
\section{Currying}\label{currying}
Let's have a second look at all the candidates for the function object.
This time, however, let's think of the morphism \code{g} as a function
@ -361,7 +361,7 @@ def catstr(s1: String)(s2: String) = s1 + s2
Of course that requires some amount of foresight or prescience on the
part of a library writer.
\subsection{Exponentials}\label{exponentials}
\section{Exponentials}\label{exponentials}
In mathematical literature, the function object, or the internal
hom-object between two objects \code{a} and \code{b}, is often
@ -418,7 +418,7 @@ explains the identification of Haskell's function type with the
categorical exponential object --- which corresponds more to our idea of
\emph{data}.
\subsection{Cartesian Closed
\section{Cartesian Closed
Categories}\label{cartesian-closed-categories}
Although I will continue using the category of sets as a model for types
@ -463,7 +463,7 @@ is called a \newterm{bicartesian closed} category. We'll see in the next
section that bicartesian closed categories, of which \textbf{Set} is a
prime example, have some interesting properties.
\subsection{Exponentials and Algebraic Data
\section{Exponentials and Algebraic Data
Types}\label{exponentials-and-algebraic-data-types}
The interpretation of function types as exponentials fits very well into
@ -591,7 +591,7 @@ It's pretty incredible how those simple high-school algebraic identities
can be lifted to category theory and have practical application in
functional programming.
\subsection{Curry-Howard Isomorphism}\label{curry-howard-isomorphism}
\section{Curry-Howard Isomorphism}\label{curry-howard-isomorphism}
I have already mentioned the correspondence between logic and algebraic
data types. The \code{Void} type and the unit type \code{()}
@ -716,7 +716,7 @@ coproducts, function types, and so on. And, as if to dispel any doubts,
the theory is being formulated in Coq and Agda. Computers are
revolutionizing the world in more than one way.
\subsection{Bibliography}\label{bibliography}
\section{Bibliography}\label{bibliography}
\begin{enumerate}
\tightlist
@ -732,7 +732,7 @@ Next:
\href{https://bartoszmilewski.com/2015/04/07/natural-transformations/}{Natural
Transformations}.
\subsection{Acknowledgments}\label{acknowledgments}
\section{Acknowledgments}\label{acknowledgments}
I'd like to thank Gershom Bazerman for checking my math and logic, and
André van Meulebrouck, who has been volunteering his editing help

2
src/content/2.1/Declarative Programming.tex
View File

@ -208,7 +208,7 @@ Next
\href{https://bartoszmilewski.com/2015/04/15/limits-and-colimits/}{Limits
and Colimits}.
\subsection{Acknowledgments}\label{acknowledgments}
\section{Acknowledgments}\label{acknowledgments}
I'd like to thank Gershom Bazerman for checking my math and logic, and
André van Meulebrouck, who has been volunteering his editing help.\\

12
src/content/2.2/Limits and Colimits.tex
View File

@ -158,7 +158,7 @@ diagram is the product of two objects. The product (together with the
two projections) contains the information about both objects. And being
universal means that it has no extraneous junk.
\subsection{Limit as a Natural
\section{Limit as a Natural
Isomorphism}\label{limit-as-a-natural-isomorphism}
There is still something unsatisfying about this definition of a limit.
@ -339,7 +339,7 @@ As a preview of coming attractions, let me mention that the set
category; so our natural isomorphism relates two hom-sets, which points
at an even more general relationship called an adjunction.
\subsection{Examples of Limits}\label{examples-of-limits}
\section{Examples of Limits}\label{examples-of-limits}
We've seen that the categorical product is a limit of a diagram
generated by a simple category we called \textbf{2}.
@ -571,7 +571,7 @@ twice :: (t -> t) -> t -> t
with \code{t} a free type variable.
\subsection{Colimits}\label{colimits}
\section{Colimits}\label{colimits}
Just like all constructions in category theory, limits have their dual
image in opposite categories. When you invert the direction of all
@ -601,7 +601,7 @@ The dual of the pullback is called the \newterm{pushout}. It's based on a
diagram called a span, generated by the category
\code{1\textless{}-2-\textgreater{}3}.
\subsection{Continuity}\label{continuity}
\section{Continuity}\label{continuity}
I said previously that functors come close to the idea of continuous
mappings of categories, in the sense that they never break existing
@ -680,7 +680,7 @@ calculus. In calculus limits and continuity are defined in terms of open
neighborhoods. Open sets, which define topology, form a category (a
poset).
\subsection{Challenges}\label{challenges}
\section{Challenges}\label{challenges}
\begin{enumerate}
\tightlist
@ -707,7 +707,7 @@ poset).
Next: \href{https://bartoszmilewski.com/2015/07/21/free-monoids/}{Free
Monoids}.
\subsection{Acknowledgments}\label{acknowledgments}
\section{Acknowledgments}\label{acknowledgments}
I'd like to thank Gershom Bazerman for checking my math and logic, and
André van Meulebrouck, who has been volunteering his editing help.\\

8
src/content/2.3/Free Monoids.tex
View File

@ -67,7 +67,7 @@ identifications --- just enough to uphold the laws --- is called a free
construction. What we have just done is to construct a \newterm{free
monoid} from the set of generators \code{\{a,\ b\}}.
\subsection{Free Monoid in Haskell}\label{free-monoid-in-haskell}
\section{Free Monoid in Haskell}\label{free-monoid-in-haskell}
A two-element set in Haskell is equivalent to the type \code{Bool},
and the free monoid generated by this set is equivalent to the type
@ -114,7 +114,7 @@ free monoid by identifying more than the minimum number of elements
required by the laws? I'll show you that this follows directly from the
universal construction.
\subsection{Free Monoid Universal
\section{Free Monoid Universal
Construction}\label{free-monoid-universal-construction}
If you recall our previous experiences with universal constructions, you
@ -262,7 +262,7 @@ have been made.
We'll come back to free monoids when we talk about adjunctions.
\subsection{Challenges}\label{challenges}
\section{Challenges}\label{challenges}
\begin{enumerate}
\item
@ -297,7 +297,7 @@ Next:
\href{https://bartoszmilewski.com/2015/07/29/representable-functors/}{Representable
Functors}.
\subsection{Acknowledgments}\label{acknowledgments}
\section{Acknowledgments}\label{acknowledgments}
I'd like to thank Gershom Bazerman for checking my math and logic, and
André van Meulebrouck, who has been volunteering his editing help

10
src/content/2.4/Representable Functors.tex
View File

@ -51,7 +51,7 @@ categories, but you can compare sets of apples against sets of oranges.
Often transforming a categorical problem into a set-theoretical problem
gives us the necessary insight or even lets us prove valuable theorems.
\subsection{The Hom Functor}\label{the-hom-functor}
\section{The Hom Functor}\label{the-hom-functor}
Every category comes equipped with a canonical family of mappings to
\textbf{Set}. Those mappings are in fact functors, so they preserve the
@ -169,7 +169,7 @@ fact succintly as:
C(-, =) :: Cop × C -> Set
\end{verbatim}
\subsection{Representable Functors}\label{representable-functors}
\section{Representable Functors}\label{representable-functors}
We've seen that, for every choice of an object \code{a} in \emph{C},
we get a functor from \emph{C} to \textbf{Set}. This kind of
@ -382,7 +382,7 @@ valuable in practice. So, surprisingly, even though it's not concerned
with performance at all, category theory provides ample opportunities to
explore alternative implementations that have practical value.
\subsection{Challenges}\label{challenges}
\section{Challenges}\label{challenges}
\begin{enumerate}
\item
@ -409,7 +409,7 @@ Pair a = Pair a a
\code{tabulate} and \code{index}.
\end{enumerate}
\subsection{Bibliography}\label{bibliography}
\section{Bibliography}\label{bibliography}
\begin{enumerate}
\tightlist
@ -423,7 +423,7 @@ Next:
\href{https://bartoszmilewski.com/2015/09/01/the-yoneda-lemma/}{The
Yoneda Lemma}.
\subsection{Acknowledgments}\label{acknowledgments}
\section{Acknowledgments}\label{acknowledgments}
I'd like to thank Gershom Bazerman for checking my math and logic, and
André van Meulebrouck, who has been volunteering his editing help

10
src/content/2.5/The Yoneda Lemma.tex
View File

@ -238,7 +238,7 @@ hom-functor through a lossy transformation. Such a transformation may
not only lose information, but it may also cover only a small part of
the image of the functor \code{F} in \textbf{Set}.
\subsection{Yoneda in Haskell}\label{yoneda-in-haskell}
\section{Yoneda in Haskell}\label{yoneda-in-haskell}
We have already encountered the hom-functor in Haskell under the guise
of the reader functor:
@ -338,7 +338,7 @@ of spaghetti code from interacting stateful handlers. As we'll see
later, judicious use of functors and monads can restore some
compositional properties of CPS.
\subsection{Co-Yoneda}\label{co-yoneda}
\section{Co-Yoneda}\label{co-yoneda}
As usual, we get a bonus construction by inverting the direction of
arrows. The Yoneda lemma can be applied to the opposite category
@ -366,7 +366,7 @@ forall x . (x -> a) -> F x ≅ F a
Notice that in some literature it's the contravariant version that's
called the Yoneda lemma.
\subsection{Challenges}\label{challenges}
\section{Challenges}\label{challenges}
\begin{enumerate}
\item
@ -393,13 +393,13 @@ psi :: F a -> (forall x . (a -> x) -> F x) psi fa h = fmap h fa
functor.
\end{enumerate}
\subsection{Bibliography}\label{bibliography}
\section{Bibliography}\label{bibliography}
Next:
\href{https://bartoszmilewski.com/2015/10/28/yoneda-embedding/}{Yoneda
Embedding}.
\subsection{Acknowledgments}\label{acknowledgments}
\section{Acknowledgments}\label{acknowledgments}
I'd like to thank Gershom Bazerman for checking my math and logic, and
André van Meulebrouck, who has been volunteering his editing help

12
src/content/2.6/Yoneda Embedding.tex
View File

@ -96,7 +96,7 @@ Notice that this doesn't mean that \code{F} is a bijection on
image of \code{F}, and we can't say anything about hom-sets for those
objects.
\subsection{The Embedding}\label{the-embedding}
\section{The Embedding}\label{the-embedding}
The (contravariant) functor we have just described, the functor that
maps objects in \emph{C} to functors in \code{{[}C,\ Set{]}}:
@ -134,7 +134,7 @@ is given by:
Again, mathematicians know a lot about the category of presheaves, so
being able to embed an arbitrary category in it is a big win.
\subsection{Application to Haskell}\label{application-to-haskell}
\section{Application to Haskell}\label{application-to-haskell}
In Haskell, the Yoneda embedding can be represented as the isomorphism
between natural transformations amongst reader functors on the one hand,
@ -186,7 +186,7 @@ provides a very useful
\href{https://bartoszmilewski.com/2015/07/13/from-lenses-to-yoneda-embedding/}{representation
of lenses} from the \code{Control.Lens} library.
\subsection{Preorder Example}\label{preorder-example}
\section{Preorder Example}\label{preorder-example}
This example was suggested by Robert Harper. It's the application of the
Yoneda embedding to a category defined by a preorder. A preorder is a
@ -267,7 +267,7 @@ must also be below \code{b}. Conversely, when you substitute
\code{a\ \textless{}=\ b}. But you must admit that arriving at this
result through the Yoneda embedding is much more exciting.
\subsection{Naturality}\label{naturality}
\section{Naturality}\label{naturality}
The Yoneda lemma establishes the isomorphism between the set of natural
transformations and an object in \textbf{Set}. Natural transformations
@ -325,7 +325,7 @@ mechanical. It follows from the fact that our isomorphism is built up
from functors and natural transformations. There is simply no way for it
to go wrong.
\subsection{Challenges}\label{challenges}
\section{Challenges}\label{challenges}
\begin{enumerate}
\tightlist
@ -353,7 +353,7 @@ Next:
\href{https://bartoszmilewski.com/2015/11/17/its-all-about-morphisms/}{It's
All About Morphisms}.
\subsection{Acknowledgments}\label{acknowledgments}
\section{Acknowledgments}\label{acknowledgments}
I'd like to thank Gershom Bazerman for checking my math and logic.\\
\href{https://twitter.com/BartoszMilewski}{Follow @BartoszMilewski}

18
src/content/3.1/It’s All About Morphisms.tex
View File

@ -14,7 +14,7 @@ hom-sets. Also, you'll see that adjunctions provide a more general
language to describe a lot of constructions we've studied before, so it
might help to review them too.
\subsection{Functors}\label{functors}
\section{Functors}\label{functors}
To begin with, you should really think of functors as mappings of
morphisms --- the view that's emphasized in the Haskell definition of
@ -27,7 +27,7 @@ be composed. So if we want the composition of morphisms to be mapped to
the composition of \newterm{lifted} morphisms, the mapping of their
endpoints is pretty much determined.
\subsection{Commuting Diagrams}\label{commuting-diagrams}
\section{Commuting Diagrams}\label{commuting-diagrams}
A lot of properties of morphisms are expressed in terms of commuting
diagrams. If a particular morphism can be described as a composition of
@ -52,7 +52,7 @@ the mapping of functors. This way commutativity is reduced to the role
of the assembly language for the higher level language of natural
transformations.
\subsection{Natural Transformations}\label{natural-transformations}
\section{Natural Transformations}\label{natural-transformations}
In general, natural transformations are very convenient whenever we need
a mapping from morphisms to commuting squares. Two opposing sides of a
@ -109,7 +109,7 @@ that defines the diagram in \emph{C}. Both functors \code{F} and
happens that this particular natural transformation between \code{F}
and \code{G} is an \newterm{isomorphism}.
\subsection{Natural Isomorphisms}\label{natural-isomorphisms}
\section{Natural Isomorphisms}\label{natural-isomorphisms}
A natural isomorphism --- which is a natural transformation whose every
component is reversible --- is category theory's way of saying that
@ -118,7 +118,7 @@ be an isomorphism between objects --- a morphism that has the inverse.
If you visualize functor images as sheets, a natural isomorphism is a
one-to-one invertible mapping between those sheets.
\subsection{Hom-Sets}\label{hom-sets}
\section{Hom-Sets}\label{hom-sets}
But what are morphisms? They do have more structure than objects: unlike
objects, morphisms have two ends. But if you fix the source and the
@ -154,7 +154,7 @@ h&apos; ∘ F f ≠ h&apos; ∘ F g
where \code{h\&apos;} is not in the image of \code{F}.
\subsection{Hom-Set Isomorphisms}\label{hom-set-isomorphisms}
\section{Hom-Set Isomorphisms}\label{hom-set-isomorphisms}
A lot of categorical constructions rely on isomorphisms between
hom-sets. But since hom-sets are just sets, a plain isomorphism between
@ -196,7 +196,7 @@ This is no coincidence --- we'll see next that these are just different
examples of adjunctions, which are defined as natural isomorphisms of
hom-sets.
\subsection{Asymmetry of Hom-Sets}\label{asymmetry-of-hom-sets}
\section{Asymmetry of Hom-Sets}\label{asymmetry-of-hom-sets}
There is one more observation that will help us understand adjunctions.
Hom-sets are, in general, not symmetric. A hom-set \code{C(a,\ b)} is
@ -219,7 +219,7 @@ generalization of a preoder.
A preorder is a thin category --- all hom-sets are either singletons or
empty. We can visualize a general category as a ``thick'' preorder.
\subsection{Challenges}\label{challenges}
\section{Challenges}\label{challenges}
\begin{enumerate}
\tightlist
@ -238,7 +238,7 @@ empty. We can visualize a general category as a ``thick'' preorder.
Next:
\href{https://bartoszmilewski.com/2016/04/18/adjunctions/}{Adjunctions}.
\subsection{Acknowledgments}\label{acknowledgments}
\section{Acknowledgments}\label{acknowledgments}
I'd like to thank Gershom Bazerman for checking my math and logic, and
André van Meulebrouck, who has been volunteering his editing help

14
src/content/3.10/Ends and Coends.tex
View File

@ -88,7 +88,7 @@ from \code{p\ a\ a} to \code{p\ a\ b}:
dimap id f paa :: p a b
\end{verbatim}
\subsection{Dinatural Transformations}\label{dinatural-transformations}
\section{Dinatural Transformations}\label{dinatural-transformations}
Since profunctors are functors, we can define natural transformations
between them in the standard way. In many cases, though, it's enough to
@ -123,7 +123,7 @@ Notice that a component of a natural transformation \code{α} in
indexed by one object, since it only maps diagonal elements of the
respective profunctors.
\subsection{Ends}\label{ends}
\section{Ends}\label{ends}
We are now ready to advance from ``algebra'' to what could be considered
the ``calculus'' of category theory. The calculus of ends (and coends)
@ -251,7 +251,7 @@ Ends can also be defined for target categories other than \textbf{Set},
but here we'll only consider \textbf{Set}-valued profunctors and their
ends.
\subsection{Ends as Equalizers}\label{ends-as-equalizers}
\section{Ends as Equalizers}\label{ends-as-equalizers}
The commutation condition in the definition of the end can be written
using an equalizer. First, let's define two functions (I'm using Haskell
@ -290,7 +290,7 @@ that the equalizer picks the largest subset on which two functions are
equal. In this case it picks the subset of the product of all diagonal
elements for which the wedge diagrams commute.
\subsection{Natural Transformations as
\section{Natural Transformations as
Ends}\label{natural-transformations-as-ends}
The most important example of an end is the set of natural
@ -344,7 +344,7 @@ idb ∘ τb ∘ F f
Their equality, demanded by the wedge condition, is nothing but the
naturality condition for \code{τ}.
\subsection{Coends}\label{coends}
\section{Coends}\label{coends}
As expected, the dual to an end is called a coend. It is constructed
from a dual to a wedge called a cowedge (pronounced co-wedge, not
@ -474,7 +474,7 @@ statement, with a tuple of handlers, one for every type present in the
sum. Here, the sum type is replaced by a coend, and a family of handlers
becomes an end, or a polymorphic function.
\subsection{Ninja Yoneda Lemma}\label{ninja-yoneda-lemma}
\section{Ninja Yoneda Lemma}\label{ninja-yoneda-lemma}
The set of natural transformations that appears in the Yoneda lemma may
be encoded using an end, resulting in the following formulation:
@ -548,7 +548,7 @@ isomorphism:
∫ z C(a, z) × F z ≅ F a
\end{verbatim}
\subsection{Profunctor Composition}\label{profunctor-composition}
\section{Profunctor Composition}\label{profunctor-composition}
Let's explore further the idea that a profunctor describes a relation
--- more precisely, a proof-relevant relation, meaning that the set

12
src/content/3.11/Kan Extensions.tex
View File

@ -84,7 +84,7 @@ But, importantly, we are free to replace the trivial category \textbf{1}
with an arbitrary category \emph{A}, and the definition of the right Kan
extension remains valid.
\subsection{Right Kan Extension}\label{right-kan-extension}
\section{Right Kan Extension}\label{right-kan-extension}
The right Kan extension of the functor \code{D::I-\textgreater{}C}
along the functor \code{K::I-\textgreater{}A} is a functor
@ -148,7 +148,7 @@ is not injective on objects or not faithful on hom-sets, as in the
example of the limit. In that case, the Kan extension tries its best to
extrapolate the lost information.
\subsection{Kan Extension as
\section{Kan Extension as
Adjunction}\label{kan-extension-as-adjunction}
Now suppose that the right Kan extension exists for any \code{D} (and
@ -226,7 +226,7 @@ The adjunction formula is an important result because, as we'll see
soon, we can calculate Kan extensions using ends (coends), thus giving
us practical means of finding right (and left) adjoints.
\subsection{Left Kan Extension}\label{left-kan-extension}
\section{Left Kan Extension}\label{left-kan-extension}
There is a dual construction that gives us the left Kan extension. To
build some intuition, we'll can start with the definition of a colimit
@ -308,7 +308,7 @@ Combining the two results, we get:
RanKIC ⊣ K ⊣ LanKIC
\end{verbatim}
\subsection{Kan Extensions as Ends}\label{kan-extensions-as-ends}
\section{Kan Extensions as Ends}\label{kan-extensions-as-ends}
The real power of Kan extensions comes from the fact that they can be
calculated using ends (and coends). For simplicity, we'll restrict our
@ -441,7 +441,7 @@ hand side of the adjunction we set out to prove:
These kinds of calculations using ends, coends, and the Yoneda lemma are
pretty typical for the ``calculus'' of ends.
\subsection{Kan Extensions in Haskell}\label{kan-extensions-in-haskell}
\section{Kan Extensions in Haskell}\label{kan-extensions-in-haskell}
The end/coend formulas for Kan extensions can be easily translated to
Haskell. Let's start with the right extension:
@ -551,7 +551,7 @@ repackaged the container using the natural transformation between the
identity functor and the pair functor, and (3) called the function
\code{f}.
\subsection{Free Functor}\label{free-functor}
\section{Free Functor}\label{free-functor}
An interesting application of Kan extensions is the construction of a
free functor. It's the solution to the following practical problem:

16
src/content/3.12/Enriched Categories.tex
View File

@ -42,7 +42,7 @@ enriched categories, and that's because a very useful online source of
categorical knowledge, the \href{https://ncatlab.org/}{nLab}, is written
mostly in terms of enriched categories.
\subsection{Why Monoidal Category?}\label{why-monoidal-category}
\section{Why Monoidal Category?}\label{why-monoidal-category}
When constructing an enriched category we have to keep in mind that we
should be able to recover the usual definitions when we replace the
@ -81,7 +81,7 @@ tensor product.
As you can see, objects taken from some monoidal category \emph{V} are
good candidates for hom-set replacement.
\subsection{Monoidal Category}\label{monoidal-category}
\section{Monoidal Category}\label{monoidal-category}
We've talked about monoidal categories before, but it's worth restating
the definition. A monoidal category defines a tensor product that is a
@ -166,7 +166,7 @@ example of a category that is not biclosed is the category of
endofunctors in \textbf{Set}, with functor composition serving as tensor
product. That's the category we used to define monads.
\subsection{Enriched Category}\label{enriched-category}
\section{Enriched Category}\label{enriched-category}
A category \emph{C} enriched over a monoidal category \emph{V} replaces
hom-sets with hom-objects. To every pair of objects \code{a} and
@ -207,7 +207,7 @@ Unit laws are likewise expressed in terms of unitors:
\includegraphics[width=4.65625in]{images/leftid.jpg}
\subsection{Preorders}\label{preorders}
\section{Preorders}\label{preorders}
A preorder is defined as a thin category, one in which every hom-set is
either empty or a singleton. We interpret a non-empty set
@ -245,7 +245,7 @@ There is only one morphism going from 1, and that's the identity
preorder. So both transitivity and reflexivity are automatically
enforced, if we implement a preorder as an enriched category.
\subsection{Metric Spaces}\label{metric-spaces}
\section{Metric Spaces}\label{metric-spaces}
An interesting example is due to
\href{http://www.tac.mta.ca/tac/reprints/articles/1/tr1.pdf}{William
@ -306,7 +306,7 @@ to \code{c}. But that's just the standard triangle inequality. Check!
By re-casting the metric space in terms of an enriched category, we get
the triangle inequality and the zero self-distance ``for free.''
\subsection{Enriched Functors}\label{enriched-functors}
\section{Enriched Functors}\label{enriched-functors}
The definition of a functor involves the mapping of morphisms. In the
enriched setting, we don't have the notion of individual morphisms, so
@ -336,7 +336,7 @@ morphisms in \emph{V} that ``select'' the identity:
\includegraphics[width=4.04167in]{images/functorid.jpg}
\subsection{Self Enrichment}\label{self-enrichment}
\section{Self Enrichment}\label{self-enrichment}
A closed symmetric monoidal category may be self-enriched by replacing
hom-sets with internal homs (see the definition above). To make this
@ -426,7 +426,7 @@ equivalent. Now we also know that, through self-enrichment, we can use
the exponential set as the hom-object and express composition in terms
of cartesian products of exponential objects.
\subsection{Relation to 2-Categories}\label{relation-to-2-categories}
\section{Relation to 2-Categories}\label{relation-to-2-categories}
I talked about 2-categories in the context of \textbf{Cat}, the category
of (small) categories. The morphisms between categories are functors,

8
src/content/3.13/Topoi.tex
View File

@ -37,7 +37,7 @@ category that has just the right properties to serve as a replacement
for set theory is called a \newterm{topos} (plural: topoi), and it
provides, among other things, a generalized notion of a subset.
\subsection{Subobject Classifier}\label{subobject-classifier}
\section{Subobject Classifier}\label{subobject-classifier}
Let's start by trying to express the idea of a subset using functions
rather than elements. Any function \code{f} from some set \code{a}
@ -202,7 +202,7 @@ This happens to be a natural isomorphism of two functors. In other
words, \code{Sub(-)} is a representable (contravariant) functor whose
representation is the object Ω.
\subsection{Topos}\label{topos}
\section{Topos}\label{topos}
A topos is a category that:
@ -227,7 +227,7 @@ It would be tempting to define the subobject classifier as a coproduct
\textbf{Set}--- but we want to be more general than that. Topoi in which
this is true are called Boolean.
\subsection{Topoi and Logic}\label{topoi-and-logic}
\section{Topoi and Logic}\label{topoi-and-logic}
In set theory, a characteristic function may be interpreted as defining
a property of the elements of a set --- a \newterm{predicate} that is true
@ -262,7 +262,7 @@ Next:
\href{https://bartoszmilewski.com/2017/08/26/lawvere-theories/}{Lawvere
Theories}.
\subsection{Challenges}\label{challenges}
\section{Challenges}\label{challenges}
\begin{enumerate}
\tightlist

20
src/content/3.14/Lawvere Theories.tex
View File

@ -10,7 +10,7 @@ monads. But there is an alternative universe in which, by chance,
Eugenio Moggi turned his attention to Lawvere theories rather than
monads. Let's explore that universe.
\subsection{Universal Algebra}\label{universal-algebra}
\section{Universal Algebra}\label{universal-algebra}
There are many ways of describing algebras at various levels of
abstraction. We try to find a general language to describe things like
@ -77,7 +77,7 @@ the roadmap:
\includegraphics[width=5.31250in]{images/lawvere1.png}
\subsection{Lavwere Theories}\label{lavwere-theories}
\section{Lavwere Theories}\label{lavwere-theories}
All Lawvere theories share a common backbone. All objects in a Lawvere
theory are generated from just one object using products (really, just
@ -214,7 +214,7 @@ At this point it would be very helpful to present a non-trivial example
of a Lawvere theory, but it would be hard to explain it without first
understanding what models are.
\subsection{Models of Lawvere
\section{Models of Lawvere
Theories}\label{models-of-lawvere-theories}
The key to understand Lawvere theories is to realize that one such
@ -305,7 +305,7 @@ function \code{M\ 1\ -\textgreater{}\ N\ 1} induces a natural
transformation between the two models \code{M} and \code{N}.
Therefore \code{Mod(Fop,\ Set)} is equivalent to \textbf{Set}.
\subsection{The Theory of Monoids}\label{the-theory-of-monoids}
\section{The Theory of Monoids}\label{the-theory-of-monoids}
The simplest nontrivial example of a Lawvere theory describes the
structure of monoids. It is a single theory that distills the structure
@ -358,7 +358,7 @@ The category of \newterm{models} of the Lawvere theory for monoids,
\code{Mod(LMon,\ Set)}, is equivalent to the category of all monoids,
\textbf{Mon}.
\subsection{Lawvere Theories and
\section{Lawvere Theories and
Monads}\label{lawvere-theories-and-monads}
As you may remember, algebraic theories can be described using monads
@ -494,7 +494,7 @@ finitary, with the notable exception of the continuation monad. It is
possible to to extend the notion of Lawvere theory beyond finitary
operations.
\subsection{Monads as Coends}\label{monads-as-coends}
\section{Monads as Coends}\label{monads-as-coends}
Let's explore the coend formula in more detail.
@ -635,7 +635,7 @@ T a = a × L(1, 1) = a
which is the identity monad.
\subsection{Lawvere Theory of Side
\section{Lawvere Theory of Side
Effects}\label{lawvere-theory-of-side-effects}
Since there is such a strong connection between monads and Lawvere
@ -703,7 +703,7 @@ Next:
\href{https://bartoszmilewski.com/2017/09/06/monads-monoids-and-categories/}{Monads,
Monoids, and Categories}.
\subsection{Challenges}\label{challenges}
\section{Challenges}\label{challenges}
\begin{enumerate}
\tightlist
@ -724,8 +724,8 @@ Monoids, and Categories}.
the left Kan extension of its own restriction.
\end{enumerate}
\subsection{Acknowledgments}\label{acknowledgments}
\section{Acknowledgments}\label{acknowledgments}
I'm grateful to Gershom Bazerman for many useful comments.
\subsection{Further Reading}\label{further-reading}
\section{Further Reading}\label{further-reading}

8
src/content/3.15/Monads, Monoids, and Categories.tex
View File

@ -18,7 +18,7 @@ As it turns out they are all interrelated, one leading to another in a
never-ending cycle of abstractions. I decided that showing these
interconnections might be a good way to end this book.
\subsection{Bicategories}\label{bicategories}
\section{Bicategories}\label{bicategories}
One of the most difficult aspects of category theory is the constant
switching of perspectives. Take the category of sets, for instance. We
@ -185,7 +185,7 @@ where 0-cells are categories, 1-cells are profunctors, and 2-cells are
natural transformations. The composition of profunctors was given by a
coend.
\subsection{Monads}\label{monads}
\section{Monads}\label{monads}
By now you should be pretty familiar with the definition of a monad as a
monoid in the category of endofunctors. Let's revisit this definition
@ -305,7 +305,7 @@ one-to-one correspondence). So it's really just a set and a few
functions. Considering the pivotal role that category theory plays in
all of mathematics, this is a very humbling realization.
\subsection{Challenges}\label{challenges}
\section{Challenges}\label{challenges}
\begin{enumerate}
\tightlist
@ -321,4 +321,4 @@ all of mathematics, this is a very humbling realization.
What's a monad algebra for a monad in \textbf{Span}?
\end{enumerate}
\subsection{Bibliography}\label{bibliography}
\section{Bibliography}\label{bibliography}

12
src/content/3.2/Adjunctions.tex
View File

@ -31,7 +31,7 @@ swap :: (a,b) -> (b,a) swap (a,b) = (b,a)
\code{swap} happens to be its own inverse.
\subsection{Adjunction and Unit/Counit
\section{Adjunction and Unit/Counit
Pair}\label{adjunction-and-unitcounit-pair}
When we talk about categories being isomorphic, we express this in terms
@ -241,7 +241,7 @@ and \code{u} is a function, here on type constructors). Conversely,
I'll explain in a moment why, in Haskell, we can impose the condition
that the right adjoint \code{u} be a \newterm{representable} functor.
\subsection{Adjunctions and Hom-Sets}\label{adjunctions-and-hom-sets}
\section{Adjunctions and Hom-Sets}\label{adjunctions-and-hom-sets}
There is an equivalent definition of the adjunction in terms of natural
isomorphisms of hom-sets. This definition ties nicely with universal
@ -429,7 +429,7 @@ C(L (), -) ≅ R
which shows that \code{R} is indeed representable.
\subsection{Product from Adjunction}\label{product-from-adjunction}
\section{Product from Adjunction}\label{product-from-adjunction}
We have previously introduced several concepts using universal
constructions. Many of those concepts, when defined globally, are easier
@ -607,7 +607,7 @@ for instance:
(,) Int Bool ~ (Int, Bool)
\end{verbatim}
\subsection{Exponential from
\section{Exponential from
Adjunction}\label{exponential-from-adjunction}
The exponential \code{ba}, or the function object \code{a⇒b}, can be
@ -670,7 +670,7 @@ unique object, up to isomorphism. That's why we have ``the'' product and
``the'' exponential. This property translates to adjunctions as well: if
a functor has an adjoint, this adjoint is unique up to isomorphism.
\subsection{Challenges}\label{challenges}
\section{Challenges}\label{challenges}
\begin{enumerate}
\item
@ -700,7 +700,7 @@ Next:
\href{https://bartoszmilewski.com/2016/06/15/freeforgetful-adjunctions/}{Free/Forgetful
Adjunctions}.
\subsection{Acknowledgments}\label{acknowledgments}
\section{Acknowledgments}\label{acknowledgments}
I'd like to thank Edward Kmett and Gershom Bazerman for checking my math
and logic, and André van Meulebrouck, who has been volunteering his

6
src/content/3.3/Free\Forgetful Adjunctions.tex
View File

@ -134,7 +134,7 @@ For simplicity I used the type \code{Int} rather than
\code{replicate} creates a list of length \code{n} pre-filled with a
given value --- here, the unit.
\subsection{Some Intuitions}\label{some-intuitions}
\section{Some Intuitions}\label{some-intuitions}
What follows are some hand-waving arguments. Those kind of arguments are
far from rigorous, but they help in forming intuitions.
@ -238,7 +238,7 @@ instance, done in implementing matrix calculus, where eager evaluation
would lead to lots of allocations of temporary arrays to store
intermediate results.
\subsection{Challenges}\label{challenges}
\section{Challenges}\label{challenges}
\begin{enumerate}
\tightlist
@ -253,7 +253,7 @@ Next:
\href{https://bartoszmilewski.com/2016/11/21/monads-programmers-definition/}{Monads:
Programmer's Definition}.
\subsection{Acknowledgments}\label{acknowledgments}
\section{Acknowledgments}\label{acknowledgments}
I'd like to thank Gershom Bazerman for checking my math and logic, and
André van Meulebrouck, who has been volunteering his editing help

6
src/content/3.4/Monads - Programmer’s Definition.tex
View File

@ -82,7 +82,7 @@ called the \code{do} notation for monadic composition. We'll see its
use later. But first, let me explain why we need monadic composition in
the first place.
\subsection{The Kleisli Category}\label{the-kleisli-category}
\section{The Kleisli Category}\label{the-kleisli-category}
We have previously arrived at the
\href{https://bartoszmilewski.com/2014/12/23/kleisli-categories/}{writer
@ -180,7 +180,7 @@ tell :: w -> Writer w () tell s = Writer ((), s)
We'll use it later as a building block for other monadic functions.
\subsection{Fish Anatomy}\label{fish-anatomy}
\section{Fish Anatomy}\label{fish-anatomy}
When implementing the fish operator for different monads you quickly
realize that a lot of code is repeated and can be easily factored out.
@ -265,7 +265,7 @@ For completeness, here's \code{join} for the \code{Writer} monad:
join :: Monoid w => Writer w (Writer w a) -> Writer w a join (Writer ((Writer (a, w&apos;)), w)) = Writer (a, w `mappend` w&apos;)
\end{verbatim}
\subsection{\texorpdfstring{The \code{do}
\section{\texorpdfstring{The \code{do}
Notation}{The do Notation}}\label{the-do-notation}
One way of writing code using monads is to work with Kleisli arrows ---

6
src/content/3.5/Monads and Effects.tex
View File

@ -15,7 +15,7 @@ problem that would otherwise be solved using impure functions (e.g., by
accessing and modifying some global state) was solved with pure
functions.
\subsection{The Problem}\label{the-problem}
\section{The Problem}\label{the-problem}
Here is a short list of similar problems, copied from
\href{https://core.ac.uk/download/pdf/21173011.pdf}{Eugenio Moggi's
@ -67,7 +67,7 @@ The next section is heavy on Haskell examples. Feel free to skim or even
skip it if you're eager to get back to category theory or if you're
already familiar with Haskell's implementation of monads.
\subsection{The Solution}\label{the-solution}
\section{The Solution}\label{the-solution}
First, let's analyze the way we used the \code{Writer} monad. We
started with a pure function that performed a certain task --- given
@ -596,7 +596,7 @@ the action that prints ``World!'' receives, as input, the Universe in
which ``Hello '' is already on the screen. It outputs a new Universe,
with ``Hello World!'' on the screen.
\subsection{Conclusion}\label{conclusion}
\section{Conclusion}\label{conclusion}
Of course I have just scratched the surface of monadic programming.
Monads not only accomplish, with pure functions, what normally is done

8
src/content/3.6/Monads Categorically.tex
View File

@ -196,7 +196,7 @@ multiplication μ, unit η, associativity, and unit laws. But our
definition of a monoid is too narrow to describe a monad as a monoid. So
let's generalize the notion of a monoid.
\subsection{Monoidal Categories}\label{monoidal-categories}
\section{Monoidal Categories}\label{monoidal-categories}
Let's go back to the conventional definition of a monoid. It's a set
with a binary operation and a special element called unit. In Haskell,
@ -405,7 +405,7 @@ we'll see shortly, for the composition of endofunctors (and also for
some more esoteric products like Day convolution). Monoidal categories
will play an essential role in the formulation of enriched categories.
\subsection{Monoid in a Monoidal
\section{Monoid in a Monoidal
Category}\label{monoid-in-a-monoidal-category}
We are now ready to define a monoid in a more general setting of a
@ -437,7 +437,7 @@ because we need to lift pairs of morphisms to form products such as
straightforward generalization of our previous results for categorical
products.
\subsection{Monads as Monoids}\label{monads-as-monoids}
\section{Monads as Monoids}\label{monads-as-monoids}
Monoidal structures pop up in unexpected places. One such place is the
functor category. If you squint a little, you might be able to see
@ -504,7 +504,7 @@ All told, monad is just a monoid in the category of endofunctors.
You might have seen it emblazoned on some t-shirts at functional
programming conferences.
\subsection{Monads from Adjunctions}\label{monads-from-adjunctions}
\section{Monads from Adjunctions}\label{monads-from-adjunctions}
An
\href{https://bartoszmilewski.com/2016/04/18/adjunctions/}{adjunction},

16
src/content/3.7/Comonads.tex
View File

@ -50,7 +50,7 @@ In practice, we use slightly different primitives, as we'll see shortly.
The question is, what's the use for comonads in programming?
\subsection{Programming with Comonads}\label{programming-with-comonads}
\section{Programming with Comonads}\label{programming-with-comonads}
Let's compare the monad with the comonad. A monad provides a way of
putting a value in a container using \code{return}. It doesn't give
@ -70,7 +70,7 @@ result --- it embellishes it with context --- a co-Kleisli arrow takes a
value together with a whole context and produces a result. It's an
embodiment of \newterm{contextual computation}.
\subsection{The Product Comonad}\label{the-product-comonad}
\section{The Product Comonad}\label{the-product-comonad}
Remember the reader monad? We introduced it to tackle the problem of
implementing computations that need access to some read-only environment
@ -123,7 +123,7 @@ later.
It's easy to generalize the \code{Product} comonad to arbitrary
product types including tuples and records.
\subsection{Dissecting the
\section{Dissecting the
Composition}\label{dissecting-the-composition}
Continuing the process of dualization, we could go ahead and dualize
@ -214,7 +214,7 @@ new state of the current cell. To do that, it would look at its context
\code{duplicate} to produce all possible foci and then we apply
\code{f} to each of them.
\subsection{The Stream Comonad}\label{the-stream-comonad}
\section{The Stream Comonad}\label{the-stream-comonad}
This process of shifting the focus from one element of the container to
another is best illustrated with the example of an infinite stream. Such
@ -298,7 +298,7 @@ The result is the stream of running averages.
A stream is an example of a unidirectional, one-dimensional comonad. It
can be easily made bidirectional or extended to two or more dimensions.
\subsection{Comonad Categorically}\label{comonad-categorically}
\section{Comonad Categorically}\label{comonad-categorically}
Defining a comonad in category theory is a straightforward exercise in
duality. As with the monad, we start with an endofunctor \code{T}. The
@ -405,7 +405,7 @@ of endofunctors,
The comonad is a comonoid in the category of endofunctors.
\subsection{The Store Comonad}\label{the-store-comonad}
\section{The Store Comonad}\label{the-store-comonad}
Another important example of a comonad is the dual of the state monad.
It's called the costate comonad or, alternatively, the store comonad.
@ -533,7 +533,7 @@ returning the modified version of \code{a}. Similarly, \code{get}
could be implemented to read the value of the \code{s} field from
\code{a}. We'll explore these ideas more in the next section.
\subsection{Challenges}\label{challenges}
\section{Challenges}\label{challenges}
\begin{enumerate}
\tightlist
@ -542,7 +542,7 @@ could be implemented to read the value of the \code{s} field from
Hint: What type do you pick for \code{s}?
\end{enumerate}
\subsection{Acknowledgments}\label{acknowledgments}
\section{Acknowledgments}\label{acknowledgments}
I'm grateful to Edward Kmett for reading the draft of this post and
pointing out flaws in my reasoning.

12
src/content/3.8/F-Algebras.tex
View File

@ -154,7 +154,7 @@ can be evaluated using the evaluator of the algebra. So far we've only
seen very simple expressions. We are often interested in more elaborate
expressions that can be defined using recursion.
\subsection{Recursion}\label{recursion}
\section{Recursion}\label{recursion}
One way to generate arbitrary expression trees is to replace the
variable \code{a} inside the functor definition with recursion. For
@ -254,7 +254,7 @@ unFix :: Fix f -> f (Fix f) unFix (Fix x) = x
The two functions are the inverse of each other. We'll use these
functions later.
\subsection{Category of F-Algebras}\label{category-of-f-algebras}
\section{Category of F-Algebras}\label{category-of-f-algebras}
Here's the oldest trick in the book: Whenever you come up with a way of
constructing some new objects, see if they form a category. Not
@ -388,7 +388,7 @@ data Nat = Zero | Succ Nat
A natural number is either zero or a successor of another number. This
is known as the Peano representation for natural numbers.
\subsection{Catamorphisms}\label{catamorphisms}
\section{Catamorphisms}\label{catamorphisms}
Let's rewrite the initiality condition using Haskell notation. We call
the initial algebra \code{Fix\ f}. Its evaluator is the contructor
@ -459,7 +459,7 @@ In general, an algebra for \code{NatF} defines a recurrence relation:
the value of the current element in terms of the previous element. A
catamorphism then evaluates the n-th element of that sequence.
\subsection{Folds}\label{folds}
\section{Folds}\label{folds}
A list of \code{e} is the initial algebra of the following functor:
@ -517,7 +517,7 @@ sum = foldr (\e s -> e + s) 0.0
As you can see, \code{foldr} is just a convenient specialization of a
catamorphism to lists.
\subsection{Coalgebras}\label{coalgebras}
\section{Coalgebras}\label{coalgebras}
As usual, we have a dual construction of an F-coagebra, where the
direction of the morphism is reversed:
@ -655,7 +655,7 @@ 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
with the comonad structure. We'll talk about this in the next section.
\subsection{Challenges}\label{challenges}
\section{Challenges}\label{challenges}
\begin{enumerate}
\tightlist

12
src/content/3.9/Algebras for Monads.tex
View File

@ -109,7 +109,7 @@ lists, and then fold the resulting list. Again, if we interpret
binary operation is associative. These conditions are certainly
fulfilled when \code{(a,\ f,\ z)} is a monoid.
\subsection{T-algebras}\label{t-algebras}
\section{T-algebras}\label{t-algebras}
Since mathematicians prefer to call their monads \code{T}, they call
algebras compatible with them T-algebras. T-algebras for a given monad T
@ -255,7 +255,7 @@ doesn't change anything, since the action of \code{UT} on morphisms is
trivial. So, indeed, the \code{μ} obtained from the adjunction is the
same as the \code{μ} of the original monad \code{T}.
\subsection{The Kleisli Category}\label{the-kleisli-category}
\section{The Kleisli Category}\label{the-kleisli-category}
We've seen the Kleisli category before. It's a category constructed from
another category \emph{C} and a monad \code{T}. We'll call this
@ -366,7 +366,7 @@ in the same monad \code{T} on \emph{C}. The Kleisli adjunction we've
just seen is the initial object in this category, and the
Eilenberg-Moore adjunction is the terminal object.
\subsection{Coalgebras for Comonads}\label{coalgebras-for-comonads}
\section{Coalgebras for Comonads}\label{coalgebras-for-comonads}
Analogous constructions can be done for any
\href{https://bartoszmilewski.com/2017/01/02/comonads/}{comonad}
@ -403,7 +403,7 @@ adjunction reproduces the original comonad as the composite
Similarly, we can construct a co-Kleisli category with co-Kleisli arrows
and regenerate the comonad from the corresponding adjunction.
\subsection{Lenses}\label{lenses}
\section{Lenses}\label{lenses}
Let's go back to our discussion of lenses. A lens can be written as a
coalgebra:
@ -514,7 +514,7 @@ gives \code{s} back.
In other words, a well-behaved lens is indeed a comonad coalgebra for
the \code{Store} functor.
\subsection{Challenges}\label{challenges}
\section{Challenges}\label{challenges}
\begin{enumerate}
\item
@ -531,7 +531,7 @@ UW ⊣ FW
Prove that the above adjunction reproduces the original comonad.
\end{enumerate}
\subsection{Acknowledgment}\label{acknowledgment}
\section{Acknowledgment}\label{acknowledgment}
I'd like to thank Gershom Bazerman for helpful comments.