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

51–60 of 224 posts

Re: Why I am learning category theory

#51

Post by musk_micropenis »

fdupress wrote: post #41
musk_micropenis wrote: post #31

Earlier quoted context omitted.

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.

Strings/lists under concatenation do not form a group since concatenation is not uniquely invertible. (In the sense of "there is no list -xs that you can concatenate onto xs to get the empty list.)

Again, I don't see how this piece of information is useful for a programmer. And if it is, I'll bet it's 10x more useful if expressed in more ordinary language.

Re: Why I am learning category theory

#52

Post by layer8 »

larve wrote: post #43
BenoitP wrote: post #39

Earlier quoted context omitted.

> unlocks something that allows me to think in a broader fashion I believe this is what's at hand here. What is that something? What is that broad fashion? An example would be welcome

It's always hard to point out when some very abstract knowledge has guided your intuition, but I apply monads very often to compose things that go beyond "purely functional immutable data function composition". for example, composing the scheduling of PLC actions so that error handling / restarts can be abstracted away. The more recent insights of learning how to model things with just morphisms are broadening my con…

Morphisms are not a concept that is specific to category theory. Are there any lemmas or theorems of category theory that are useful in software development?

Re: Why I am learning category theory

#53

Post by larve »

musk_micropenis wrote: post #51
fdupress wrote: post #41

Earlier quoted context omitted.

Strings/lists under concatenation do not form a group since concatenation is not uniquely invertible. (In the sense of "there is no list -xs that you can concatenate onto xs to get the empty list.)

Again, I don't see how this piece of information is useful for a programmer. And if it is, I'll bet it's 10x more useful if expressed in more ordinary language.

This is useful for example when implementing compiler optimizations, or concrete string implementations. It means that you can reduce "foo" + "bar" + foo to at least "foobar" + foo and that you can intern "foobar". Would that work the same without calling it a monoid? Of course, monoid is just a name. But that name allows you to go shopping in a wide variety of other fields and work other people have done and mine it for ideas or even concrete implementations.

Re: Why I am learning category theory

#54

Post by hosh »

musk_micropenis wrote: post #31
hosh wrote: post #25

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

For most of my years in primary education, math was easy. Until it was not. I ran headlong into the idea of "instantaneous rate of change", and I was confronted with the existential crises that there is nothing inherently concrete or "real" about the idea of instantaneous rate of change. My mind just got stuck on there, and I nearly failed the course in high school.

Everything after that point was not easy, and somewhere, there was a belief forming that maybe I was not so good at math.

Two things I encountered changed my perspective on that. The first was reading a math graduate student's experience where they talk about struggling with concepts, like groping about in a dark room until one day, you find the light switch and you see it all come together. The other is Kalid Azad's "Math, Better Explained" series. His approach is to introduce the intuition first, before going into the rigor. Between those two, I realized that I had never really learned how to learn math.

Once I started with the intuition, I also realized why people get stuck on things. There are people who don't get negative numbers. They keep looking for something concrete, as if there were something intrinsic to reality that makes negative numbers "real". And there isn't. And yet, in my day-to-day life, I work with negative numbers. I am far better able to reason and navigate the modern world because I grok the intuition of negative numbers.

Then there are the cultures where there isn't even a notion of natural numbers. Their counting system is, "one", "two", and "many". In their day to day life, to echo your sentiment, they can go on their whole life without the "insight" that things can be countable. Many of them probably won't even care that they don't have the intuition of countable things. And yet, in this modern culture, I find myself introducing the idea to my toddler.

Ultimately, it's up to each individual's decision how far they want to go with this. Each culture and civilization has a norm of a minimum set of intuitions in order for that person to navigate that civilization. Category Theory is outside that norm, even among the software engineer subculture. Perhaps one day, it will be the norm, but not today. Beyond that, no one can make you grok a mathematical intuition, as useful as they are once grokked.

Re: Why I am learning category theory

#55

Post by revskill »

nnoitra wrote: post #4

Will it make you a better React dev tho?

Yes. A React Component could be defined as a Functor with contramap function which map props with function.

const renderer = props => Hello {props.pageName}

const Title = ReactComponent(renderer).contramap(props => { pageName: props.title })

Title.fold({ title: 'Home page' }) // Hello Home page

Re: Why I am learning category theory

#56

Post by layer8 »

zozbot234 wrote: post #19
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…

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

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

#57

Post by musk_micropenis »

larve wrote: post #53
musk_micropenis wrote: post #51

Earlier quoted context omitted.

Again, I don't see how this piece of information is useful for a programmer. And if it is, I'll bet it's 10x more useful if expressed in more ordinary language.

This is useful for example when implementing compiler optimizations, or concrete string implementations. It means that you can reduce "foo" + "bar" + foo to at least "foobar" + foo and that you can intern "foobar". Would that work the same without calling it a monoid? Of course, monoid is just a name. But that name allows you to go shopping in a wide variety of other fields and work other people have done and mine it…

A vast, overwhelming majority of programmers will never implement a concrete string type or compiler optimizations. Can you show me how this kind of theory is practical for a working programmer who does things like batch processing jobs, web applications, embedded software, event-driven distributed systems, etc?

Re: Why I am learning category theory

#58

Post by larve »

layer8 wrote: post #52
larve wrote: post #43

Earlier quoted context omitted.

It's always hard to point out when some very abstract knowledge has guided your intuition, but I apply monads very often to compose things that go beyond "purely functional immutable data function composition". for example, composing the scheduling of PLC actions so that error handling / restarts can be abstracted away. The more recent insights of learning how to model things with just morphisms are broadening my con…

Morphisms are not a concept that is specific to category theory. Are there any lemmas or theorems of category theory that are useful in software development?

that's interestingly enough not something I'm interested in (formally deriving things and doing "proper" maths as part of my software work). I care much more about developing new intuitions, and seeing the category theoretical definition of monoid https://en.wikipedia.org/wiki/Monoid_(category_theory) inspired me a lot.

In fact I think that one of the great things about software is that you can not care about being very formal, and you can just bruteforce your way through a lot of things. DO your database calls really compose? or can pgbouncer throw some nonsense in there? Well maybe it breaks the abstraction, but we can just not care and put in a cloudformation alert in there and move on.

Re: Why I am learning category theory

#59

Post by rssoconnor »

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…

Apologies for the jargon, but there isn't room in a comment box for a detailed explanation.

"The Essence of the Iterator Pattern"[0] posed an open problem in type theory as to whether or not "lawful traversals", of type `∀ F:Applicative. (X -> F X) -> (B -> F B)` could appear for anything other than what is called a "finitary container"[1], B := ∃S. X^(P S) where the (P S) is a natural number (or equivalently a polynomial functor B := ∃n. C_n * X^n). Or rather, there was an open question as to what laws are needed so that "lawful traversals" would imply that B is a finitary container.

Eventually I came up with a fairly long proof[2] that the original laws proposed in "The Essence of the Iterator Pattern" were in fact adequate to ensure that B is a finitary container. Mauro Jaskelioff[3] rewrote my proof in the language of category theory to be few lines long: use Yoneda lemma twice and a few other manipulations.

Anyhow, the upshot of reframing this as a simple argument in Category Theory meant that, with the help of James Deikun, I was able go generalize the argument to other types of containers. In particular we were able to device a new kind of "optic"[6] for "Naperian containers" (also known as a representable functors) which are of the form B:=P->X (aka containers with a fixed shape).

Since then people have been able to come up with a whole host of classes of containers, optics for those classes, representations for those optics, and a complete characterization of operations available for those classes of containers, and how to make different container classes transparently composable with each other[4].

For example, we know that finitary containers are characterized by their traversal function (i.e the essence of the iterator pattern). Naperian containers are characterized by their zip function. Unary containers are characterized by a pair of getter and setter functions, something implicitly understood by many programmers. And so on.

I don't know if all this means that people should learn category theory. In fact, I really only know the basics, and I can almost but not quite follow "Doubles for Monoidal Categories"[5]. But now-a-days I have an "optical" view of the containers in, and forming, my data structures, slotting them into various named classes of containers and then knowing exactly what operations are available and how to compose them.

[0]https://www.cs.ox.ac.uk/jeremy.gibbons/publications/iterator...

[1]https://en.wikipedia.org/wiki/Container_(type_theory)

[2]https://github.com/coq-contribs/traversable-fincontainer

[3]https://arxiv.org/abs/1402.1699

[4]https://arxiv.org/abs/2001.07488

[5]https://golem.ph.utexas.edu/category/2019/11/doubles_for_mon...

[6]https://r6research.livejournal.com/28050.html

Re: Why I am learning category theory

#60

Post by larve »

musk_micropenis wrote: post #57
larve wrote: post #53

Earlier quoted context omitted.

This is useful for example when implementing compiler optimizations, or concrete string implementations. It means that you can reduce "foo" + "bar" + foo to at least "foobar" + foo and that you can intern "foobar". Would that work the same without calling it a monoid? Of course, monoid is just a name. But that name allows you to go shopping in a wide variety of other fields and work other people have done and mine it…

A vast, overwhelming majority of programmers will never implement a concrete string type or compiler optimizations. Can you show me how this kind of theory is practical for a working programmer who does things like batch processing jobs, web applications, embedded software, event-driven distributed systems, etc?

my personal favourite: seeing the foldable (a monoid with two types, kind of) in event driven systems means you can model a lot of your embedded software / web applications as a set of functional state/event reducing functions, and build a clean system right from the get go. Seeing the functors in there tells you which part of the state can be split, parallelized or batched for performance or modularity).

Again, these are all very possible without knowing category theory, but category theory studies what the abstractions behind this could be. I find that the huge amount of intuition (driven by some formalism picked up along the way, but even more so by just writing a lot of code) I developed is reflected in what I see in category theory. It's why I genuinely think that web development is just like embedded development: https://the.scapegoat.dev/embedded-programming-is-like-web-d... which seems to be way more controversial than I thought it would be.

Post reply on HN