Category Theory for Programmers (2014)
bartoszmilewski.com
bartoszmilewski.com
1. Wasn't Feynman the one who was promoting replacing classical mechanics with relativity for freshman physics? How has that turned out?
2. Fuzzy logic makes a similar argument. Bart Kowasaki down in San Diego I believed proved mathematically that fuzzy logic equates Calculus and Nyquist equations. I'm probably not getting that quite right. But, Fuzzy Logic was called the "cocaine of math" and yet the Japanese have done quite well in using fuzzy math in software and manufacturing. The arguments put forth here about why every developer should learn category theory smack of the same arguments that have been made about Fuzzy logic and why fuzzy math should be taught in elementary school. I personally like and use fuzzy logic for programming but wide spread adoption of fuzzy logic never took hold. From what I've read of Category Theory, Fuzzy Logic seems to have a better argument as a programming shift because Fuzzy is a lot less abstract. Just start with a bunch of if statements that approximate the math.
Category theory is good for making extremely watertight conceptual arguments for discrete properties being preserved under transformations: it's "general abstract nonsense", yes (a famous characterization of the subject) but it really does elucidate the underlying structures in common across a lot of different mathematical settings.
If there's something wrong with the computational flavour of category theory, it's probably that it lacks fuzziness and is too much part of the linguistic/logical picture of the world. Giuseppe Longo, a category theorist, has a paper about this: http://www.di.ens.fr/users/longo/files/PhilosophyAndCognitio...
http://mathoverflow.net/questions/169187/what-non-categorica...
I suspect the reasons are broadly analogous. To paraphrase a quote of Atiyah's, the usefulness of theory is that once a field is complex enough, a little bit of it can serve to provide "organizing principles" (quoting Qiaochu Yuan from the MO post above) that help both learners (who can exploit similarities in different fields so that unfamilar things feel less alien) and experts (for whom many things are made easier, or even possible, by working at higher levels of abstraction[1]).
Knowledge just keeps piling up, and abstraction is one way of increasing the "density" of information one takes in so that one doesn't have to spend one's whole life trying to learn enough to work -- or, in the researcher's case, getting to the frontiers of current knowledge.
[0]: Roughly, my understanding of it is that it's what happens when you don't require properties like associativity, but say that (ab)c should be "deformable" into a(bc) in some way. Complications arise, interesting stuff happens. The usual.
[1]: Akin to the birds of Freeman Dyson's "birds and frogs".
Still somewhat shaken to this day by that very first meeting, it really didn't go that well.
I really don't grok the math behind it and it is very nice to see this pop up, and Bartosz definitely knows his stuff. I'll give it another whirl. Hats off to him for trying to make it approachable.
Also Brian Beckman and others have often had interesting things to say in these areas.
http://rebcabin.github.io/blog/2013/03/17/category-theory-re...
These days I understand the formal math behind it even less than I used to, which is to say abysmally; however it did teach me some things about how to think about composition that have subconsciously been influential I think over the years.
Nice post.
http://logicaltypes.blogspot.com/2015/08/pure-functional-pro...
Not that being maintainable isn't a worthy goal or that expressiveness and DSLs can't be maintainable, just wondering why it would be the primary goal.
IS CT only used when writing a piece of code that's supposed to be long living and have regular updates or something?
Let's take something like Clojure. I get immutable data, sane multithreading (I haven't had thread related problems in my code for years), etc. All without monads. Whenever I've started doing things like introducing state monads, or seen code involving applicative and "free" stuff, it basically becomes an opaque blob of functions. Zero ability to have the code self introspect or to leverage that pile of functions.
The better method is immutable data and data-first designs. Data is searchable, introspect-able, and transformable. Most CT stuff is all about composing functions via functions. Making your entire system opaque, at least from the point of view of the program itself.
And then there's languages like Eff that completely remove the need for stuff like monads: http://math.andrej.com/eff/
So yeah, for me it's been more-or-less a waste of time reading up on this stuff.
Specifically, the semantics of Eff involve free Monads.
As for the semantics of algebraic effects and handlers, if you are not really interested I won't bore you with a long winded explanation. Suffice it to say that you can get the advantages of Eff in Haskell by using free Monads (the syntax of Eff is nicer though).
If someone ever cracks the speed thing, I bet you'll see a lot more Haskell with Eff monads in it.
data State a self = Get self | Put a self
class State repr where
get :: repr a
put :: a -> repr ()
With the first implementation we write a function that interprets the adt, writing different interpreters is easy. We parametrized over self so we can combine languages by combining their adt's and give that as self. To tie the knot we use use recursion and end up with the free monad.With the second version we depend on multiple type classes to combine languages and implement them for different types to get different interpreters. The big advantage with this approach is that we don't have to construct the adt's before interpreting which is where the speed difference comes from.
Tl;dr: if you want to go fast you have to skip constructing adts and if you do that you end up with something like haskell's mtl.
I think if folks are interested, they should investigate CT for it's own sake (it is interesting mathematically) and not for some expected payoff.
I will say that though I only have a basic understanding, I at least acknowledge that go far with it seem to be more comfortable with how "things can be embedded in other things" and "prove compositional properties" at least in certain carefully constructed situations.
To me, the main value in learning FP CT is becoming handy at recognizing more of the patterns underlying the code I've been writing and working on for ages.
Consider the GoF Design Patterns book -- if you haven't been programming very long, many of the patterns might look odd or needless, but the more code you work on, the more you start to recognize the patterns as applied in real life.
Category theory for programming is like that, plus with some added formalism that proves how it's safe/possible to compose these patterns.
In particular, the lamba calculus is closely related to Cartesian closed categories, which are in turn related to topoi (which are used in many cases of mathematical logic). And from there it's a small leap to probability and generalizations of probability theory.
So basically, if you're a programming language designer with esoteric tastes, category theory contains some great abstractions.
Here's an example showing how to represent quantum superposition as a monad: http://blog.sigfpe.com/2007/02/monads-for-vector-spaces-prob... If this kind of thing makes you drool, go learn some category theory. :-)
They're common patterns a lot of people use without knowing anything about CT, for example if you fold/reduce over a collection with an initial value, and the collection may be empty, you're looking at a monoidal operation. You can call the initial value a constant identity. Like sum, product.
If you fold/reduce over a collection where the collection may not be empty, and you need to use the first element as the initial value, you're looking at a semigroup operation. Like min/max/mean.
What are some programming applicable Category Theory topics that aren't covered in abstract algebra?
"By the way, in addition to all the existing monoids you know (Ints under '+', strings, lists...), functions under function composition also form a monoid. Here's an example."
Isn't that pretty much getting them to the same place? Do they really need a study of category theory?
Not quite function composition, but given a type a, (a ->) is a monad (the so called "reader monad"). We have
return :: x -> (a -> x)
return x = \a -> x
(>>=) :: (a -> x) -> (x -> (a -> y)) -> (a -> y)
m >>= f = \a -> f (m a) a
(Incidentally, these are two of the Łukasiewicz axioms for propositional calculus.)It is a functor with
fmap :: (x -> y) -> (a -> x) -> (a -> y)
fmap f m = \a -> f (m a)
In the case x=y, then fmap takes the monoid of functions on x to the monoid of functions on (a -> x).Venturing into more abstract territory, "a monad is a monoid in the category of endofunctors of a category C." (This has never helped me with understanding how to use monads in Haskell.) Basically, the choice of endofunctor is the type constructor for the monad, the unit map is `return` and the composition map is `join`.
> return x = \a -> x
>
> (>>=) :: (a -> x) -> (x -> (a -> y)) -> (a -> y)
> m >>= f = \a -> f (m a) a
>(Incidentally, these are two of the Łukasiewicz axioms for propositional calculus.)
Also the K and S in SKI combinator calculus https://en.wikipedia.org/wiki/SKI_combinator_calculus
return :: a -> a
return = id
join :: a -> a
join = id
If this were isomorphic to the function composition monoid, there would be some way to interpret join as function composition, but I don't see it. Please show me if you know the isomorphism! (My thinking is a bit fuzzy on this, but it appears to me that the identity monad is actually isomorphic to a trivial monoid --- if you want, you can model the trivial monoid as the one-element set {0} under addition.)Bind is
(>>=) :: a -> (a -> b) -> b
(>>=) = flip id
that is, function application. Still no function composer in sight, though.This article seems to imply a correlation between the fish operator (<=<) and composition. Specifically his section on Kleisli monad.
http://www.haskellforall.com/2012/08/the-category-design-pat...
But I don't know the space well enough to know if that's answering your question.
Monads are like a monoid at the type level plus a bunch of coherence rules. For every type a, there is a "composition" m (m a) -> m a and a "unit" a -> m a. (Compare with a monoid, where there is a composition m x m -> m and a unit {1} -> m.) Also, the composition must be natural in the sense that whenever there is a map f :: a -> b then you have a bunch of "commuting squares": the composition m (m a) -> m (m b) -> m b must equal m (m a) -> m a -> m b and the composition a -> m a -> m b must equal a -> b -> m b. (Some of these maps are fmap f or fmap (fmap f).)
The naturality thing is important and shows up quite a lot, and category theory was invented to understand naturality. It's sort of a higher higher order functional programming.
Clearly much more to learn.
Thanks - While I did have this vague idea, and it says it from the types, seeing it written out in this way was clarifying.
> Category theory is extreme in the sense that it actively discourages us from looking inside the objects. An object in category theory is an abstract nebulous entity. All you can ever know about it is how it relates to other object — how it connects with them using arrows.
I think it's a great way to learn a different approach to solving math problems and, more importantly, computer science problems. When you start to think of objects not as what they are but what they can be, you get an extremely natural inclination towards immutability and, assuming your chosen language has a powerful type system, an awesome "free" mitigation against programming errors.
With category theory, you easily formulate your thoughts into function composition, and can more readily rely on the type system to validate your code. This is pretty much what you must do in Haskell, but it's useful in imperative languages as well. There's a reason functional paradigms are leaking into Java, C++, Python, etc: they're mighty useful.
I think you're being a bit generous saying we are doing CT in programming languages. Fine to say inspired by CT, but the OP comment is much more true than what we do in say Haskell. Haskell encourages composition but it does in fact look into (pattern match) on data all the time
[0]: http://rea.tech/how-we-used-category-theory-to-solve-a-probl...
My impression so far is that CT teaches you a set of orthogonal abstractions (call them patterns if you like) that will allow you to talk about ideas very precisely. To some degree, being able to talk about ideas makes it easier to have new ones.
In yesterday's lecture, we learned about products (think: tuple types) in CT, and of course their definition is more abstract than that. Now I know that other things can be products, too -- and next time I'll see one of them, I'll try thinking of that as a tuple.
Additionally, next time we'll flip the arrows in the diagram and talk about co-products. Then, the knowledge I have from yesterday, and the knowledge I have from a few lectures back (that you can flip arrows) will be composed to produce new knowledge.
Compared to haskell, category theory is free of practical limitations, and you work with graphical models, not code.
Both of these are advantages, IMO.
Also, CT is quite beautiful in a way I can't describe.