Live data from Hacker News

Category Theory Illustrated – Natural Transformations

abuseofnotation.github.io

81–86 of 86 posts

Re: Category Theory Illustrated – Natural Transformations

#81

Earlier quoted context omitted.

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

Thanks, that sharpens it then to a question about natural numbers, or at least some idea of an indefinitely extensible collection of unique elements: it seems the ordering on the numbers isn't required for a collection of variables, we just need them to be distinct.

I don't think you need set theory to define set theory (someone would have noticed that kind of circularity), but there still seems to be some sleight of hand in the usual presentations, with authors often saying in the definition of first-order logic prior to defining set theory that "there is an infinite set of variables". Then they define a membership relation, an empty set, and then "construct the natural numbers"... But I guess that's just a sloppiness or different concern in the particular presentation, and the seeming circularity is eliminable.

Maybe instead of saying at the outset that we require natural numbers, wouldn't it be enough to give an operation or algorithm which can be repeated indefinitely many times to give new symbols? This is effectively what you're illustrating with the x, x*, x**, etc.

If that's all we need then it seems perfectly clear, but this kind of operational or algorithmic aspect of the foundation of logic and mathematics isn't usually acknowledged, or at least the usual presentation don't put it in this way, so I'm wondering if there's some inadequacy or incompleteness about it.*

Re: Category Theory Illustrated – Natural Transformations

#82
post #80

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.

Then why link to the middle of the whole thing, instead of the beginning?

Re: Category Theory Illustrated – Natural Transformations

#83
post #70
post #54

Earlier quoted context omitted.

But what's the utility of this definition? Does it help solve or prove something?

It helps you build an intuition for categories, if you're used to graphs :) If you have a working intuition for categories then in most cases the specific formulation you choose as a foundation doesn't matter, just as most mathematicians work nominally in set theory without worrying about the subtleties of ZFC.

IMO the right intuition about a tool comes from applying it in the context where it provides a real leverage. In case of Category Theory that would be advanced algebraic topology (not re-phrasing basic things which are easier to understand without CT).

Re: Category Theory Illustrated – Natural Transformations

#85
post #58
post #41

Earlier quoted context omitted.

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…

Good point, algebraic topology is mostly concerned with Top -> Grp functors to prove the properties of continuous transformation, while Haskel community focuses on Hask -> Hask endofunctors to use fancy names for mundane things.

And yet the categorical concepts in Hask are undoubtedly practically useful, more so than an arbitrary sample of concepts, and compose extraordinarily well. Does that have nothing to do with those concepts deriving from (even more general concepts of) category theory?

Re: Category Theory Illustrated – Natural Transformations

#86
post #83
post #70

Earlier quoted context omitted.

It helps you build an intuition for categories, if you're used to graphs :) If you have a working intuition for categories then in most cases the specific formulation you choose as a foundation doesn't matter, just as most mathematicians work nominally in set theory without worrying about the subtleties of ZFC.

IMO the right intuition about a tool comes from applying it in the context where it provides a real leverage. In case of Category Theory that would be advanced algebraic topology (not re-phrasing basic things which are easier to understand without CT).

Rephrasing things is useful when it allows you to draw equivalences with other things that might have results or insights that translate across, which is something a lot of people use CT for. As with most maths the payoffs aren't always immediate, though, which leads to a lot of frustration with from programmers who expect immediate results from their insights.

From a programming perspective, though, a fair few important things have (by now) turned out to be useful that have come as a result of rephrasing programming in mathematical terms. Some top contenders are monads (directly from CT — think Haskell, but also LINQ, JavaScript Thenables, async/await, Rust Option/Result combinators, parser combinators), proof assistants and modern approaches to type systems, linear/substructural logic (think Rust or C++ move semantics), functional programming (which is now embraced at least to some extent by all mainstream programming languages), functional reactive programming (the core ideas behind things like React), et cetera.

Post reply on HN