From ee59574ad3eb3c96d05789f2fc54940076916bee Mon Sep 17 00:00:00 2001 From: Igal Tabachnik Date: Mon, 16 Oct 2017 21:26:02 +0300 Subject: [PATCH] Small fixes + version bump! This fixes several issues: fixes #42 fixes #45 fixes #53 fixes #60 fixes #69 fixes #70 fixes #36 --- src/content/0.0/Preface.tex | 8 +- .../Category - The Essence of Composition.tex | 29 ++-- src/content/1.10/Natural Transformations.tex | 18 +-- src/content/1.2/Types and Functions.tex | 24 ++- .../1.3/Categories Great and Small.tex | 24 +-- src/content/1.4/Kleisli Categories.tex | 8 +- src/content/1.5/Products and Coproducts.tex | 137 +++++++++--------- .../1.6/Simple Algebraic Data Types.tex | 12 +- src/content/1.7/Functors.tex | 24 +-- src/content/1.8/Functoriality.tex | 25 ++-- src/content/1.9/Function Types.tex | 58 ++++---- src/content/2.1/Declarative Programming.tex | 2 +- src/content/2.2/Limits and Colimits.tex | 10 +- src/content/2.3/Free Monoids.tex | 6 +- src/content/2.4/Representable Functors.tex | 8 +- src/content/2.5/The Yoneda Lemma.tex | 4 +- src/content/2.6/Yoneda Embedding.tex | 4 +- src/content/3.1/It's All About Morphisms.tex | 8 +- src/content/3.13/Topoi.tex | 2 +- src/content/3.14/Lawvere Theories.tex | 4 +- .../3.15/Monads, Monoids, and Categories.tex | 2 +- src/content/3.2/Adjunctions.tex | 2 +- .../3.3/Free-Forgetful Adjunctions.tex | 4 +- src/content/3.5/Monads and Effects.tex | 4 +- src/content/3.7/Comonads.tex | 2 +- src/ctfp.tex | 9 +- 26 files changed, 214 insertions(+), 224 deletions(-) diff --git a/src/content/0.0/Preface.tex b/src/content/0.0/Preface.tex index 8953c05f..4f5bb392 100644 --- a/src/content/0.0/Preface.tex +++ b/src/content/0.0/Preface.tex @@ -100,7 +100,7 @@ \begin{figure} \centering -\fbox{\includegraphics[width=3.12500in]{images/img_1299.jpg}} +\includegraphics[width=70mm]{images/img_1299.jpg} \end{figure} One of the forces that are driving the big change is the multicore @@ -131,7 +131,7 @@ us to rethink the foundations of programming. Just like the builders of Europe's great gothic cathedrals we've been honing our craft to the limits of material and structure. There is an unfinished gothic -\href{http://en.wikipedia.org/wiki/Beauvais_Cathedral}{cathedral in +\urlref{http://en.wikipedia.org/wiki/Beauvais_Cathedral}{cathedral in Beauvais}, France, that stands witness to this deeply human struggle with limitations. It was intended to beat all previous records of height and lightness, but it suffered a series of collapses. Ad hoc measures @@ -148,6 +148,6 @@ \begin{figure} \centering -\fbox{\includegraphics[totalheight=8cm]{images/beauvais_interior_supports.jpg}} +\includegraphics[totalheight=8cm]{images/beauvais_interior_supports.jpg} \caption{Ad hoc measures preventing the Beauvais cathedral from collapsing.} -\end{figure} +\end{figure} \ No newline at end of file diff --git a/src/content/1.1/Category - The Essence of Composition.tex b/src/content/1.1/Category - The Essence of Composition.tex index c683cd08..77f79c0d 100644 --- a/src/content/1.1/Category - The Essence of Composition.tex +++ b/src/content/1.1/Category - The Essence of Composition.tex @@ -3,7 +3,7 @@ why categories are so easy to represent pictorially. An object can be drawn as a circle or a point, and an arrow\ldots{} is an arrow. (Just for variety, I will occasionally draw objects as piggies and arrows as -fireworks.) But the essence of a category is \newterm{composition}. Or, if you +fireworks.) But the essence of a category is \emph{composition}. Or, if you prefer, the essence of composition is a category. Arrows compose, so if you have an arrow from object $A$ to object $B$, and another arrow from object $B$ to object $C$, then there must be an arrow --- their composition @@ -17,17 +17,17 @@ category because it’s missing identity morphisms (see later).} \end{figure} -\section{Arrows as Functions}\label{arrows-as-functions} +\section{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 -functions. You have a function \code{f} that takes an argument of type $A$ and -returns a $B$. You have another function \code{g} that takes a $B$ and returns a $C$. +functions. You have a function $f$ that takes an argument of type $A$ and +returns a $B$. You have another function $g$ that takes a $B$ and returns a $C$. You can compose them by passing the result of $f$ to $g$. You have just defined a new function that takes an $A$ and returns a $C$. In math, such composition is denoted by a small circle between -functions: \ensuremath{g \circ f}. Notice the right to left order of composition. For some +functions: $g \circ f$. Notice the right to left order of composition. For some people this is confusing. You may be familiar with the pipe notation in Unix, as in: @@ -36,7 +36,7 @@ \section{Arrows as Functions}\label{arrows-as-functions} \end{Verbatim} or the chevron \code{>>} in F\#, which both go from left to right. But in mathematics and in Haskell functions -compose right to left. It helps if you read \(g \circ f\) as ``g \emph{after} f.'' +compose right to left. It helps if you read $g \circ f$ as ``g \emph{after} f.'' Let's make this even more explicit by writing some C code. We have one function \code{f} that takes an argument of type \code{A} and @@ -83,12 +83,12 @@ \section{Arrows as Functions}\label{arrows-as-functions} straightforward functional concepts in C++ is a little embarrassing. In fact, Haskell will let you use Unicode characters so you can write composition as: - +% don't 'mathify' this block \begin{Verbatim} g ◦ f \end{Verbatim} You can even use Unicode double colons and arrows: - +% don't 'mathify' this block \begin{Verbatim}[commandchars=\\\{\}] f \ensuremath{\Colon} A → B \end{Verbatim} @@ -97,7 +97,7 @@ \section{Arrows as Functions}\label{arrows-as-functions} two types. You compose two functions by inserting a period between them (or a Unicode circle). -\section{Properties of Composition}\label{properties-of-composition} +\section{Properties of Composition} There are two extremely important properties that the composition in any category must satisfy. @@ -108,7 +108,7 @@ \section{Properties of Composition}\label{properties-of-composition} that can be composed (that is, their objects match end-to-end), you don't need parentheses to compose them. In math notation this is expressed as: -\[h\circ{}(g\circ{}f) = (h\circ{}g)\circ{}f = h\circ{}g\circ{}f\] +\[h \circ (g \circ f) = (h \circ g) \circ f = h \circ g \circ f\] In (pseudo) Haskell: \begin{Verbatim} @@ -186,7 +186,7 @@ \section{Properties of Composition}\label{properties-of-composition} Romans had a number system without a zero and they were able to build excellent roads and aqueducts, some of which survive to this day. -Neutral values like zero or \code{id} are extremely useful when +Neutral values like zero or $\id$ are extremely useful when working with symbolic variables. That's why Romans were not very good at algebra, whereas the Arabs and the Persians, who were familiar with the concept of zero, were. So the identity function becomes very handy as an @@ -198,8 +198,7 @@ \section{Properties of Composition}\label{properties-of-composition} Arrows can be composed, and the composition is associative. Every object has an identity arrow that serves as a unit under composition. -\section{Composition is the Essence of -Programming}\label{composition-is-the-essence-of-programming} +\section{Composition is the Essence of Programming} Functional programmers have a peculiar way of approaching problems. They start by asking very Zen-like questions. For instance, when designing an @@ -223,7 +222,7 @@ \section{Composition is the Essence of imposed on us by computers. It reflects the limitations of the human mind. Our brains can only deal with a small number of concepts at a time. One of the most cited papers in psychology, -\href{http://en.wikipedia.org/wiki/The_Magical_Number_Seven,_Plus_or_Minus_Two}{The +\urlref{http://en.wikipedia.org/wiki/The_Magical_Number_Seven,_Plus_or_Minus_Two}{The Magical Number Seven, Plus or Minus Two}, postulated that we can only keep $7 \pm 2$ ``chunks'' of information in our minds. The details of our understanding of the human short-term memory might be changing, but we @@ -263,7 +262,7 @@ \section{Composition is the Essence of understand how to compose it with other objects, you've lost the advantages of your programming paradigm. -\section{Challenges}\label{challenges} +\section{Challenges} \begin{enumerate} \tightlist diff --git a/src/content/1.10/Natural Transformations.tex b/src/content/1.10/Natural Transformations.tex index 9bb34ccb..ec0570d6 100644 --- a/src/content/1.10/Natural Transformations.tex +++ b/src/content/1.10/Natural Transformations.tex @@ -3,7 +3,7 @@ \begin{wrapfigure}[13]{R}{0pt} \raisebox{0pt}[\dimexpr\height-0.75\baselineskip\relax]{ -\fbox{\includegraphics[width=60mm]{images/1_functors.jpg}}}% +\includegraphics[width=60mm]{images/1_functors.jpg}}% \end{wrapfigure} \noindent @@ -29,7 +29,7 @@ \begin{figure}[H] \centering -\fbox{\includegraphics[width=80mm]{images/2_natcomp.jpg}} +\includegraphics[width=80mm]{images/2_natcomp.jpg} \end{figure} \noindent @@ -131,7 +131,7 @@ a natural transformation whose components are all isomorphisms (invertible morphisms). -\section{Polymorphic Functions}\label{polymorphic-functions} +\section{Polymorphic Functions} We talked about the role of functors (or, more specifically, endofunctors) in programming. They correspond to type constructors that @@ -355,7 +355,7 @@ \section{Polymorphic Functions}\label{polymorphic-functions} \end{Verbatim} There are only two of these, \code{dumb} and \code{obvious}: -\begin{Verbatim}[commandchars=\\\{\}] +\begin{Verbatim} dumb (Reader _) = Nothing \end{Verbatim} and @@ -371,7 +371,7 @@ \section{Polymorphic Functions}\label{polymorphic-functions} and \code{Just ()}. We'll come back to the Yoneda lemma later --- this was just a little teaser. -\section{Beyond Naturality}\label{beyond-naturality} +\section{Beyond Naturality} A parametrically polymorphic function between two functors (including the edge case of the \code{Const} functor) is always a natural @@ -441,7 +441,7 @@ \section{Beyond Naturality}\label{beyond-naturality} transformations, called dinatural transformations, that deals with such cases. We'll get to them when we discuss ends. -\section{Functor Category}\label{functor-category} +\section{Functor Category} Now that we have mappings between functors --- natural transformations --- it's only natural to ask the question whether functors form a @@ -550,7 +550,7 @@ \section{Functor Category}\label{functor-category} $\cat{D^C}$ is a category, which we can identify with the functor category between $\cat{C}$ and $\cat{D}$. -\section{2-Categories}\label{categories} +\section{2-Categories} With that out of the way, let's have a closer look at $\Cat$. By definition, any Hom-set in $\Cat$ is a set of functors. But, as we @@ -748,7 +748,7 @@ \section{Conclusion} they become sources and targets of morphisms: natural transformations. A natural transformation is a special type of polymorphic function. -\section{Challenges}\label{challenges} +\section{Challenges} \begin{enumerate} \tightlist @@ -780,7 +780,7 @@ \section{Challenges}\label{challenges} \end{Verbatim} and -\begin{Verbatim}[commandchars=\\\{\}] +\begin{Verbatim} f :: String -> Int f x = read x \end{Verbatim} diff --git a/src/content/1.2/Types and Functions.tex b/src/content/1.2/Types and Functions.tex index 1854cca8..94a0c998 100644 --- a/src/content/1.2/Types and Functions.tex +++ b/src/content/1.2/Types and Functions.tex @@ -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. -\section{Who Needs Types?}\label{who-needs-types} +\section{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,8 +35,7 @@ \section{Who Needs Types?}\label{who-needs-types} once Romeo is declared a human being, he doesn't sprout leaves or trap photons in his powerful gravitational field. -\section{Types Are About -Composability}\label{types-are-about-composability} +\section{Types Are About Composability} Category theory is about composing arrows. But not any two arrows can be composed. The target object of one arrow must be the same as the source @@ -95,7 +94,7 @@ \section{Types Are About almost always a probabilistic rather than a deterministic process. Testing is a poor substitute for proof. -\section{What Are Types?}\label{what-are-types} +\section{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 @@ -147,7 +146,7 @@ \section{What Are Types?}\label{what-are-types} scientists came up with a brilliant idea, or a major hack, depending on your point of view, to extend every type by one more special value called the \newterm{bottom} and denoted by \code{\_|\_}, or -Unicode \ensuremath{\bot}. This ``value'' corresponds to a non-terminating computation. +Unicode $\bot$. This ``value'' corresponds to a non-terminating computation. So a function declared as: \begin{Verbatim} @@ -180,7 +179,7 @@ \section{What Are Types?}\label{what-are-types} functions, which return valid results for every possible argument. Because of the bottom, you'll see the category of Haskell types and -functions referred to as \textbf{Hask} rather than $\Set$. From +functions referred to as $\cat{Hask}$ rather than $\Set$. From the theoretical point of view, this is the source of never-ending complications, so at this point I will use my butcher's knife and terminate this line of reasoning. From the pragmatic point of view, it's @@ -189,8 +188,7 @@ \section{What Are Types?}\label{what-are-types} 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.} -\section{Why Do We Need a Mathematical -Model?}\label{why-do-we-need-a-mathematical-model} +\section{Why Do We Need a Mathematical Model?} As a programmer you are intimately familiar with the syntax and grammar of your programming language. These aspects of the language are usually @@ -283,7 +281,7 @@ \section{Why Do We Need a Mathematical appreciate the thought that functions and algorithms from the Haskell standard library come with proofs of correctness. -\section{Pure and Dirty Functions}\label{pure-and-dirty-functions} +\section{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 +309,7 @@ \section{Pure and Dirty Functions}\label{pure-and-dirty-functions} all kinds of effects using only pure functions. So we really don't lose anything by restricting ourselves to mathematical functions. -\section{Examples of Types}\label{examples-of-types} +\section{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 @@ -384,8 +382,8 @@ \section{Examples of Types}\label{examples-of-types} mathematical sense of the word. A pure function that returns unit does nothing: it discards its argument. -Mathematically, a function from a set A to a singleton set maps every -element of A to the single element of that singleton set. For every A +Mathematically, a function from a set $A$ to a singleton set maps every +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}: @@ -458,7 +456,7 @@ \section{Examples of Types}\label{examples-of-types} have the form \code{ctype::is(alpha, c)}, \code{ctype::is(digit, c)}, etc. -\section{Challenges}\label{challenges} +\section{Challenges} \begin{enumerate} \tightlist diff --git a/src/content/1.3/Categories Great and Small.tex b/src/content/1.3/Categories Great and Small.tex index 6f214239..1fc426e4 100644 --- a/src/content/1.3/Categories Great and Small.tex +++ b/src/content/1.3/Categories Great and Small.tex @@ -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. -\section{No Objects}\label{no-objects} +\section{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 @@ \section{No Objects}\label{no-objects} category of all categories (yes, there is one). If you think that an empty set makes sense, then why not an empty category? -\section{Simple Graphs}\label{simple-graphs} +\section{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,18 +34,18 @@ \section{Simple Graphs}\label{simple-graphs} satisfy its laws (here, the laws of a category). We'll see more examples of it in the future. -\section{Orders}\label{orders} +\section{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. Let's check if it indeed is a category. Do we have identity morphisms? Every object is less than or equal to itself: check! Do we have -composition? If $a \leq b$ and $b \leq c$ then $a \leq c$: check! Is composition associative? Check! A set with a +composition? If $a \leqslant b$ and $b \leqslant c$ then $a \leqslant c$: check! Is composition associative? Check! A set with a relation like this is called a \newterm{preorder}, so a preorder is indeed a category. You can also have a stronger relation, that satisfies an additional -condition that, if $a \leq b$ and $b \leq a$ then $a$ must be +condition that, if $a \leqslant b$ and $b \leqslant a$ then $a$ must be the same as $b$. That's called a \newterm{partial order}. Finally, you can impose the condition that any two objects are in a @@ -59,7 +59,7 @@ \section{Orders}\label{orders} A set of morphisms from object a to object b in a category $\cat{C}$ is called a \newterm{hom-set} and is written as $\cat{C}(a, b)$ (or, sometimes, -$\cat{Hom_C}(a, b)$). So every hom-set in a preorder is either +$\mathbf{Hom}_{\cat{C}}(a, b)$). So every hom-set in a preorder is either empty or a singleton. That includes the hom-set $\cat{C}(a, a)$, the set of morphisms from a to a, which must be a singleton, containing only the identity, in any preorder. You may, however, have cycles in a preorder. @@ -70,7 +70,7 @@ \section{Orders}\label{orders} quicksort, bubble sort, merge sort, etc., can only work correctly on total orders. Partial orders can be sorted using topological sort. -\section{Monoid as Set}\label{monoid-as-set} +\section{Monoid as Set} Monoid is an embarrassingly simple but amazingly powerful concept. It's the concept behind basic arithmetics: Both addition and multiplication @@ -109,14 +109,14 @@ \section{Monoid as Set}\label{monoid-as-set} mappend :: m -> m -> m \end{Verbatim} The type signature for a two-argument function, -\code{m->m->m}, might look strange at first, +\code{m -> m -> m}, might look strange at first, but it will make perfect sense after we talk about currying. You may interpret a signature with multiple arrows in two basic ways: as a function of multiple arguments, with the rightmost type being the return type; or as a function of one argument (the leftmost one), returning a function. The latter interpretation may be emphasized by adding parentheses (which are redundant, because the arrow is -right-associative), as in: \code{m->(m->m)}. +right-associative), as in: \code{m -> (m -> m)}. We'll come back to this interpretation in a moment. Notice that, in Haskell, there is no way to express the monoidal @@ -222,7 +222,7 @@ \section{Monoid as Set}\label{monoid-as-set} } \end{Verbatim} -\section{Monoid as Category}\label{monoid-as-category} +\section{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 @@ -253,7 +253,7 @@ \section{Monoid as Category}\label{monoid-as-category} An astute reader might have noticed that the mapping from integers to adders follows from the second interpretation of the type signature of -\code{mappend} as \code{m->(m->m)}. It +\code{mappend} as \code{m -> (m -> m)}. It tells us that \code{mappend} maps an element of a monoid set to a function acting on that set. @@ -310,7 +310,7 @@ \section{Monoid as Category}\label{monoid-as-category} composition of morphisms in M translates into monoidal product in the set $\cat{M}(m, m)$. -\section{Challenges}\label{challenges} +\section{Challenges} \begin{enumerate} \tightlist diff --git a/src/content/1.4/Kleisli Categories.tex b/src/content/1.4/Kleisli Categories.tex index 258599ca..3ab341c5 100644 --- a/src/content/1.4/Kleisli Categories.tex +++ b/src/content/1.4/Kleisli Categories.tex @@ -159,7 +159,7 @@ so before we write more code, let's analyze the problem from the categorical point of view. -\section{The Writer Category}\label{the-writer-category} +\section{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 @@ -300,7 +300,7 @@ \section{The Writer Category}\label{the-writer-category} make the library work --- here the logging library's only requirement is that the log have monoidal properties. -\section{Writer in Haskell}\label{writer-in-haskell} +\section{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} @@ -395,7 +395,7 @@ \section{Writer in Haskell}\label{writer-in-haskell} process = upCase >=> toWords \end{Verbatim} -\section{Kleisli Categories}\label{kleisli-categories} +\section{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 @@ -424,7 +424,7 @@ \section{Kleisli Categories}\label{kleisli-categories} programs that in imperative languages are traditionally implemented using side effects. -\section{Challenge}\label{challenge} +\section{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 diff --git a/src/content/1.5/Products and Coproducts.tex b/src/content/1.5/Products and Coproducts.tex index c5d91318..7fe03be8 100644 --- a/src/content/1.5/Products and Coproducts.tex +++ b/src/content/1.5/Products and Coproducts.tex @@ -21,7 +21,7 @@ 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. -\section{Initial Object}\label{initial-object} +\section{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 @@ -49,13 +49,13 @@ \section{Initial Object}\label{initial-object} \begin{figure}[H] \centering -\fbox{\includegraphics[width=60mm]{images/initial.jpg}} +\includegraphics[width=60mm]{images/initial.jpg} \end{figure} \noindent However, even that doesn't guarantee the uniqueness of the initial object (if one exists). But it guarantees the next best thing: -uniqueness \emph{up to isomorphism}. Isomorphisms are very important in +uniqueness \newterm{up to isomorphism}. Isomorphisms are very important in category theory, so I'll talk about them shortly. For now, let's just agree that uniqueness up to isomorphism justifies the use of ``the'' in the definition of the initial object. @@ -77,7 +77,7 @@ \section{Initial Object}\label{initial-object} It's this family of morphisms that makes \code{Void} the initial object in the category of types. -\section{Terminal Object}\label{terminal-object} +\section{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 $a$ is ``more terminal'' @@ -93,7 +93,7 @@ \section{Terminal Object}\label{terminal-object} \begin{figure}[H] \centering -\fbox{\includegraphics[width=60mm]{images/final.jpg}} +\includegraphics[width=60mm]{images/final.jpg} \end{figure} \noindent @@ -132,7 +132,7 @@ \section{Terminal Object}\label{terminal-object} Insisting on uniqueness gives us just the right precision to narrow down the definition of the terminal object to just one type. -\section{Duality}\label{duality} +\section{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 @@ -141,10 +141,10 @@ \section{Duality}\label{duality} reversing all the arrows. The opposite category automatically satisfies all the requirements of a category, as long as we simultaneously redefine composition. If original morphisms -$f\Colon{}a\to b$ and $g\Colon{}b\to c$ composed -to $h\Colon{}a\to c$ with $h=g \circ f$, then the reversed -morphisms $f^{op}\Colon{}b\to a$ and $g^{op}\Colon{}c\to b$ will compose to -$h^{op}\Colon{}c\to a$ with $h^{op}=f^{op} \circ g^{op}$. And reversing +$f \Colon a \to b$ and $g \Colon b \to c$ composed +to $h \Colon a \to c$ with $h = g \circ f$, then the reversed +morphisms $f^{op} \Colon b \to a$ and $g^{op} \Colon c \to b$ will compose to +$h^{op} \Colon c \to a$ with $h^{op} = f^{op} \circ g^{op}$. And reversing the identity arrows is a (pun alert!) no-op. Duality is a very important property of categories because it doubles @@ -159,7 +159,7 @@ \section{Duality}\label{duality} It follows then that a terminal object is the initial object in the opposite category. -\section{Isomorphisms}\label{isomorphisms} +\section{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 @@ -188,11 +188,10 @@ \section{Isomorphisms}\label{isomorphisms} $g$ is the inverse of morphism $f$ if their composition is the identity morphism. These are actually two equations because there are two ways of composing two morphisms: - -\begin{Verbatim} -f . g = id -g . f = id -\end{Verbatim} +\begin{gather*} +f \circ g = \id \\ +g \circ f = \id +\end{gather*} When I said that the initial (terminal) object was unique up to isomorphism, I meant that any two initial (terminal) objects are isomorphic. That's actually easy to see. Let's suppose that we have two @@ -205,7 +204,7 @@ \section{Isomorphisms}\label{isomorphisms} \begin{figure}[H] \centering -\fbox{\includegraphics[width=1.56250in]{images/uniqueness.jpg}} +\includegraphics[width=40mm]{images/uniqueness.jpg} \caption{All morphisms in this diagram are unique.} \end{figure} @@ -230,7 +229,7 @@ \section{Isomorphisms}\label{isomorphisms} not the case here. This ``uniqueness up to unique isomorphism'' is the important property of all universal constructions. -\section{Products}\label{products} +\section{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 @@ -284,7 +283,7 @@ \section{Products}\label{products} \begin{figure}[H] \centering -\fbox{\includegraphics[width=1.56250in]{images/productpattern.jpg}} +\includegraphics[width=40mm]{images/productpattern.jpg} \end{figure} \noindent @@ -293,7 +292,7 @@ \section{Products}\label{products} \begin{figure}[H] \centering -\fbox{\includegraphics[width=1.56250in]{images/productcandidates.jpg}} +\includegraphics[width=40mm]{images/productcandidates.jpg} \end{figure} \noindent @@ -331,31 +330,31 @@ \section{Products}\label{products} But we haven't explored yet the other part of the universal construction: the ranking. We want to be able to compare two instances -of our pattern. We want to compare one candidate object \emph{c} and its +of our pattern. We want to compare one candidate object $c$ and its two projections \emph{p} and \emph{q} with another candidate object -\emph{c'} and its two projections \emph{p'} and \emph{q'}. We would like -to say that \emph{c} is ``better'' than \emph{c'} if there is a morphism -\emph{m} from \emph{c'} to \emph{c} --- but that's too weak. We also +$c'$ and its two projections \emph{p'} and \emph{q'}. We would like +to say that $c$ is ``better'' than $c'$ if there is a morphism +$m$ from $c'$ to $c$ --- but that's too weak. We also want its projections to be ``better,'' or ``more universal,'' than the -projections of \emph{c'}. What it means is that the projections +projections of $c'$. What it means is that the projections \emph{p'} and \emph{q'} can be reconstructed from \emph{p} and \emph{q} -using \emph{m}: +using $m$: -\begin{Verbatim}[commandchars=\\\{\}] +\begin{Verbatim} p' = p . m q' = q . m \end{Verbatim} \begin{figure}[H] \centering -\fbox{\includegraphics[width=1.56250in]{images/productranking.jpg}} +\includegraphics[width=40mm]{images/productranking.jpg} \end{figure} \noindent -Another way of looking at these equation is that \emph{m} +Another way of looking at these equation is that $m$ \emph{factorizes} \emph{p'} and \emph{q'}. Just pretend that these equations are in natural numbers, and the dot is multiplication: -\emph{m} is a common factor shared by \emph{p'} and \emph{q'}. +$m$ is a common factor shared by \emph{p'} and \emph{q'}. Just to build some intuitions, let me show you that the pair \code{(Int, Bool)} with the two canonical projections, \code{fst} @@ -364,26 +363,26 @@ \section{Products}\label{products} \begin{figure}[H] \centering -\fbox{\includegraphics[width=2.20833in]{images/not-a-product.jpg}} +\includegraphics[width=50mm]{images/not-a-product.jpg} \end{figure} \noindent The mapping \code{m} for the first candidate is: -\begin{Verbatim}[commandchars=\\\{\}] +\begin{Verbatim} m :: Int -> (Int, Bool) m x = (x, True) \end{Verbatim} Indeed, the two projections, \code{p} and \code{q} can be reconstructed as: -\begin{Verbatim}[commandchars=\\\{\}] +\begin{Verbatim} p x = fst (m x) = x q x = snd (m x) = True \end{Verbatim} The \code{m} for the second example is similarly uniquely determined: -\begin{Verbatim}[commandchars=\\\{\}] +\begin{Verbatim} m (x, _, b) = (x, b) \end{Verbatim} We were able to show that \code{(Int, Bool)} is better than either of @@ -391,7 +390,7 @@ \section{Products}\label{products} find some \code{m'} that would help us reconstruct \code{fst} and \code{snd} from \code{p} and \code{q}? -\begin{Verbatim}[commandchars=\\\{\}] +\begin{Verbatim} fst = p . m' snd = q . m' \end{Verbatim} @@ -405,12 +404,12 @@ \section{Products}\label{products} \code{q} ignore the second component of the triple, our \code{m'} can put anything in it. We can have: -\begin{Verbatim}[commandchars=\\\{\}] +\begin{Verbatim} m' (x, b) = (x, x, b) \end{Verbatim} or -\begin{Verbatim}[commandchars=\\\{\}] +\begin{Verbatim} m' (x, b) = (x, 42, b) \end{Verbatim} and so on. @@ -420,7 +419,7 @@ \section{Products}\label{products} to the cartesian product \code{(a, b)} that factorizes them. In fact, it just combines \code{p} and \code{q} into a pair. -\begin{Verbatim}[commandchars=\\\{\}] +\begin{Verbatim} m :: c -> (a, b) m x = (p x, q x) \end{Verbatim} @@ -433,10 +432,10 @@ \section{Products}\label{products} always exist, but when it does, it is unique up to a unique isomorphism. \begin{quote} -A \textbf{product} of two objects \emph{a} and \emph{b} is the object -\emph{c} equipped with two projections such that for any other object -\emph{c'} equipped with two projections there is a unique morphism -\emph{m} from \emph{c'} to \emph{c} that factorizes those projections. +A \textbf{product} of two objects $a$ and $b$ is the object +$c$ equipped with two projections such that for any other object +$c'$ equipped with two projections there is a unique morphism +$m$ from $c'$ to $c$ that factorizes those projections. \end{quote} \noindent @@ -449,38 +448,38 @@ \section{Products}\label{products} factorizer p q = \x -> (p x, q x) \end{Verbatim} -\section{Coproduct}\label{coproduct} +\section{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 -pattern, we end up with an object \emph{c} equipped with two -\emph{injections}, \code{i} and \code{j}: morphisms from \emph{a} -and \emph{b} to \emph{c}. +pattern, we end up with an object $c$ equipped with two +\emph{injections}, \code{i} and \code{j}: morphisms from $a$ +and $b$ to $c$. -\begin{Verbatim}[commandchars=\\\{\}] +\begin{Verbatim} i :: a -> c j :: b -> c \end{Verbatim} \begin{figure}[H] \centering -\fbox{\includegraphics[width=1.56250in]{images/coproductpattern.jpg}} +\includegraphics[width=40mm]{images/coproductpattern.jpg} \end{figure} \noindent -The ranking is also inverted: object \emph{c} is ``better'' than object -\emph{c'} that is equipped with the injections \emph{i'} and \emph{j'} -if there is a morphism \emph{m} from \emph{c} to \emph{c'} that +The ranking is also inverted: object $c$ is ``better'' than object +$c'$ that is equipped with the injections $i'$ and $j'$ +if there is a morphism $m$ from $c$ to $c'$ that factorizes the injections: -\begin{Verbatim}[commandchars=\\\{\}] +\begin{Verbatim} i' = m . i j' = m . j \end{Verbatim} \begin{figure}[H] \centering -\fbox{\includegraphics[width=1.56250in]{images/coproductranking.jpg}} +\includegraphics[width=40mm]{images/coproductranking.jpg} \end{figure} \noindent @@ -489,16 +488,16 @@ \section{Coproduct}\label{coproduct} to unique isomorphism. \begin{quote} -A \textbf{coproduct} of two objects \emph{a} and \emph{b} is the object -\emph{c} equipped with two injections such that for any other object -\emph{c'} equipped with two injections there is a unique morphism -\emph{m} from \emph{c} to \emph{c'} that factorizes those injections. +A \textbf{coproduct} of two objects $a$ and $b$ is the object +$c$ equipped with two injections such that for any other object +$c'$ equipped with two injections there is a unique morphism +$m$ from $c$ to $c'$ that factorizes those injections. \end{quote} \noindent In the category of sets, the coproduct is the \emph{disjoint union} of -two sets. An element of the disjoint union of \emph{a} and \emph{b} is -either an element of \emph{a} or an element of \emph{b}. If the two sets +two sets. An element of the disjoint union of $a$ and $b$ is +either an element of $a$ or an element of $b$. If the two sets overlap, the disjoint union contains two copies of the common part. You can think of an element of a disjoint union as being tagged with an identifier that specifies its origin. @@ -539,7 +538,7 @@ \section{Coproduct}\label{coproduct} separating data constructors with a vertical bar. The \code{Contact} example translates into the declaration: -\begin{Verbatim}[commandchars=\\\{\}] +\begin{Verbatim} data Contact = PhoneNum Int | EmailAddr String \end{Verbatim} Here, \code{PhoneNum} and \code{EmailAddr} serve both as @@ -547,7 +546,7 @@ \section{Coproduct}\label{coproduct} this later). For instance, this is how you would construct a contact using a phone number: -\begin{Verbatim}[commandchars=\\\{\}] +\begin{Verbatim} helpdesk :: Contact; helpdesk = PhoneNum 2222222 \end{Verbatim} @@ -556,7 +555,7 @@ \section{Coproduct}\label{coproduct} coproduct is a data type called \code{Either}, which is defined in the standard Prelude as: -\begin{Verbatim}[commandchars=\\\{\}] +\begin{Verbatim} Either a b = Left a | Right b \end{Verbatim} It is parameterized by two types, \code{a} and \code{b} and has two @@ -568,13 +567,13 @@ \section{Coproduct}\label{coproduct} injections \code{i} and \code{j}, the factorizer for \code{Either} produces the factoring function: -\begin{Verbatim}[commandchars=\\\{\}] +\begin{Verbatim} factorizer :: (a -> c) -> (b -> c) -> Either a b -> c factorizer i j (Left a) = i a factorizer i j (Right b) = j b \end{Verbatim} -\section{Asymmetry}\label{asymmetry} +\section{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 @@ -610,14 +609,14 @@ \section{Asymmetry}\label{asymmetry} morphism selects an element from the product set --- it selects a concrete pair. It also factorizes the two projections: -\begin{Verbatim}[commandchars=\\\{\}] +\begin{Verbatim} p = fst . m q = snd . m \end{Verbatim} When acting on the singleton value \code{()}, the only element of the singleton set, these two equations become: -\begin{Verbatim}[commandchars=\\\{\}] +\begin{Verbatim} p () = fst (m ()) q () = snd (m ()) \end{Verbatim} @@ -669,7 +668,7 @@ \section{Asymmetry}\label{asymmetry} symmetric, because they are invertible. In the category of sets, an isomorphism is the same as a bijection. -\section{Challenges}\label{challenges} +\section{Challenges} \begin{enumerate} \tightlist @@ -720,12 +719,12 @@ \section{Challenges}\label{challenges} allows multiple acceptable morphisms from it to \code{Either}. \end{enumerate} -\section{Bibliography}\label{bibliography} +\section{Bibliography} \begin{enumerate} \tightlist \item The Catsters, - \href{https://www.youtube.com/watch?v=upCSDIO9pjc}{Products and + \urlref{https://www.youtube.com/watch?v=upCSDIO9pjc}{Products and Coproducts} video. \end{enumerate} \ No newline at end of file diff --git a/src/content/1.6/Simple Algebraic Data Types.tex b/src/content/1.6/Simple Algebraic Data Types.tex index 49f78e7b..639da776 100644 --- a/src/content/1.6/Simple Algebraic Data Types.tex +++ b/src/content/1.6/Simple Algebraic Data Types.tex @@ -12,7 +12,7 @@ Let's have a closer look at product and sum types as they appear in programming. -\section{Product Types}\label{product-types} +\section{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; @@ -165,7 +165,7 @@ \section{Product Types}\label{product-types} 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. -\section{Records}\label{records} +\section{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 @@ -226,7 +226,7 @@ \section{Records}\label{records} The parentheses could be omitted in this case, because an infix operator has lower precedence than a function call. -\section{Sum Types}\label{sum-types} +\section{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 @@ -392,7 +392,7 @@ \section{Sum Types}\label{sum-types} 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. -\section{Algebra of Types}\label{algebra-of-types} +\section{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 @@ -512,7 +512,7 @@ \section{Algebra of Types}\label{algebra-of-types} \code{(1 + a*x)}, and use the distributive property. This leads to the following series: -\begin{Verbatim}[commandchars=\\\{\}] +\begin{Verbatim} x = 1 + a*x x = 1 + a*(1 + a*x) = 1 + a + a*a*x x = 1 + a + a*a*(1 + a*x) = 1 + a + a*a + a*a*a*x @@ -558,7 +558,7 @@ \section{Algebra of Types}\label{algebra-of-types} isomorphism between logic and type theory. We'll come back to it when we talk about function types. -\section{Challenges}\label{challenges} +\section{Challenges} \begin{enumerate} \tightlist diff --git a/src/content/1.7/Functors.tex b/src/content/1.7/Functors.tex index b4bd3c06..519da7b3 100644 --- a/src/content/1.7/Functors.tex +++ b/src/content/1.7/Functors.tex @@ -78,7 +78,7 @@ everything into one singularity. We'll see more of this functor when we discuss limits and colimits. -\section{Functors in Programming}\label{functors-in-programming} +\section{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 @@ -88,7 +88,7 @@ \section{Functors in Programming}\label{functors-in-programming} realizing that they were just that. I'm talking about definitions of types that were parameterized by other types. Let's see a few examples. -\subsection{The Maybe Functor}\label{the-maybe-functor} +\subsection{The Maybe Functor} The definition of \code{Maybe} is a mapping from type \code{a} to type \code{Maybe a}: @@ -134,7 +134,7 @@ \subsection{The Maybe Functor}\label{the-maybe-functor} \begin{figure}[H] \centering -\fbox{\includegraphics[width=3.12500in]{images/functormaybe.jpg}} +\includegraphics[width=3.12500in]{images/functormaybe.jpg} \end{figure} \noindent @@ -162,7 +162,7 @@ \subsection{The Maybe Functor}\label{the-maybe-functor} functor laws,'' but they simply ensure the preservation of the structure of the category. -\subsection{Equational Reasoning}\label{equational-reasoning} +\subsection{Equational Reasoning} To prove the functor laws, I will use \newterm{equational reasoning}, which is a common proof technique in Haskell. It takes advantage of the fact @@ -275,7 +275,7 @@ \subsection{Equational Reasoning}\label{equational-reasoning} equational reasoning if you implement \code{square} as a macro, with disastrous results. -\subsection{Optional}\label{optional} +\subsection{Optional} Functors are easily expressed in Haskell, but they can be defined in any language that supports generic programming and higher-order functions. @@ -341,7 +341,7 @@ \subsection{Optional}\label{optional} especially if, in the future, there are multiple functors overloading \code{fmap}? (We'll see more functors soon.) -\subsection{Typeclasses}\label{typeclasses} +\subsection{Typeclasses} So how does Haskell deal with abstracting the functor? It uses the typeclass mechanism. A typeclass defines a family of types that support @@ -407,7 +407,7 @@ \subsection{Typeclasses}\label{typeclasses} definitions for a lot of simple data types, including \code{Maybe}, are part of the standard Prelude library. -\subsection{Functor in C++}\label{functor-in-c} +\subsection{Functor in C++} Can we try the same approach in C++? A type constructor corresponds to a template class, like \code{optional}, so by analogy, we would @@ -442,7 +442,7 @@ \subsection{Functor in C++}\label{functor-in-c} \code{fmap} selects the overload. It totally ignores the more generic definition of \code{fmap}. -\subsection{The List Functor}\label{the-list-functor} +\subsection{The List Functor} To get some intuition as to the role of functors in programming, we need to look at more examples. Any type that is parameterized by another type @@ -529,7 +529,7 @@ \subsection{The List Functor}\label{the-list-functor} the new proposed C++ range library makes the functorial nature of ranges much more pronounced. -\subsection{The Reader Functor}\label{the-reader-functor} +\subsection{The Reader Functor} Now that you might have developed some intuitions --- for instance, functors being some kind of containers --- let me show you an example @@ -600,7 +600,7 @@ \subsection{The Reader Functor}\label{the-reader-functor} with the above implementation of \code{fmap} is called the reader functor. -\section{Functors as Containers}\label{functors-as-containers} +\section{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 @@ -700,7 +700,7 @@ \section{Functors as Containers}\label{functors-as-containers} the $\Delta_c$ functor I mentioned earlier --- the endo-functor case of a black hole. We'll be seeing more of it in the future. -\section{Functor Composition}\label{functor-composition} +\section{Functor Composition} It's not hard to convince yourself that functors between categories compose, just like functions between sets compose. A composition of two @@ -793,7 +793,7 @@ \section{Functor Composition}\label{functor-composition} same structures repeating themselves at many levels of abstraction. We'll see later that functors form categories as well. -\section{Challenges}\label{challenges} +\section{Challenges} \begin{enumerate} \tightlist diff --git a/src/content/1.8/Functoriality.tex b/src/content/1.8/Functoriality.tex index 50e7eff4..53a57b7a 100644 --- a/src/content/1.8/Functoriality.tex +++ b/src/content/1.8/Functoriality.tex @@ -4,7 +4,7 @@ mappings between objects in a category) can be extended to functors (which include mappings between morphisms). -\section{Bifunctors}\label{bifunctors} +\section{Bifunctors} Since functors are morphisms in $\Cat$ (the category of categories), a lot of intuitions about morphisms --- and functions in particular --- @@ -106,8 +106,7 @@ \section{Bifunctors}\label{bifunctors} 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). -\section{Product and Coproduct -Bifunctors}\label{product-and-coproduct-bifunctors} +\section{Product and Coproduct Bifunctors} An important example of a bifunctor is the categorical product --- a product of two objects that is defined by a \hyperref[products-and-coproducts]{universal @@ -159,8 +158,7 @@ \section{Product and Coproduct monoidal category (we still need to learn about naturality, before we can get there). -\section{Functorial Algebraic Data -Types}\label{functorial-algebraic-data-types} +\section{Functorial Algebraic Data Types} We've seen several examples of parameterized data types that turned out to be functors --- we were able to define \code{fmap} for them. @@ -319,7 +317,7 @@ \section{Functorial Algebraic Data same: You provide the behavior for the basic building blocks and sums and products, and let the compiler figure out the rest. -\section{Functors in C++}\label{functors-in-c} +\section{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 @@ -408,7 +406,7 @@ \section{Functors in C++}\label{functors-in-c} \end{Verbatim} This implementation can also be automatically derived by the compiler. -\section{The Writer Functor}\label{the-writer-functor} +\section{The Writer Functor} I promised that I would come back to the \hyperref[kleisli-categories-page]{Kleisli category} I described earlier. Morphisms in that category were @@ -482,8 +480,7 @@ \section{The Writer Functor}\label{the-writer-functor} an implementation of \code{fmap} for a given type constructor, one that preserves identity, then it must be unique. -\section{Covariant and Contravariant -Functors}\label{covariant-and-contravariant-functors} +\section{Covariant and Contravariant Functors} Now that we've reviewed the writer functor, let's go back to the reader functor. It was based on the partially applied function-arrow type @@ -549,7 +546,7 @@ \section{Covariant and Contravariant same way $F$ does, but when it comes to mapping morphisms, it reverses them. It takes a morphism $f \Colon b \to a$ in $\cat{C}$, maps it first to the opposite morphism $f^{op} \Colon a \to b$ -and then uses the functor $F$ on it, to get $F f^{op} \Colon F a \to F b$. +and then uses the functor $F$ on it, to get $F f^{op} \Colon F\ a \to F\ b$. Considering that $F a$ is the same as $G a$ and $F b$ is the same as $G b$, the whole trip can be described as: $G f \Colon (b \to a) \to (G a \to G b)$ @@ -562,7 +559,7 @@ \section{Covariant and Contravariant \begin{figure}[H] \centering -\fbox{\includegraphics[width=60mm]{images/contravariant.jpg}} +\includegraphics[width=60mm]{images/contravariant.jpg} \end{figure} \noindent @@ -599,7 +596,7 @@ \section{Covariant and Contravariant contramap = flip (.) \end{Verbatim} -\section{Profunctors}\label{profunctors} +\section{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 @@ -632,7 +629,7 @@ \section{Profunctors}\label{profunctors} \begin{figure}[H] \centering -\fbox{\includegraphics[width=60mm]{images/dimap.jpg}} +\includegraphics[width=60mm]{images/dimap.jpg} \caption{dimap} \end{figure} @@ -649,7 +646,7 @@ \section{Profunctors}\label{profunctors} Profunctors have their application in the Haskell lens library. We'll see them again when we talk about ends and coends. -\section{Challenges}\label{challenges} +\section{Challenges} \begin{enumerate} \tightlist diff --git a/src/content/1.9/Function Types.tex b/src/content/1.9/Function Types.tex index db952a02..c0150b9a 100644 --- a/src/content/1.9/Function Types.tex +++ b/src/content/1.9/Function Types.tex @@ -3,7 +3,7 @@ \begin{wrapfigure}[12]{R}{0pt} \raisebox{0pt}[\dimexpr\height-0.75\baselineskip\relax]{ -\fbox{\includegraphics[width=40mm]{images/set-hom-set.jpg}}}% +\includegraphics[width=40mm]{images/set-hom-set.jpg}}% \caption{Hom-set in Set is just a set} \end{wrapfigure} @@ -21,7 +21,7 @@ \pagebreak \begin{wrapfigure}[11]{R}{0pt} \raisebox{0pt}[\dimexpr\height]{ -\fbox{\includegraphics[width=40mm]{images/hom-set.jpg}}}% +\includegraphics[width=40mm]{images/hom-set.jpg}}% \caption{Hom-set in category C is an external set} \end{wrapfigure} @@ -31,7 +31,7 @@ to construct objects that represent hom-sets. Such objects are called \newterm{internal} hom-sets. -\section{Universal Construction}\label{universal-construction} +\section{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 @@ -67,7 +67,7 @@ \section{Universal Construction}\label{universal-construction} \begin{figure} \centering -\fbox{\includegraphics[width=60mm]{images/functionset.jpg}} +\includegraphics[width=60mm]{images/functionset.jpg} \caption{In Set we can pick a function $f$ from a set of functions $z$ and we can pick an argument $x$ from the set (type) $a$. We get an element $f x$ in the set (type) $b$.} @@ -85,7 +85,7 @@ \section{Universal Construction}\label{universal-construction} \begin{figure} \centering -\fbox{\includegraphics[width=60mm]{images/functionpattern.jpg}} +\includegraphics[width=60mm]{images/functionpattern.jpg} \caption{A pattern of objects and morphisms that is the starting point of the universal construction} \end{figure} @@ -110,7 +110,7 @@ \section{Universal Construction}\label{universal-construction} requiring that there be a unique mapping between candidate objects --- a mapping that somehow factorizes our construction. In our case, we'll decree that $z$ together with the morphism $g$ from -$z\times a$ to $b$ is \emph{better} than some other +$z \times a$ to $b$ is \emph{better} than some other $z'$ with its own application $g'$, if and only if there is a unique mapping $h$ from $z'$ to $z$ such that the application of $g'$ factors @@ -119,7 +119,7 @@ \section{Universal Construction}\label{universal-construction} \begin{figure} \centering -\fbox{\includegraphics[width=60mm]{images/functionranking.jpg}} +\includegraphics[width=60mm]{images/functionranking.jpg} \caption{Establishing a ranking between candidates for the function object} \end{figure} @@ -128,7 +128,7 @@ \section{Universal Construction}\label{universal-construction} $h \Colon z'\to z$, we want to close the diagram that has both $z'$ and $z$ crossed with $a$. What we really need, given the mapping $h$ from $z'$ -to $z$, is a mapping from $z'\times a$ to $z\times a$. +to $z$, is a mapping from $z' \times a$ to $z \times a$. And now, after discussing the \hyperref[functoriality]{functoriality of the product}, we know how to do it. Because the product itself is a functor (more precisely an endo-bi-functor), it's possible to lift pairs @@ -136,7 +136,7 @@ \section{Universal Construction}\label{universal-construction} but also products of morphisms. Since we are not touching the second component of the product -$z'\times a$, we will lift the pair of morphisms +$z' \times a$, we will lift the pair of morphisms $(h, \id)$, where $\id$ is an identity on $a$. So, here's how we can factor one application, $g$, out of another @@ -149,7 +149,7 @@ \section{Universal Construction}\label{universal-construction} of this as a symbolic name for one object, not to be confused with a Haskell typeclass constraint --- I'll discuss different ways of naming it later). This object comes with its own application --- a morphism -from $(a \Rightarrow b)\times{}a$ to $b$ --- which we will call +from $(a \Rightarrow b) \times a$ to $b$ --- which we will call $eval$ The object \code{$a \Rightarrow b$} is the best if any other candidate for a function object can be uniquely mapped to it in such a way that its application morphism $g$ factorizes through @@ -158,7 +158,7 @@ \section{Universal Construction}\label{universal-construction} \begin{figure}[H] \centering -\fbox{\includegraphics{images/universalfunctionobject.jpg}} +\includegraphics{images/universalfunctionobject.jpg} \caption{The definition of the universal function object. This is the same diagram as above, but now the object $a \Rightarrow b$ is \emph{universal}.} \end{figure} @@ -191,7 +191,7 @@ \section{Universal Construction}\label{universal-construction} This is why, in Haskell, we interpret the function type \code{a -> b} as the categorical function object $a \Rightarrow b$. -\section{Currying}\label{currying} +\section{Currying} Let's have a second look at all the candidates for the function object. This time, however, let's think of the morphism $g$ as a function @@ -316,7 +316,7 @@ \section{Currying}\label{currying} Of course that requires some amount of foresight or prescience on the part of a library writer. -\section{Exponentials}\label{exponentials} +\section{Exponentials} In mathematical literature, the function object, or the internal hom-object between two objects $a$ and $b$, is often @@ -373,8 +373,7 @@ \section{Exponentials}\label{exponentials} categorical exponential object --- which corresponds more to our idea of \emph{data}. -\section{Cartesian Closed -Categories}\label{cartesian-closed-categories} +\section{Cartesian Closed Categories} Although I will continue using the category of sets as a model for types and functions, it's worth mentioning that there is a larger family of @@ -415,8 +414,7 @@ \section{Cartesian Closed section that bicartesian closed categories, of which $\Set$ is a prime example, have some interesting properties. -\section{Exponentials and Algebraic Data -Types}\label{exponentials-and-algebraic-data-types} +\section{Exponentials and Algebraic Data Types} The interpretation of function types as exponentials fits very well into the scheme of algebraic data types. It turns out that all the basic @@ -427,7 +425,7 @@ \section{Exponentials and Algebraic Data prove them (such as adjunctions or the Yoneda lemma), but I'll list them here nevertheless as a source of valuable intuitions. -\subsection{Zeroth Power}\label{zeroth-power} +\subsection{Zeroth Power} \[a^{0} = 1\] In the categorical interpretation, we replace 0 with the initial object, @@ -455,7 +453,7 @@ \subsection{Zeroth Power}\label{zeroth-power} that can be passed to \code{absurd}. (And if you manage to pass it a never ending calculation, it will never return!) -\subsection{Powers of One}\label{powers-of-one} +\subsection{Powers of One} \[1^{a} = 1\] This identity, when interpreted in $\Set$, restates the definition @@ -468,7 +466,7 @@ \subsection{Powers of One}\label{powers-of-one} also think of it as the function \code{const} partially applied to \code{()}. -\subsection{First Power}\label{first-power} +\subsection{First Power} \[a^{1} = a\] This is a restatement of the observation that morphisms from the @@ -478,7 +476,7 @@ \subsection{First Power}\label{first-power} elements of the set \code{a} and functions that pick those elements, \code{() -> a}. -\subsection{Exponentials of Sums}\label{exponentials-of-sums} +\subsection{Exponentials of Sums} \[a^{b+c} = a^{b} \times a^{c}\] Categorically, this says that the exponential from a coproduct of two @@ -504,16 +502,14 @@ \subsection{Exponentials of Sums}\label{exponentials-of-sums} \end{minted} Here, \code{n} is an \code{Int} and \code{x} is a \code{Double}. -\subsection{Exponentials of -Exponentials}\label{exponentials-of-exponentials} +\subsection{Exponentials of Exponentials} \[(a^{b})^{c} = a^{b \times c}\] This is just a way of expressing currying purely in terms of exponential objects. A function returning a function is equivalent to a function from a product (a two-argument function). -\subsection{Exponentials over -Products}\label{exponentials-over-products} +\subsection{Exponentials over Products} \[(a \times b)^{c} = a^{c} \times b^{c}\] In Haskell: A function returning a pair is equivalent to a pair of @@ -523,14 +519,14 @@ \subsection{Exponentials over can be lifted to category theory and have practical application in functional programming. -\section{Curry-Howard Isomorphism}\label{curry-howard-isomorphism} +\section{Curry-Howard Isomorphism} I have already mentioned the correspondence between logic and algebraic data types. The \code{Void} type and the unit type \code{()} correspond to false and true. Product types and sum types correspond to -logical conjunction \ensuremath{\wedge} (AND) and disjunction \ensuremath{\vee} (OR). In this scheme, the -function type we have just defined corresponds to logical implication \ensuremath{\Rightarrow}. -In other words, the type \code{a->b} can be read as ``if +logical conjunction $\wedge$ (AND) and disjunction $\vee$ (OR). In this scheme, the +function type we have just defined corresponds to logical implication $\Rightarrow$. +In other words, the type \code{$a -> b$} can be read as ``if a then b.'' According to the Curry-Howard isomorphism, every type can be interpreted @@ -630,13 +626,13 @@ \section{Curry-Howard Isomorphism}\label{curry-howard-isomorphism} the theory is being formulated in Coq and Agda. Computers are revolutionizing the world in more than one way. -\section{Bibliography}\label{bibliography} +\section{Bibliography} \begin{enumerate} \tightlist \item Ralph Hinze, Daniel W. H. James, - \href{http://www.cs.ox.ac.uk/ralf.hinze/publications/WGP10.pdf}{Reason + \urlref{http://www.cs.ox.ac.uk/ralf.hinze/publications/WGP10.pdf}{Reason Isomorphically!}. This paper contains proofs of all those high-school algebraic identities in category theory that I mentioned in this chapter. diff --git a/src/content/2.1/Declarative Programming.tex b/src/content/2.1/Declarative Programming.tex index 8b93c74e..4eeba730 100644 --- a/src/content/2.1/Declarative Programming.tex +++ b/src/content/2.1/Declarative Programming.tex @@ -201,7 +201,7 @@ built in, rather than being defined by universal constructions; although there have been attempts at creating categorical programming languages (see, e.g., -\href{http://web.sfc.keio.ac.jp/~hagino/thesis.pdf}{Tatsuya +\urlref{http://web.sfc.keio.ac.jp/~hagino/thesis.pdf}{Tatsuya Hagino's thesis}). Whether used directly or not, categorical definitions justify diff --git a/src/content/2.2/Limits and Colimits.tex b/src/content/2.2/Limits and Colimits.tex index cb9e9fe3..6aa4ba1e 100644 --- a/src/content/2.2/Limits and Colimits.tex +++ b/src/content/2.2/Limits and Colimits.tex @@ -2,7 +2,7 @@ everything can be viewed from many angles. Take for instance the universal construction of the \hyperref[products-and-coproducts]{product}. Now that we know more about \hyperref[chap-functors]{functors} and -\hyperref[chap-natural-transformations]{natural transformations}, can we simplify and, possibly, generalize it? Let us +\hyperref[natural-transformations]{natural transformations}, can we simplify and, possibly, generalize it? Let us try. \begin{figure}[H] @@ -177,7 +177,7 @@ two projections) contains the information about both objects. And being universal means that it has no extraneous junk. -\section{Limit as a Natural Isomorphism}\label{limit-as-a-natural-isomorphism} +\section{Limit as a Natural Isomorphism} There is still something unsatisfying about this definition of a limit. I mean, it's workable, but we still have this commutativity condition @@ -323,7 +323,7 @@ \section{Limit as a Natural Isomorphism}\label{limit-as-a-natural-isomorphism} category; so our natural isomorphism relates two hom-sets, which points at an even more general relationship called an adjunction. -\section{Examples of Limits}\label{examples-of-limits} +\section{Examples of Limits} We've seen that the categorical product is a limit of a diagram generated by a simple category we called $\cat{2}$. @@ -617,7 +617,7 @@ \section{Colimits} diagram called a span, generated by the category $1\leftarrow2\rightarrow3$. -\section{Continuity}\label{continuity} +\section{Continuity} I said previously that functors come close to the idea of continuous mappings of categories, in the sense that they never break existing @@ -696,7 +696,7 @@ \section{Continuity}\label{continuity} neighborhoods. Open sets, which define topology, form a category (a poset). -\section{Challenges}\label{challenges} +\section{Challenges} \begin{enumerate} \tightlist diff --git a/src/content/2.3/Free Monoids.tex b/src/content/2.3/Free Monoids.tex index d3dce544..6c1e2e13 100644 --- a/src/content/2.3/Free Monoids.tex +++ b/src/content/2.3/Free Monoids.tex @@ -63,7 +63,7 @@ construction. What we have just done is to construct a \newterm{free monoid} from the set of generators $\{a, b\}$. -\section{Free Monoid in Haskell}\label{free-monoid-in-haskell} +\section{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 @@ -112,7 +112,7 @@ \section{Free Monoid in Haskell}\label{free-monoid-in-haskell} required by the laws? I'll show you that this follows directly from the universal construction. -\section{Free Monoid Universal Construction}\label{free-monoid-universal-construction} +\section{Free Monoid Universal Construction} If you recall our previous experiences with universal constructions, you might notice that it's not so much about constructing something as about @@ -262,7 +262,7 @@ \section{Free Monoid Universal Construction}\label{free-monoid-universal-constru We'll come back to free monoids when we talk about adjunctions. -\section{Challenges}\label{challenges} +\section{Challenges} \begin{enumerate} \tightlist diff --git a/src/content/2.4/Representable Functors.tex b/src/content/2.4/Representable Functors.tex index 02ceb6f6..8e94d47d 100644 --- a/src/content/2.4/Representable Functors.tex +++ b/src/content/2.4/Representable Functors.tex @@ -332,7 +332,7 @@ \section{Representable Functors} with performance at all, category theory provides ample opportunities to explore alternative implementations that have practical value. -\section{Challenges}\label{challenges} +\section{Challenges} \begin{enumerate} \tightlist @@ -359,12 +359,12 @@ \section{Challenges}\label{challenges} \code{tabulate} and \code{index}. \end{enumerate} -\section{Bibliography}\label{bibliography} +\section{Bibliography} \begin{enumerate} \tightlist \item The Catsters video about - \href{https://www.youtube.com/watch?v=4QgjKUzyrhM}{representable - functors}.\urlfootnote{https://www.youtube.com/watch?v=4QgjKUzyrhM} + \urlref{https://www.youtube.com/watch?v=4QgjKUzyrhM}{representable + functors}. \end{enumerate} \ No newline at end of file diff --git a/src/content/2.5/The Yoneda Lemma.tex b/src/content/2.5/The Yoneda Lemma.tex index f69c8ba4..5da768b4 100644 --- a/src/content/2.5/The Yoneda Lemma.tex +++ b/src/content/2.5/The Yoneda Lemma.tex @@ -354,10 +354,10 @@ \section{Challenges} functor. \end{enumerate} -\section{Bibliography}\label{bibliography} +\section{Bibliography} \begin{enumerate} \tightlist \item - \href{https://www.youtube.com/watch?v=TLMxHB19khE}{Catsters} video.\urlfootnote{https://www.youtube.com/watch?v=TLMxHB19khE} + \urlref{https://www.youtube.com/watch?v=TLMxHB19khE}{Catsters} video. \end{enumerate} \ No newline at end of file diff --git a/src/content/2.6/Yoneda Embedding.tex b/src/content/2.6/Yoneda Embedding.tex index 22a3521b..7e6f4bf5 100644 --- a/src/content/2.6/Yoneda Embedding.tex +++ b/src/content/2.6/Yoneda Embedding.tex @@ -156,8 +156,8 @@ \section{Application to Haskell} The Yoneda embedding also explains some of the alternative representations of data structures in Haskell. In particular, it -provides a \href{https://bartoszmilewski.com/2015/07/13/from-lenses-to-yoneda-embedding/} -{very useful representation}\urlfootnote{https://bartoszmilewski.com/2015/07/13/from-lenses-to-yoneda-embedding/} +provides a \urlref{https://bartoszmilewski.com/2015/07/13/from-lenses-to-yoneda-embedding/} +{very useful representation} of lenses from the \code{Control.Lens} library. \section{Preorder Example} diff --git a/src/content/3.1/It's All About Morphisms.tex b/src/content/3.1/It's All About Morphisms.tex index df24dad8..58563284 100644 --- a/src/content/3.1/It's All About Morphisms.tex +++ b/src/content/3.1/It's All About Morphisms.tex @@ -6,7 +6,7 @@ language to describe a lot of constructions we've studied before, so it might help to review them too. -\section{Functors}\label{functors} +\section{Functors} To begin with, you should really think of functors as mappings of morphisms --- the view that's emphasized in the Haskell definition of @@ -19,7 +19,7 @@ \section{Functors}\label{functors} the composition of \newterm{lifted} morphisms, the mapping of their endpoints is pretty much determined. -\section{Commuting Diagrams}\label{commuting-diagrams} +\section{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 @@ -47,7 +47,7 @@ \section{Commuting Diagrams}\label{commuting-diagrams} of the assembly language for the higher level language of natural transformations. -\section{Natural Transformations}\label{natural-transformations} +\section{Natural Transformations} In general, natural transformations are very convenient whenever we need a mapping from morphisms to commuting squares. Two opposing sides of a @@ -198,7 +198,7 @@ \section{Asymmetry of Hom-Sets} A preorder is a thin category --- all hom-sets are either singletons or empty. We can visualize a general category as a ``thick'' preorder. -\section{Challenges}\label{challenges} +\section{Challenges} \begin{enumerate} \tightlist diff --git a/src/content/3.13/Topoi.tex b/src/content/3.13/Topoi.tex index e40fe14c..607875ea 100644 --- a/src/content/3.13/Topoi.tex +++ b/src/content/3.13/Topoi.tex @@ -246,7 +246,7 @@ \section{Topoi and Logic} truth object provides a more general framework for modeling interesting logics. -\section{Challenges}\label{challenges} +\section{Challenges} \begin{enumerate} \tightlist diff --git a/src/content/3.14/Lawvere Theories.tex b/src/content/3.14/Lawvere Theories.tex index 372f804d..2eeb67d4 100644 --- a/src/content/3.14/Lawvere Theories.tex +++ b/src/content/3.14/Lawvere Theories.tex @@ -3,7 +3,7 @@ Eugenio Moggi turned his attention to Lawvere theories rather than monads. Let's explore that universe. -\section{Universal Algebra}\label{universal-algebra} +\section{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 @@ -268,7 +268,7 @@ \section{The Theory of Monoids} structure of monoids. It is a single theory that distills the structure of all possible monoids, in the sense that the models of this theory span the whole category $\cat{Mon}$ of monoids. We've already seen a -\hyperref[chap-free-monoids]{universal +\hyperref[free-monoids]{universal construction}, which showed that every monoid can be obtained from an appropriate free monoid by identifying a subset of morphisms. So a single free monoid already generalizes a whole lot of monoids. There diff --git a/src/content/3.15/Monads, Monoids, and Categories.tex b/src/content/3.15/Monads, Monoids, and Categories.tex index 0438c971..f100c526 100644 --- a/src/content/3.15/Monads, Monoids, and Categories.tex +++ b/src/content/3.15/Monads, Monoids, and Categories.tex @@ -330,7 +330,7 @@ \section{Challenges} What's a monad algebra for a monad in $\cat{Span}$? \end{enumerate} -\section{Bibliography}\label{bibliography} +\section{Bibliography} \begin{enumerate} \tightlist \item diff --git a/src/content/3.2/Adjunctions.tex b/src/content/3.2/Adjunctions.tex index ecb40b20..ee4ed653 100644 --- a/src/content/3.2/Adjunctions.tex +++ b/src/content/3.2/Adjunctions.tex @@ -576,7 +576,7 @@ \section{Exponential from Adjunction} ``the'' exponential. This property translates to adjunctions as well: if a functor has an adjoint, this adjoint is unique up to isomorphism. -\section{Challenges}\label{challenges} +\section{Challenges} \begin{enumerate} \tightlist diff --git a/src/content/3.3/Free-Forgetful Adjunctions.tex b/src/content/3.3/Free-Forgetful Adjunctions.tex index be5a44da..9a91f089 100644 --- a/src/content/3.3/Free-Forgetful Adjunctions.tex +++ b/src/content/3.3/Free-Forgetful Adjunctions.tex @@ -47,7 +47,7 @@ $U$ is the free functor that builds free monoids from their generator sets. The adjunction follows from the free monoid universal construction we've discussed before.\footnote{See ch.13 on -\hyperref[chap-free-monoids]{free monoids}.} +\hyperref[free-monoids]{free monoids}.} In terms of hom-sets, we can write this adjunction as: \[\cat{arg}(F x, m) \cong \Set(x, U m)\] @@ -126,7 +126,7 @@ \code{replicate} creates a list of length \code{n} pre-filled with a given value --- here, the unit. -\section{Some Intuitions}\label{some-intuitions} +\section{Some Intuitions} What follows are some hand-waving arguments. Those kind of arguments are far from rigorous, but they help in forming intuitions. diff --git a/src/content/3.5/Monads and Effects.tex b/src/content/3.5/Monads and Effects.tex index 7cd31dc7..b85edb0d 100644 --- a/src/content/3.5/Monads and Effects.tex +++ b/src/content/3.5/Monads and Effects.tex @@ -310,7 +310,7 @@ \subsection{Write-Only State} return a = Writer (a, mempty) \end{Verbatim} -\subsection{State}\label{state} +\subsection{State} Functions that have read/write access to state combine the embellishments of the \code{Reader} and the \code{Writer}. You may @@ -599,7 +599,7 @@ \subsection{Interactive Output} which ``Hello '' is already on the screen. It outputs a new Universe, with ``Hello World!'' on the screen. -\section{Conclusion}\label{conclusion} +\section{Conclusion} Of course I have just scratched the surface of monadic programming. Monads not only accomplish, with pure functions, what normally is done diff --git a/src/content/3.7/Comonads.tex b/src/content/3.7/Comonads.tex index 2a9453dd..dff08a48 100644 --- a/src/content/3.7/Comonads.tex +++ b/src/content/3.7/Comonads.tex @@ -493,7 +493,7 @@ \section{The Store Comonad} 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. -\section{Challenges}\label{challenges} +\section{Challenges} \begin{enumerate} \tightlist diff --git a/src/ctfp.tex b/src/ctfp.tex index 017530c4..531e5de5 100644 --- a/src/ctfp.tex +++ b/src/ctfp.tex @@ -10,6 +10,7 @@ % ********************************************************** % % HISTORY: +% * Version 0.2 (October, 2017) - Math typesetting and lots of tweaks! % % * Version 0.1 (September, 2017) by Igal Tabachnik. % Based on the SICP PDF work of Andres Raba et al. @@ -41,7 +42,7 @@ \vspace{1.26em} \noindent -Version 0.1, September 2017\\ +Version 0.2, October 2017\\ \vspace{1.6em} \noindent @@ -94,7 +95,7 @@ \chapter{Products and Coproducts}\label{products-and-coproducts} \chapter{Simple Algebraic Data Types}\label{simple-algebraic-data-types} \subfile{content/1.6/Simple Algebraic Data Types} -\chapter{Functors}\label{chap-functors} +\chapter{Functors}\label{functors} \subfile{content/1.7/Functors} \chapter{Functoriality}\label{functoriality} @@ -103,7 +104,7 @@ \chapter{Functoriality}\label{functoriality} \chapter{Function Types}\label{function-types} \subfile{content/1.9/Function Types} -\chapter{Natural Transformations}\label{chap-natural-transformations} +\chapter{Natural Transformations}\label{natural-transformations} \subfile{content/1.10/Natural Transformations} \part{Part Two} @@ -114,7 +115,7 @@ \chapter{Declarative Programming}\label{declarative-programming} \chapter{Limits and Colimits}\label{limits-and-colimits} \subfile{content/2.2/Limits and Colimits} -\chapter{Free Monoids}\label{chap-free-monoids} +\chapter{Free Monoids}\label{free-monoids} \subfile{content/2.3/Free Monoids} \chapter{Representable Functors}\label{representable-functors}