Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Why I am learning category theory

the.scapegoat.dev

Post reply on HN
Print view View original

151–160 of 224 posts

Re: Why I am learning category theory

#151

Post by Twisol »

deltaseventhree wrote: post #62
i_am_toaster wrote: post #21

I would be willing to drink the kool-aid if I saw it being used in a practical way. I always feel these posts are filled with category theory jargon without ever explaining why any of the jargon is relevant or useful. I’ve even watched some applied category theory courses online and have yet to feel I’ve gained anything substantive from them. However, as I started off with, I’m always willing to try something out or…

Knowing category theory helps you better design interfaces. Exactly like the interfaces in OOP. Alot of the generic interfaces you design in OOP end up being useless. Never re-used and pointless. You never needed to make these interfaces in the first place In category theory, you will be able to create and identify interfaces that are universal, general and widely used throughout your code. Category theory allows you…

> you really need to use haskell.

Or Scala. They're the only two common-use languages I'm aware of whose type systems are expressive enough to define what a monad (or a category, or a ...) is internally. Of course you can identify particular monads (or ...) in any language, but you can't talk about them inside most languages.

Re: Why I am learning category theory

#152

Post by Twisol »

zmgsabst wrote: post #27
i_am_toaster wrote: post #21

I would be willing to drink the kool-aid if I saw it being used in a practical way. I always feel these posts are filled with category theory jargon without ever explaining why any of the jargon is relevant or useful. I’ve even watched some applied category theory courses online and have yet to feel I’ve gained anything substantive from them. However, as I started off with, I’m always willing to try something out or…

I think the real insight of category theory is you’re already doing it, eg, whiteboard diagrams. Category theory is the language of diagrams; it studies math from that perspective. However, it turns out that category theory is equivalent to type theory (ie, what computers use). So the reason why diagrams can be reliably used to represent the semantics of type theory expressions is category theory. My workflow of deve…

> However, it turns out that category theory is equivalent to type theory (ie, what computers use).

Just to elaborate on this a little, a program of type B in context of variables of types A1, A2, ..., An, can be modeled as an arrow (A1 * A2 * ... * An) -> B. (More elaborate type theories get, well, more elaborate.) The various ways you might put programs together (e.g. if-expressions, loops, ...) become various ways you can assemble arrows in your category. Sequential composition in a category is the most fundamental, since it describes dataflow from the output side of one program to the input site of another; but the other ways of composing programs together appear as additional structure on the category.

Categories take "semicolon" as the most primitive notion, and that's all a category really is. In fact, if you've heard monads called "the programmable semicolon", it's because any monad induces a related category whose effectful programs `a ~> b` are really pure programs `a -> m b`, where `m` is the monad.

Re: Why I am learning category theory

#153

Post by Twisol »

kevinventullo wrote: post #109

This crowd may not want to hear this, but as a former mathematician, the DS/Algorithms knowledge I gleaned from Leetcode grinding has been far more useful in my day-to-day work than any of the category theory I once used on a regular basis.

I think learning the essentials of another field can be more valuable than expected, whether it's a mathematician learning to program or a software engineer learning patterns of abstraction. When you've gone deep on one field, going even deeper has diminishing returns.

Software engineers and (non-categorical) mathematicians are both forced to deal with patterns of abstraction on a regular basis, so they naturally pick up a lot of what category theory concerns itself with. This can make category theory sound like quite a lot of words for very little gain. But I do think that formalizing one's intuition -- taking something understood implicitly and giving it explicit form -- can be a useful tool in its own right.

Most of the material out there on category theory attempts to formalize the algebraist's intuition. Software engineers then have to learn algebra just to learn category theory. I don't think that's essential to category theory, and I think we're starting to see more and more "elementary" category theory that doesn't take some other whole edifice as given. The fact that so many software engineers exist who do find value in a categorical perspective (it's more than you'd expect!) suggests that we'll get there eventually.

Re: Why I am learning category theory

#154

Post by btilly »

Tainnor wrote: post #126
School-Cotton wrote: post #14

Earlier quoted context omitted.

> 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.

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."

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

#155

Post by Twisol »

codekilla wrote: post #33
mark_l_watson wrote: post #17

Cool, I am also spending a little time on this. I bought a CT book by Emily Riehl but I am finding it rough going. I find her YouTube talks and lectures to be easier to follow.

Try Eugenia Chang’s new book, The Joy of Abstraction . Riehl’s book is very technical.

I second this recommendation; Cheng's book is probably the most approachable of the recent wave of category theory texts which does not assume the whole edifice of abstract algebra as a starting point.

Most CT texts introduce categories around page 1, and the Yoneda lemma a handful of pages in. Cheng's book builds up intuitions until chapter 8, where categories are defined over the course of several pages, and supposedly (I'm not there yet) ends the book with the Yoneda lemma.

You might think this means the book is mostly fluff. First: if you read it and think that, you're probably a more advanced reader than she's targeting. Second: goodness no, it's packed to the brim with categorical intuitions; there's a whole way of thinking that she's trying to motivate. Categories are just a formalization of this way of thinking; if you're not onboard with the thinking, the formalization is going to be hollow to you no matter what.

Do recommend.

Re: Why I am learning category theory

#156

Post by SleekEagle »

Tainnor wrote: post #7

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 al…

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

#157

Post by Twisol »

chowells wrote: post #87

> 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 should be pardoned for their phrasing; but I find yours more enlightening.

Re: Why I am learning category theory

#158

Post by SleekEagle »

Tainnor wrote: post #121
larve wrote: post #9

Earlier quoted context omitted.

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 theo…

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

#159

Post by Twisol »

yodsanklai wrote: post #64

Reading at the comments, people confuse concepts like monoids and functors with category theory.

"Functor" has been used in multiple ways in different fields. It's apparently a term of art in linguistics; we call C++ classes implementing `operator()` "functors"; Prolog terms have parts called "functors" (apparently imported from linguistics); and of course category theory has them.

As far as mathematics is generally concerned, I think the category theory concept is the origin. Monoids, on the other hand, did exist before category theory; the modern conception as one-object categories is nice, but it's definitely an import.

Re: Why I am learning category theory

#160

Post by larve »

Twisol wrote: post #151
deltaseventhree wrote: post #62

Earlier quoted context omitted.

Knowing category theory helps you better design interfaces. Exactly like the interfaces in OOP. Alot of the generic interfaces you design in OOP end up being useless. Never re-used and pointless. You never needed to make these interfaces in the first place In category theory, you will be able to create and identify interfaces that are universal, general and widely used throughout your code. Category theory allows you…

> you really need to use haskell. Or Scala. They're the only two common-use languages I'm aware of whose type systems are expressive enough to define what a monad (or a category, or a ...) is internally. Of course you can identify particular monads (or ...) in any language, but you can't talk about them inside most languages.

C++ fits the bill as well (!)

I wager that you can get pretty far with compile-time macros, even as rudimentary as C's, to encoder a fair bit of generic monad machinery.

Post reply on HN