Are there any more comprehensible primers out there or is this just a field of mathematics that I shouldn't expect to understand without years of prior study in other requisite fields? Or am I better off building something in Haskell and learning by doing? I know some discrete math, but all attempts at broaching category theory have been so far totally unsuccessful for me.
The branch of math itself would be mostly useless anyway, because it is mostly concerned about relations between categories, and as programmers, you usually work just within a single category, category of functions and types in your programming languages :-)
But from the practical, design-pattern viewpoint, I would suggest trying purescript :-)
My journey was working through the purescript book [1] up to the Applicative Validation chapter. And then I played around with the flare backend in try-purescript [2]. And then it clicked for me and I was suddenly able to read and comprehend Typeclassopedia [3] :-)
[1] https://leanpub.com/purescript/read [2] http://try.purescript.org/?backend=flare&session=a06d83dd-d0... [3] https://wiki.haskell.org/Typeclassopedia
You mention Applicative Functors, which form another (different) category where arrows from a to b are on the form `f (a -> b)` and composition and identity laws of these arrows are equivalent to the applicative laws.
Way he explained it, they often were searching for relations between categories that didn't at all intersect.
And way I was learning the applications of category theory in i.e. haskel, I viewed it more as learning about algebraic structures in the category of haskel types and functions.
So right now I have reasonable idea about i.e. applicative functors in haskel. But thinking about applicative functors as their own category is one abstraction step above what I am usually used to :-)
If you take the natural numbers N = {0, 1, ...} as a set and + as a binary operator forming a monoid (N, +, 0), then the arrows would correspond to (. + 0), (. + 1), (. + 2) etc. Here (. + 0) can be seen as the identity arrow, and composition of arrows (. + a) and (. + b) yields a new arrow (. + (a+b)).
For example, for each N, there is a group of invertible N by N matrices. If we want to allow non-square matrices too, we can bundle them up as a category:
- The objects are the natural numbers
- A map from N to M is an M row by N column matrix
- We compose A : N -> M and B : M -> K by multiplying them as matrices to get BA : N -> K. The objects (i.e., the dimensions) are type checking which things we can and can't multiply
1) Groups have an inverse operation, categories don't.
2) You can compose any two elements in a group, whereas in a category the input and output types have to match up.
But expect it to take some time. (10 Videos, most are around 1h, i needed to pause several times and think or try something out)
This also needs a lot of time and effort to comprehend!
I'm currently working through Conceptual Mathematics (an intro category theory book), and while the Haskell book has some overlap, it's been extremely minor. The main thing I can think of at the moment is determining the number of arbitrary maps that exist between sets. There is some overlap of things like monoids and functors, but even those have a different, more nuanced treatment in category theory (for example, the relatively simple fact that endomaps are functorial interpretations of the sum monoid was new to me, coming from that haskell book).
"Information is inherently dynamic; the same ideas can be organized and reorganized in countless ways, and the ability to translate between such organizational structures is becoming increasingly important in the sciences. Category theory offers a unifying framework for information modeling that can facilitate the translation of knowledge between disciplines."
[1] https://mitpress.mit.edu/books/category-theory-sciences
[2] https://github.com/mmai/Category-Theory-for-the-Sciences
Experience has shown that without a maths background learning CT is extremely difficult. Almost everybody basically fails.
As somebody who taught himself CT without a math background, I suggest to expect between 100 and 300 hours of serious, intensive study before CT begins to make sense.
My recommendation is to bite the bullet and study one of the many good textbooks, and solve every exercise, and rote-learn the definitions until they become second nature. You will know you've understood CT when see why Peter Freyd's quip "[t]he purpose of [category theory] is to show that which is trivial is trivially trivial" is apt. The key concepts to learn are: category, functor, natural transformation, adjunction, universal property, limit and dualisation. Once you understand those, an extremely large number of prima facie separate mathematical concepts can be seen as instances of the same few trivial ideas. But they must be rephrased in this seemingly alien and unnatural language called CT. My favourite example is Lawvere's unification of most known paradoxa (e.g. Cantor, Russell, Goedel, Tarski) as a basically a trivial fixpoint [1]. Note that after Lawvere had realised what most paradoxa have in common using a categorical re-formulation, it then became trivial to get the same insight without CT [2].
Let me illustrate the power of looking at a phenomenon using a new language with the example of computation itself: we have two dominant abstractions of computation:
- Turing machines
- Lambda calculus
Simplifying only a tiny bit: Turing machines gave us the theory of computational complexity but has not been helpful at all in the development of programming languages in general, and typing systems in particular; in contrast, lambda-calculus has been the foundation of most work on programming languages in general and practically all work on types. Yet lambda-calculus has been mostly silent on complexity theory (although [3] is the beginning of a rapprochement).
Finally, let me state my belief that the average programmer has currently no need to understand CT. The main categorical concept that has filtered down to conventional programming are monads, and monads can be explained and understood completely without reference to CT.
[1] F. W. Lawvere, Diagonal arguments and cartesian closed categories.
[2] N. S. Yanofsky, A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points.
in the lingua franca of javascript.
var timesThree = (x => x * 3)
//for this function 0 is a fixed point...
var a = 0
console.log(a == timesThree(a))
//7 is not a fixed point
var b = 7
console.log(b == timesThree(b))The proof, if you are interested, is not difficult. Let sub be the function that describes, via codes, substituting the (numeral n_ of the number) n for a free variable v of a formula χ : sub(<χv>, n_) = <χn_>. Then the PROOF is: consider ψ(sub(v,v)), call it θv, let m be <θv> and let φ be θm_. Then, provably, φ <=> ψ(sub(m_,m_)) <=> ψ(sub(<θv>,m_)) <=> ψ(<θm_>) <=> ψ(<φ>). Ta-da!
Goedel used this to get the "formula that says I am not provable", φ <=> not Prov(<φ>).
explain the fixed point idea
The key insight behind Lawvere's abstract framework to paradoxa is the the general existence of certain fixpoints.
Definition. We say that a set B has the fixpoint property if any function f:B→B has a fixpoint (i.e. f b = b for some b in B).
With this convenient definition, we are now ready to state and prove Lawvere's ridiculously simple and yet great theorem.
Theorem (Lawvere). If e:A→(A→B) is a surjective function, then B has the fixed point property.
The proof is quite easy. Let e:A→(A→B) be surjective. We have to show that B has the fixpoint property. That means for every f:B→B there is b∈B such that f(b)=b. Choose a function f:B→B and define the function g:A→B by setting
a ↦ f (e a a)
e a0 = g.
f (g a0) = f (e a0 a0) = g a0
Now many/most paradoxa are special cases of Lawvere's theorem. But for each paradox, the specific functions involved are a bit different. Let's look at an example.
Theorem (Cantor). There is no surjection e:A→Pow(A).
To see why this is true, note that Pow(A) is isomorphic to A→Bool. But there is a function on Bool that has no fixpoints, for example negation ¬:Bool→Bool, contradicting Lawvere's theorem.
---------------
Well, what does it mean that A can speak about itself? To approach an answer, we could maybe first ask a simpler question: what does it mean to speak about A? How about this for an answer: to speak about A means to say something about A's elements. What does it mean to say something about A's elements? Maybe stating whether any given element a∈A has a property of interest? But what's a property? Easy: a property of A's elements is a function
p:A→Bool
A→Bool
A→(A→Bool)
Are there any non-singleton sets with the fixpoint property?
> a ↦ f (e a a)
Don't you mean
a ↦ e a a
I won't pretend I absorbed all (or even most) of it, but I at least understand the "Standard Haskell Joke" now (which is a funny misquote from his book)[1][2]. I also understand much more clearly why Haskell is so associated with Category Theory.
[1]: "A monad is just a monoid in the category of endofunctors, what's the problem?"
[2]: What MacLane actually wrote is:
All told, a monad in X is just a monoid in the category of endofunctors of X, with product × replaced by composition of endofunctors and unit set by the identity endofunctor.