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

Category Theory Illustrated – Natural Transformations

abuseofnotation.github.io

Post reply on HN
Print view View original

71–80 of 86 posts

Re: Category Theory Illustrated – Natural Transformations

#71

Post by chermi »

hamburgererror wrote: post #8

What's the thing with category theory? I see this topic discussed quite frequently here but I don't get it why people are so into it

Pinging the https://planting.space/ people! I know some of them are on HN, at least recruiting in the past. I haven't updated my knowledge in a while, but my impression of the company was basically that they were going make money using category theory(+all math) in clever and useful ways. I think they turned toward AI a little, but they're at the root a bunch of people who think category theory is useful. Hence, the ping!

Re: Category Theory Illustrated – Natural Transformations

#72

Post by Twey »

ctenb wrote: post #41
Twey wrote: post #30

Earlier quoted context omitted.

Insofar as ‘computation’ is about mapping one state or value to another state or value, it has a lot to do with CT! The question of whether CT is _useful_ for studying computation is different, and there are certainly other lenses you can see computation through that some people would argue are better. But it's hard to deny that they're _related_.

I mean, technically almost all of math can be related to other math one way or another. To say the CT has a lot to do with computation is definitely a stretch. CT is not a recognized Computer Science subject. It's mostly used in the functional programming community to name certain concepts and theorems, but then applied to a specific type system (so it's not actually doing CT, since your restricting yourself to a sin…

> To say the CT has a lot to do with computation is definitely a stretch.

I think the argument I presented above adequately justifies CT as fundamentally connected to computation, at least as we study it today, though I think there are other formalisms as well that are just as worthy.

> CT is not a recognized Computer Science subject

I'm not sure who decides this :) Certainly when I studied computer science we had modules on category theory, along with other applicable ‘discrete math’ subjects.

CS is a bit of a grab-bag of a discipline, so it's very hard to say what does or doesn't belong on a CS curriculum. But I think programming language semantics, which is the field where you see CT pop up the most, is probably uncontroversially CS, or at least I don't know what other discipline would claim it.

> It's mostly used in the functional programming community to name certain concepts and theorems

It's mostly used in the PL community; its use in functional programming is an attempt to connect the language more directly to that lineage (or because functional programming languages traditionally came from that community, where the language is already understood and available to describe things).

> but then applied to a specific type system (so it's not actually doing CT, since your restricting yourself to a single category, whereas CT is really about connecting different categories by generalizing over them)

I agree that there's not a lot of interesting category theory to do when restricted to a single category, but this isn't quite correct. Some type systems, e.g. simply typed lambda calculus, are adequately _described_ by a single category, though in more advanced cases you usually need more than one (e.g. dependently typed languages are often described by ‘categories with families’, which are a slightly more sophisticated category-theoretical construction). But even within a single type system you usually find many categories; for example a type system can often be described by a category of terms that map between its typing contexts, but within that category you also have a category of types and functions between them, a category of (functorial) type constructors and natural transformations, et cetera. An important family of examples are the Kleisli categories over monads: every monad actually defines a category of its own, whose categorical laws give the good behaviour of monads that make them useful for composing effectful computations. Interactions between these different categories are where inspiration comes from for CT-flavoured API design, e.g. the ‘interpreter’ pattern that's popular in Haskell (https://softwareengineering.stackexchange.com/questions/2427...). Even in pure CT the study of ‘connecting different categories’ can be seen mostly as taking a sufficiently close look at the category `Cat` of categories and functors!

Re: Category Theory Illustrated – Natural Transformations

#73

Post by senderista »

tikhonj wrote: post #69
hamburgererror wrote: post #8

What's the thing with category theory? I see this topic discussed quite frequently here but I don't get it why people are so into it

Category theory gives us a nice, high-level set of conceptual tools to try to understand and generalize over things that are hard to connect otherwise. Some people find that useful directly, other people just enjoy it for its own sake, or even for aesthetic reasons. (I think all three are totally reasonable!) At the same time, it's actually rather more accessible than most other areas of pure math—at least at the lev…

> You can reasonably learn about categories, functors, natural transformations and so on without needing a graduate degree's worth of math courses first.

This is the whole premise of _Conceptual Mathematics_: category theory for high school students.

Re: Category Theory Illustrated – Natural Transformations

#74

Post by Twey »

stared wrote: post #38
Twey wrote: post #33

Earlier quoted context omitted.

Category theory is popular in computer science because, at a fundamental level, they're very compatible ways of seeing the world. In computing, we think about: - a set of states - with transformations between them - including a ‘do nothing’ transformation - that can be composed associatively (a sequence of statements `{a; b;}; c` transforms the state in the same way as a sequence of statements `a; {b; c;}`) - but onl…

Still, what's in your opinion, the advantage of thinking in category theory rather than set theory? (For programming, not - algebraic geometry.) I mean, all examples I heard can be directly treated with groups, monoids, and regular functions. I know some abstract concepts that can be defined in a nice way with CT but not nearly as easy - set theory, e.g. (abstract) tensor product. Yet, for other concepts, including q…

In my opinion, the important advantage of category theory over set theory in (some!) computational contexts is that it allows you to generalize more easily. Generalizing from sets and functions to objects and morphisms lets you play around with instantiating those objects and morphisms with a variety of different beasts while maintaining the structure you've built up on top of them, and you can even use it to modularly build towers of functionality by layering one abstraction on top of another, even if you choose later to instantiate one of those layers with good old sets and functions. By contrast, it's hard to imagine treating something like async functions with plain old set theory: while there is of course a way to do it, you'd have to reason about several different layers of abstraction together to get all the way down to sets in one step.

Re: Category Theory Illustrated – Natural Transformations

#78

Post by griffzhowl »

rck wrote: post #65
griffzhowl wrote: post #61

Earlier quoted context omitted.

One way I've seen it presented is that the early Greek philosophers were grappling with how to reconcile two basic facts: somethings stay the same (constancy or regularity), and some things change. Heraclitus was before Parmenides and said that everything changes. Parmenides said that nothing changes, and then the atomists, most prominently Democritus, synthesised these two points of view by saying that there are ato…

I'm not sure what motivated Parmenides because he was more of a poet than anything - it just happened that his poetry was what we would now recognize as incredibly philosophical. He didn't really argue, he just wrote down what the "goddess" told him. But I think the basic problem is that everyone back then agreed that you can't get "something from nothing," and it sure seems like change requires being to come from no…

Ah, I was only thinking of Plato's theory of forms, not Aristotle's, but it makes sense it would be more about something taking on a form in Aristotle, since he was much more concerned with biology than Plato, whose forms are more timeless.

Thanks for the Parmenides poem. It seems much more straightforward than the various commentaries and analyses I've seen written about it.

VIII.16: ἔστιν ἢ οὐκ ἔστιν· :: It is or it is not

Very nearly "to be or not to be"...

Re: Category Theory Illustrated – Natural Transformations

#79

Post by housecarpenter »

griffzhowl wrote: post #49
tristramb wrote: post #17

Earlier quoted context omitted.

Category theory is what you get when you take mappings instead of sets as the primitive objects of your universe. At first this might seem a perverse thing to do as mappings seem more complex than sets, but that is just because traditionally mappings have usually been defined in terms of sets. In set theory you can specify that two sets be equal and you can also specify that one set be an element of another. In categ…

> Category theory is what you get when you take mappings instead of sets as the primitive objects of your universe. I'm not sure about that, because you still need some concept of set (or collection or class) to define a category, because you need a set of objects and mappings between them (technically that's a "small" category, but to define any larger category would require at least as much set-theoretical complica…

Defining first-order logic doesn't really require set theory, but it does require some conception of natural numbers. Instead of saying there's an infinite set of variables, you can have a single symbol x and a mark *, and then you can say a variable is any string consisting of x followed by any number of marks. You can do the same thing with constants, relation symbols and function symbols. This does mean there can only be countably many of each type of symbol but for foundational purposes that's fine since each proof will only mention finitely many variables.

Allowing uncountably many symbols can be more convenient when you apply logic in other ways, e.g. when doing model theory, but from a foundational perspective when you're doing stuff like that you're not using the "base" logic but rather using the formalized version of logic that you can define within the set theory that you defined using the base logic.

Re: Category Theory Illustrated – Natural Transformations

#80

Post by mrkeen »

anal_reactor wrote: post #45

I hate this particular mix of prose and formalism. Too complicated to be pop-sci, too informal to be, well, formal. I got to this part: > We know that two orders are isomorphic if there are two functors, such that going from one to the other and back again leads you to the same object. And I have no clue what is a functor, nor order. "Functor" wasn't defined, and "order" is defined as "thin category", which in turn r…

> And I have no clue what is a functor, nor order.

If you press the Prev button at the top of the page it takes you back to Functors. Twice more and it will take you back to Orders.

Post reply on HN