> Category theory is really the mathematics of abstraction Mathematics is the mathematics of abstraction. That's all you're doing in math, from the beginning to the end. What's the same between "I have two sheep in this pen and five in that one" and "I have two apples in this basket and five in that one"? Hmm, you can abstract out 2+5=7, since it works the same in both contexts. Everything in math is creating and exp…
> Mathematics is the mathematics of abstraction. > Category theory is the mathematics of composition. I don't know why you're being downvoted (tone?) but you're right. Categories formalize exactly and only the notion of composition; its power is that this notion appears everywhere when you know what to look for. Most mathematical abstractions have composition baked in at one level or another, so I think the author sh…
Why I am learning category theory
161–170 of 224 posts
Re: Why I am learning category theory
#162Earlier quoted context omitted.
I mean absolutely no disrespect to anyone doing serious work in CT or in Haskell - and I'm actually very interested in Haskell as a language per se and have been exploring it more in recent months - but having spent some time in Haskell communities, I have to agree. There's a lot of empty posturing by people who don't really seem to understand a lot of mathematics but still seem to have very strong convictions about…
I'm curious why you call out constructivism. I've only really seen constructivism talked about by people who actually have a strong math background. Because it is hard to speak out against, say, the classical notions of existence that say that there are more real numbers than rational ones unless you actually understand why the classical proofs don't work constructively. And not just as, "We don't allow that proof."…
Which I don't mind. If you know your maths, your logic and ideally even your philosophy it's perfectly fine to work in constructivism or even prefer it.
But I've definitely seen some dumb, uninformed hot takes about how maths is just this big conspiracy that doesn't allow dissenting opinions because they've seen some NJ Wildberger video where he shittalks the real numbers.
So it's not even just constructivism per se, more this mix of unprincipled finitism + constructivism + no axiom of choice (or any mixture thereof), as opposed to anything grounded in some rigorous methodology. Basically the "I don't understand set theory or logic but I've heard that Banach Tarski is weird, so mainstream mathematics must be full of shit".
You'd think people wouldn't have hot takes about mathematics, but somehow they do.
Re: Why I am learning category theory
#163Earlier quoted context omitted.
Isn't Redux only used when the app becomes too complex with really complex state?
I think so. Despite being an Elm fan I never used Redux. My side projects or work projects are small so local state and context were more than enough. Although Redux is like Elm, the language (Typescript or ES) make immutability hard so it doesn’t feel as natural a paradigm. Also pragmatically calling setState from an event is just easier for small projects.
Re: Why I am learning category theory
#164Re: Why I am learning category theory
#165Earlier quoted context omitted.
I think so. Despite being an Elm fan I never used Redux. My side projects or work projects are small so local state and context were more than enough. Although Redux is like Elm, the language (Typescript or ES) make immutability hard so it doesn’t feel as natural a paradigm. Also pragmatically calling setState from an event is just easier for small projects.
Why is Elm mentioned specifically. As far as I know (state, action) => state is just a function without side effects?
Having no side effects in JS is easy (just don't do it!) but immutability takes some effort.
React requires immutability so that if it sees the reference to an object again, it knows that it contains the same data. If it promised to work when mutating objects it would continuously need to deep search inside them to see what changed.
In JS, some array operations mutate the array, some copy it, you have to know specifically what operation you are using. In Elm, nothing mutates objects. All built in functions and functions you create will not do this.
In short - you can do (state, action) => state in any programming language, but mistakes caused by mutations are impossible in Elm by design.
Hope that makes sense.
Re: Why I am learning category theory
#166Earlier quoted context omitted.
I'm curious why you call out constructivism. I've only really seen constructivism talked about by people who actually have a strong math background. Because it is hard to speak out against, say, the classical notions of existence that say that there are more real numbers than rational ones unless you actually understand why the classical proofs don't work constructively. And not just as, "We don't allow that proof."…
> I've only really seen constructivism talked about by people who actually have a strong math background. Which I don't mind. If you know your maths, your logic and ideally even your philosophy it's perfectly fine to work in constructivism or even prefer it. But I've definitely seen some dumb, uninformed hot takes about how maths is just this big conspiracy that doesn't allow dissenting opinions because they've seen…
As for the specific complaint, once you have Constructivism, Banach Tarski falls apart (even in versions with the axiom of choice). So if you don't like the weirdness, there is no need to accept it. (But you won't get advanced degrees in math unless you can at least temporarily pretend to accept it. Zorn's lemma is just too widely used.)
But can we agree to both dislike people who argue that 0.999... is not 1?
Re: Why I am learning category theory
#167Earlier quoted context omitted.
It's a common observation that many mathematicians and maths students tend to fall into either the algebraic or the analytic camp, although of course, there are more nuances and some people are genuinely good at both. I myself find beauty in some parts of analysis, but algebra definitely speaks more to me (e.g. I find a proof of Lagrange's Theorem more beautiful than one of the Intermediate Value Theorem). So I can r…
> It's a common observation that many mathematicians and maths students tend to fall into either the algebraic or the analytic camp (we don't talk about the topologists)
Re: Why I am learning category theory
#168Earlier quoted context omitted.
In Ruby and many other languages, you have this idea of a string concatenation: "foo" + "bar" -> "foobar" "foo" + "" -> "foo" That makes it a monoid. Instead of talking about OOP patterns, knowing that the "+" operator is a monoid for string objects lets us write code that is composable. Similarly, with arrays: [:foo,:bar] + [:baz] -> [:foo,:bar,:baz] [:foo,:bar] + [] -> [:foo,:bar] Some language platforms will imple…
Most of us can go our whole careers without the "insight" that string concatenation is a "monoid". I don't know any languages that would balk at "foo" + "" or [a, b].concat([]). This all seems academic beyond belief.
Sorry for the wall of text, but I think to maybe help you understand why people (like me) like to work with it a bit more explicitly, I'll have to make it more concrete and give lots of examples. The good stuff comes at the end.
So let's say you have a list or array type. You want to aggregate all the things inside. Let me write pseudo code from here
let balances = List(1, 4, 23, 7)
let overallBalance = ???
How do you calculate that? Well it's simple - use a for-loop or call .reduce on it or maybe your language even has a builtin sum() function that works for lists of numbers right? let overallBalance = sum(balances)
Now what happens if you want to concatenate strings instead? Can you reuse sum()? Probably not - you will have to hope that your language / std lib has another function for that. Or you have to fall back to implementing it yourself.Not so if monoids are explicitly supported. Because then, it will be exactly(!) the same function (which has been implemented only once) - no type-overloading or anything.
let overallBalance = combineAll(balances)
let concattenated = combineAll(listOfStrings)
Okay, seems a little bit helpful but also doesn't seem super readable, so I guess that's maybe not very convincing. But the reason why I personally love to work with monoids as an explicit concept is the thing that comes next.Let's say you got bitten because you used plain numbers (or even proper money-types) for the balances but in the code at some point you mixed up two things and you added a balance to the users age (or something like that) because you used the wrong variable by accident.
You decide to make Balance an explicit type
class Balance( private innerValue of type number/money )
So the code changes let balances = List(Balance(1), Balance(4), Balance(23), Balance(7))
let overallBalance = sum(balances)
But the second line stops compiling. The std lib sum function doesn't support your custom balance class for obvious reasons. You will have to unwrap the inner values and then wrap them again (both for the sum() method or in your handwritten for-loop).In case you use a duck-typed language where you can just "delegate" the plus-operation to the inner value: congratulations, you are already using monoids without calling it like that. Unfortunately, there is no protection against problems, such as that + might mean different things on different types and they can be used with sum() but cause unexpected results (read: bugs).
In case you use a language that has good supports for monoids, you essentially have to add just one line:
a monoid exists for class Balance using Balance.innerValue
That's it. You can now do let balances = List(Balance(1), Balance(4), Balance(23), Balance(7))
let overallBalance = combineAll(balances)
And, magically, "overallBalance" will be of type Balance and be the aggregated balance.
In case you think that it can't work as easy as that, I'm happy to show you some runnable code in a concrete language that does exactly that. :)On top of that, it does not end here.
Let's take it a step further. Let's say don't only have the account-balances of a single person (that would be the example above). You have that for multiple people.
So essentially, you've got
let listOfBalances = List(
List(Balance(1), Balance(4)),
List(Balance(23), Balance(7)),
List(),
List(Balance(42)
)
And you want to calculate the overall combined balance. Now it gets interesting. Even in a duck-typed language, you can't use sum() anymore, because the inner lists don't support that. You will have to to fall back to a manual two step process, such as sum(listOfBalances.map(balances => sum(balances)))
But with monoids it's different. Since we know how to combine balances in a monoidic way, we also automatically know how to do that for a list that contains balances. In fact, we can do so for any list that contains something that we know of how to combine it. That means, without any other code changes required, you can simply do let overallBalance = combineAll(combineAll(listOfBalances))
This is recursive and goes as far as you want. And it does not only work with lists, but also Maps and other structures. Imagine you have a map with keys that are strings and values that are of any type but constrained to be a monoid. E.g. Map("user1" -> Balance(3), "user2" -> Balance(5)). Or Map("user1" -> List(Balance(2), Balance(3), "user2" -> List(Balance(5))). Or even maps of maps.Now if we have two of those and we know that the values are monoids, we can combine them as well, using again the same function, no matter what is inside. E.g.:
let map1 = Map("user1" -> Balance(3), "user2" -> Balance(4))
let map2 = Map("user2" -> Balance(5), "user3" -> Balance(6))
let aggregated = combine(map1, map2)
And the result will be Map("user1" -> Balance(3), "user2" -> Balance(9), "user3" -> Balance(6))
This is such a powerful concept and makes a lot of things so convenient that I'm always crying when I work in a language that does not support it and I have to handroll all of my aggregations.One note at the end: all of this can be absolutely typesafe in the sense that if you try to call combine/combineAll on something that isn't combinable (= is not a monoid) it will fail to compile and tell you so. This is not theory, I use this every day at work.
Re: Why I am learning category theory
#169Earlier quoted context omitted.
Arguably from a mathematical perspective, the choice of ‘+’ is poor as it implies that the operation is commutative when it’s only associative. Julia used “foo” * “bar” for this reason: https://groups.google.com/g/julia-dev/c/4K6S7tWnuEs/m/RF6x-f...
Then the length() function would be a logarithm...
Re: Why I am learning category theory
#170As I've learned more about category theory (and its applications), I've found string diagrams to be a really nice tool. But string diagrams flip the above around -- morphisms are boxes, and objects are wires. A wire is just a point-to-point link; it doesn't do anything on its own, it just connects a port of one type with a matching port on another site. It's the graphical realization of the composition operation itself.
Meanwhile, morphisms are the things that actually have behavior and real identities, so we draw them as boxes with inputs and outputs and give them names. This lines up with my understanding that in category theory, it's the morphisms that matter; the objects are no more than labels governing how you can stick the morphisms together. You may as well call the morphisms "widgets" or "components", and call the objects "interfaces", because that's literally correct.
This ends up really nice in the context of distributed systems, where concurrency gives you a monoidal category. In string diagrams, concurrently is quite literally the result of putting two diagrams side-by-side, rather than connecting them end-to-end. It's lovely, and some of the research I'm doing right now is actually founded on formalizing the message-passing causal diagrams distsys researchers and practitioners use every day, and using them as a vehicle for building programs that are more amenable to being proven correct. (Distributed systems are hard to verify for both humans and computers; I'd like to think that what I'm doing will be just as good for giving human practitioners a good framework for convincing themselves their code is correct -- or better, making bugs more obvious.)