News for hackers. Stuff that matters.
Re:Why I am learning category theory by Tainnor on Wednesday November 30, 2022 @12:15PM (#33803878)
As someone with a maths degree, yet who admittedly hasn't looked into category theory beyond some basic notions, I still don't quite understand why anyone would want to learn category theory before e.g. abstract algebra or even just fundamental mathematical reasoning (definition, theorem, proof).

Maybe I'm missing something but it seems to me that all you can study monads in programming languages without having to also learn the category theory abstraction of it. The same goes for semigroups, monoids, folds, functors, ...

I'm sure there's a benefit in category theory once you want to unify all these abstractions and talk about all of them together, but I see so many people who think they have to learn CT before they can understand monads in e.g. Haskell, and I don't really understand why.

Re:Why I am learning category theory by umanwizard on Wednesday November 30, 2022 @12:31PM (#33804203)
> As someone with a maths degree, yet who admittedly hasn't looked into category theory beyond some basic notions, I still don't quite understand why anyone would want to learn category theory before e.g. abstract algebra

Because people think “category theory” means “abstract math” in general, due to cargo-culting in and around the Haskell community.

Re:Why I am learning category theory by Karrot_Kream on Wednesday November 30, 2022 @02:48PM (#33806553)
Yeah when I read all of this "category theory expands your mind" thinking, it makes me think that folks were looking for mathematical maturity more than category theory. Work through any good book on algebra and analysis and you'll learn and prove a bunch of stuff about objects and relations.
Re:Why I am learning category theory by bmitc on Wednesday November 30, 2022 @05:22PM (#33808734)
I also have a math background but am now a software engineer, and I agree. One can learn category theory all by itself, but it's relatively unimportant in software and computer science as far as I can tell. It's really only powerful as a unifying, abstraction, and conceptual relating tool in upper mathematics where the divisions of mathematics begin to blur.
Re:Why I am learning category theory by Tainnor on Wednesday November 30, 2022 @05:28PM (#33808825)
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 certain aspects of it (constructivism is another such thing).

Re:Why I am learning category theory by btilly on Wednesday November 30, 2022 @06:55PM (#33809902)
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."

To make that concrete, let's use computable analysis as a foundation for constructivism. In short, we represent Cauchy sequences as computer programs about which we can prove things in our favorite axiom system. You can build up a version of real analysis from that. It is easy to attempt Cantor's diagonal argument. You'll get a concrete program. But it will only represent a real number in our system if our axiom system can prove that every program it proves works, works as proven. This immediately brings up consistency. And so Gödel proves that showing this program represents a computable number in our system would imply our axioms to be inconsistent. (Bad axioms! Bad axioms!) And therefore Cantor's proof fails to produce a number in our system.

Of course classically we would say that if the axioms are consistent, then the program will compute a Cauchy sequence. And so it really does represent a real number even though we couldn't verify it. But whether we accept this alternate argument is a question of philosophy, not logic.

Re:Why I am learning category theory by Tainnor on Wednesday November 30, 2022 @07:36PM (#33810484)
> 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 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 by btilly on Wednesday November 30, 2022 @08:19PM (#33810912)
I'm glad I haven't seen that then. But conversely it does annoy me to see classical mathematicians dogmatically claim as true statements that depend on their philosophy. And that I have seen a lot of.

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 by zozbot234 on Thursday December 01, 2022 @02:31AM (#33813393)
You can account for and "do" classical math perfectly fine as a constructivist+finitist. It just means that any statements about non-constructive existence or non-decidable choice must be phrased as negative statements in the logic; positive disjunction or existentials are reserved for anything that's decidable/constructible.

And uses of the axiom of choice are viewed with suspicion even by many who are doing perfectly classical math, so there's nothing wrong with pointing them out as assumptions ("if we admit of choice being applicable to X, we have Y").

Re:Why I am learning category theory by btilly on Thursday December 01, 2022 @01:01PM (#33819988)
In theory, maybe. In practice you have to work to reconcile the constructive "all functions are continuous" with classical results like "a strictly increasing function can be discontinuous on a dense set." (The two disagree on what a function is.)

As for choice, try doing much functional analysis without Zorn's lemma.

There are parts of math that you can do constructively. But most of it you really can't. And choice is embedded in a lot more math than you'd guess.

Re:Why I am learning category theory by zozbot234 on Saturday December 03, 2022 @12:12AM (#33840828)
> In theory, maybe. In practice you have to work to reconcile the constructive "all functions are continuous" with classical results like "a strictly increasing function can be discontinuous on a dense set." [T]he two disagree on what a function is.

Well yes, it's still a different kind of math. What's not true however is this common notion that a constructivist can only ever view all "classical" math as pure nonsense. In many ways, it ought to be a lot easier for someone committed to constructivist semantics to grok a classical development than the converse - because decision procedures, computations etc. are way more of an afterthought to mainstream mathematicians.

Re:Why I am learning category theory by Tainnor on Sunday December 04, 2022 @03:00PM (#33857227)
That's why for me, constructivism - or in general mathematics with different axioms - are additions to classical mathematics, not replacements. And in that sense, they're fine for me. You'll definitely find people online defending the position that all classical maths is bullshit - I'm not saying that actual researchers behave like that, though.

But I'm also a strict formalist, or more accurately, I think whichever axioms happen to be useful should be used, without much need for there to be a epistemological commitment.

Re:Why I am learning category theory by dwils098 on Wednesday November 30, 2022 @12:41PM (#33804387)
I concur, the theory is not necessary to understand how to use it. Perhaps it is counter-intuitive and one would like hone their intuition. Still there are much better approaches to developing an adequate intuition than the theory, this is why traditional Math textbooks rely on exposition first, to establish the context of the theory...
Re:Why I am learning category theory by larve on Wednesday November 30, 2022 @12:24PM (#33804072)
author here, for context, I do have a reasonable background in maths (algebra, analysis, statistics) at a CS master-ish level (self-taught and a long time ago, though), as well as spent quite some time with programming language / type theory when I was younger, and I do use monads quite a bit in my day to day programming. In fact, the fundamental algebra concepts (rings, groups, etc...) as well as fundamental CS theory (grammars, proof theory, semantics, ...) were the only maths I felt reasonably comfortable with, compared to say, calculus or statistics which really did my head in and ultimately caused me to drop out of university.
Re:Why I am learning category theory by Karrot_Kream on Wednesday November 30, 2022 @02:47PM (#33806535)
How much do you think your predilection for algebra affected your interests? Most folks who do CT as a hobby that I know are much weaker in analytical concepts than any working mathematicians that I knew.
Re:Why I am learning category theory by larve on Wednesday November 30, 2022 @02:50PM (#33806589)
Honestly I'm pretty weak in both, but they seem to reflect my intuitions, if that makes sense? I'm nowhere near a working mathematician, and proofs usually bore me. I prefer writing code.
Re:Why I am learning category theory by Karrot_Kream on Wednesday November 30, 2022 @02:52PM (#33806634)
If you're looking for an alternate perspective, I would suggest taking an advanced undergraduate analysis book and working through it, proofs and all. It'll teach you the same kinds of stuff that you're getting out of CT but will give you "working" (lol) knowledge of how to apply it. A lot of mathematical work is about creating math objects and relations and proving properties of these objects through their relations. The exercises in a good algebra book will exercise this muscle and make your software organization better, at least IMO. Learning the definitions just isn't a substitute.

I can see why categories appeal if you're just looking at definitions, but CT often just abstracts/standardizes an approach that folks were already working with when working with rings, groups, topologies, etc. Going through the proofs will teach you when to apply what.

Aluffi (Algebra: Chapter 0) makes a great book that teaches the basics of CT and brings it up while teaching regular algebra. I highly recommend it.

Re:Why I am learning category theory by larve on Wednesday November 30, 2022 @03:06PM (#33806856)
I studied CS in germany in 1999 and we had "analysis 1+2+3" which I think was a fairly rigorous analysis treatment, I definitely did more than my fair share of proofs. I think that foundation accompanied me through all those years of programming and helped me read and pick up concepts related to type theory, algebra and functional programming.

In parallel I developed this very "visual" way of thinking about structure that makes me really resonate with CT. In a way I'm less interested in learning new maths, more so than learning more about how people approach (complex) structures I already know with these very rudimentary concepts, and seeing how their formalizations match my "folk mathematics".

I'm having a lot of fun!

edit: thanks for the book recommendation! that looks like my kind of maths book

Re:Why I am learning category theory by larve on Wednesday November 30, 2022 @03:20PM (#33807043)
i skimmed through aluffi, and it is indeed exactly the material I had at university in analysis and algebra, augmented with the category theory angle. this is great, thanks a lot. Now I have to find an affordable copy somewhere.

I also like the focus on quotient groups and galois fields, as well as using graphs as recurring examples, which have been the only times I really put the pedal to the maths metal in my programming (for some crypto and error correction stuff).

Re:Why I am learning category theory by bmitc on Wednesday November 30, 2022 @05:18PM (#33808687)
How do you know analysis at a "CS master-ish level" (not sure what that means given it's a mathematical subject) but calculus did your head in? I'm not being judgmental but am just genuinely confused given that analysis is the foundation for calculus. :)
Re:Why I am learning category theory by athrowaway12 on Wednesday November 30, 2022 @05:41PM (#33809011)
Yeah, this is some B.S. here. I have a degree in CS and math. It sounds like parent comment doesn't really know analysis. The exercises in Rudin 1 are way harder than memorizing some rules to evaluate integrals.
Re:Why I am learning category theory by larve on Wednesday November 30, 2022 @05:55PM (#33809198)
That's how I remember it. I know I had to take calculus twice, but passed analysis the first time. To be fair, this is 20+ years ago and my memory sucks at the best of times.

Looking at it now, I think maybe I just found it too boring to remember the tricks, and too tedious to not make mistakes, while I found coming up with proofs more "interesting" and requiring less rote memorization.

Re:Why I am learning category theory by athrowaway12 on Wednesday November 30, 2022 @05:59PM (#33809240)
Ah, for sure pure math is much more enjoyable to learn. I'm glad you find math interesting. Especially as a writer; that's really cool. Sorry for my previous comment.

I wish the university calculus changed the curriculum. I didn't find it particularly useful to learn how to integrate e.g. inverse trig given that WolframAlpha exists. There are lots of other examples of teaching memorization of silly tricks like that. I guess they probably do it because it's easy to test.

Re:Why I am learning category theory by larve on Wednesday November 30, 2022 @06:04PM (#33809285)
No offense taken, I totally understand that it can come across as odd. I hope my clarification makes more sense. Once I learned more about say, why leibniz and newton came up with their formulations, and what say, the inverse of the square root of the determinant of the jacobian actually allows one to formulate (how a space "dilate" when a continuous distortion is applied to it, for example), calculus (applied calculus) became a much more interesting topic for me.

While I only got so far in proving stuff about a cyber-physical I was working on, but this was really fun to learn: https://github.com/LS-Lab/KeYmaeraX-release

See also: http://lfcps.org/lfcps/

Re:Why I am learning category theory by larve on Wednesday November 30, 2022 @05:23PM (#33808753)
Calculus (at least our exams and lecture) were so much about "calculating" and applying rules and clever tricks on complex functions and multiple dimensions which just... didn't work for me. I had a lot of other things going on, so this recollection is probably off. Calculus and diff eqs started making sense to me when I started working in mathematica and systemmodeler, and realizing that it was a brilliant tool. It probably also came from the way it was taught, which was completely devoid of any historical or practical context. It was just a lot of "compute the laplacian of e^i_sin(phi) or whatever.

I found groups, limits, continuity, fields to be much more amenable to my thinking. It felt way more similar to the things I really enjoyed (building software in scheme and C and writing exploits in assembly).

Re:Why I am learning category theory by bmitc on Wednesday November 30, 2022 @05:27PM (#33808817)
Oh, I see. So it seems it was more about the presentation and interest rather than the concepts. You may like Calculus by Michael Spivak if you're interested in it again. It is much more analytical than computational.
Re:Why I am learning category theory by larve on Wednesday November 30, 2022 @05:35PM (#33808927)
That's one of the books I used when I got back into it. These days, there is so much great material on youtube and edx and coursera (plus maths stackexchange and discords) that it's absolutely fantastic to learn maths, as fantastic instructors are immediately available.

For me, I realized thst I need to write the code to accompany the maths, because it helps me disambiguate mathematical notation and put "types" on things.

It helped me a lot to work alongside real maths PhDs and realize that they have a very "intuitive" approach to maths, and don't necessarily yeet lemmas and proofs around all day, instead spending a lot of time brainstorming on the whiteboard and discussing things out, very similarly to software design. It was one of them telling me that my thinking was very mathematical that helped me "deconstruct" the fear of maths that I had built up.

Re:Why I am learning category theory by bmitc on Wednesday November 30, 2022 @06:08PM (#33809326)
I agree that using programming to understand a domain is very useful, as it’s something I’m trying to do a lot of these days. Although sometimes, there needs to be some simplification to do that that maybe skirts around the meat of the matter. But as always, a diverse approach is more powerful than a singular one.
Re:Why I am learning category theory by Tainnor on Wednesday November 30, 2022 @05:19PM (#33808700)
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 relate.

Re:Why I am learning category theory by SleekEagle on Wednesday November 30, 2022 @07:05PM (#33810050)
> 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 by Koshkin on Wednesday November 30, 2022 @08:47PM (#33811178)
Aren’t all topologists algebraic topologists today?
Re:Why I am learning category theory by Karrot_Kream on Thursday December 01, 2022 @06:31PM (#33824601)
No way? It's a pretty even split between analysts and algebraists from what I can tell. Really depends on what you're researching. Only the internet and online CS-adjacent communities have these crazy algebra-dominated communities.
Re:Why I am learning category theory by zozbot234 on Wednesday November 30, 2022 @12:43PM (#33804425)
> or even just fundamental mathematical reasoning (definition, theorem, proof).

Logic and proof theory is actually one of the areas in math where category theory is most clearly useful. Intuitively, this is because reflexivity ("A leads to A") and transitivity ("A leads to B and B leads to C, hence A leads to C") are well-known rules of any kind of proof writing or indeed of argumentation in general, and they exactly describe a category.

Re:Why I am learning category theory by layer8 on Wednesday November 30, 2022 @02:02PM (#33805835)
How exactly is it useful? Reflexivity and transitivity are concepts independent from category theory. How does category theory, specifically, help here?

As someone familiar with algebraic objects and relations etc., I don’t see what category theory is adding in terms of practical usefulness in software development.

Re:Why I am learning category theory by Tainnor on Wednesday November 30, 2022 @05:34PM (#33808910)
I know a fair bit about logic and none of it involves any CT. That's not to say you can't find it in there somewhere as a unifying concept, but the fundamental theorems such as completeness and compactness of FOL, basic model theory, Gödel's theorems, etc. do not require any CT.

Also, reflexivity, transitivity and symmetry just define an equivalence relation, no need for CT there.

Re:Why I am learning category theory by Koshkin on Wednesday November 30, 2022 @05:56PM (#33809211)
Heh, except when you wish to talk about "natural equivalence"!
Re:Why I am learning category theory by nonrandomstring on Wednesday November 30, 2022 @12:54PM (#33804623)
To me it's part of the "stretch your mind" philosophy. Plenty of exercises that add some suppleness and help with all round problem solving. It's one reason I keep up with Lisp even though nobody cares much to learn or pay me to program in it these days. Any programme of discrete and abstract maths surely has the same benefits, with a little bit of different theory areas; number, group, sets, operator... all healthy stuff unless taken to extremes :)
Re:Why I am learning category theory by umanwizard on Wednesday November 30, 2022 @01:16PM (#33805027)
But you can study all of that stuff without category theory.
Re:Why I am learning category theory by larve on Wednesday November 30, 2022 @01:23PM (#33805151)
author here, Finding higher abstractions ultimately is about being able to draw parallels amongst a wider variety of concepts. It doesn't change the concrete thing / the lower levels of abstractions in the least, and it often makes sense to stay at that lower level when communicating or getting things done. Plus I personally enjoy it and I feel it gives me a much wider array of things to draw from when designing / thinking. It broadens my toolbox, even if at the end of the day, all I do is hammer nails.
Re:Why I am learning category theory by chobytes on Wednesday November 30, 2022 @01:26PM (#33805214)
Yeah Im unsure what the point is. The motivation for CT in programming seems weak.

Eg Stuff about types and endofunctors feels like trivial examples using the jargon just to use it. OTOH discovering the Top->Grp functor in algebraic topology is kind of unexpected and revealing.

Re:Why I am learning category theory by rssoconnor on Wednesday November 30, 2022 @03:00PM (#33806744)
I agree with you. CT seems mostly useful as a way of devising entirely new abstractions, but once those abstractions are developed, you don't need CT to use them.

For example if it were 2008 and you want to be inventor Applicative functors for use in Haskell, then knowing lax monoidal functors from CT might be helpful. But if you want to just use Applicative functors, you don't need to learn lax monoidal functors first.

So programmers probably don't need to learn CT because they can just let the computer scientists devise their abstractions for them. But if you want to be a computer scientist and one day devise your own abstractions[0], then maybe CT would be helpful.

[0]https://news.ycombinator.com/item?id=33805923

Re:Why I am learning category theory by q7xvh97o2pDhNrh on Wednesday November 30, 2022 @11:26PM (#33812320)
Do you have any recommended reading for learning CT from the perspective of an engineer who does want to make their own abstractions?

Your description is the single best sales pitch for learning it that I've ever heard. I'm legitimately interested now — in a way that I simply wasn't before your comment.

Everyone else who tries to hype up CT is always like, "Whoa, bro, don't you know that addition is actually a monoid endofunctor over the set of all hyper-reals?" (Or something.) I guess that sort of breathless mathematical revelation is supposed to be so mind-blowing that anyone who hears it gets instantly hooked. My usual response was always just, "So what?"

But you're telling me I can become a better engineer? A meta-engineer, who can engineer things to engineer with? Yeah, I'd definitely be up for that.

Re:Why I am learning category theory by larve on Wednesday November 30, 2022 @11:44PM (#33812441)
(author here) I found the corecursive podcast episode about "portal abstractions" with sam ritchie quite inspiring. It's about monoids from the algebraic point of view, but the mindset is very similar, I think.

https://corecursive.com/050-sam-ritchie-portal-abstractions-...

I think I might have linked it in the article.

Re:Why I am learning category theory by rssoconnor on Thursday December 01, 2022 @09:52AM (#33816953)
My method was to spend 25 years listening to colleagues mumble about Category Theory and slowly picking up the basics. Even I didn't really use Category Theory in my abstraction work. It's just that after months of effort to crack my problem, I showed my pages of work to the Category Theory folks and they were like "oh, it's simply Yoneda this and Yoneda that and your proof can be done in 4 lines.".

That said, if I had to guess at what would be effective at getting up to speed without spending 25 years, would be to checkout https://github.com/hmemcpy/milewski-ctfp-pdf Category Theory for Programmers. Milewski was one of those people who were like "Oh, it's simply Yoneda this and Yoneda that", and he figured it out all himself in parallel without seeing my proof.

But I doubt it will be like, knowing Category Theory will enable you to have super powers for abstraction design. Rather it will be a matter of having enough mathematical tools at your disposal plus the right inspiration at the right time to realize that ones of those tools can happen to solve your abstraction programming problem you happen to be facing at some moment, in a way that is not obvious, if you are lucky. In fact, you likely have to first guess at what the right abstraction is and then fall back on Category Theory to verify the sanity of your guess.

Re:Why I am learning category theory by sargstuff on Saturday December 10, 2022 @12:31AM (#33930190)
Well, will wind up being less tensor than peers to point of being tagged as tuple when you walk in; but still 'All about the blocks' and cache on hand.

Independent of mathematical numerical systems used, everthing gets loaded at hoursX0000. Everything else after that is just bracket arrangements.

If let things stack up, then it's all about what can be accomplished before zeroing out.

https://bartoszmilewski.com/2014/10/28/category-theory-for-p...

https://math.mit.edu/~dspivak/teaching/sp18/7Sketches.pdf

Re:Why I am learning category theory by _448 on Wednesday November 30, 2022 @05:47PM (#33809082)
It is not that one has to learn CT to do FP, but not knowing it makes it difficult to take part in discussions on the mailing lists.
Re:Why I am learning category theory by SleekEagle on Wednesday November 30, 2022 @07:03PM (#33810030)
Yeah, category theory isn't even broadly well studied amongst actual mathematicians lol. I'm all for learning for the sake of learning though!
Re:Why I am learning category theory by sargstuff on Friday December 09, 2022 @11:54PM (#33929999)
It's tagged blocks, not anonymous numerical bits. (think like a schrodingers cat)