[HN Gopher] From Sets to Categories (2023)
___________________________________________________________________
From Sets to Categories (2023)
Author : boris_m
Score : 57 points
Date : 2024-08-12 09:01 UTC (2 days ago)
(HTM) web link (abuseofnotation.github.io)
(TXT) w3m dump (abuseofnotation.github.io)
| sesm wrote:
| Is there any Category Theory tutorial that illustates that we
| need this apparatus to solve some real problem? For example, for
| Group Theory there is an excellent book 'Abel's theorem in
| problems and solutions' that does exactly that.
| gremgoth wrote:
| Modern algebraic topology, especially homological algebra, more
| or less requires category theory... intro textbooks such as
| Rotman's will contain primers on category theory for this
| reason.
| sesm wrote:
| That sounds good, but what's the easiest to state
| mathematical problem that requires Category Theory apparatus
| for the solution?
| gremgoth wrote:
| Putting topology aside, and recognizing that 'ease' is
| subjective, imo Moggi's use of monads to model the
| denotational semantics of I/O in lazy functional languages
| such as Haskell is a common textbook example; the creators
| of Haskell had tried many solutions that did not work in
| practice before monads cracked it open. Even now this
| solution is more widely adopted than the alternatives
| (streaming I/O, linear I/O types, etc) and Moggi's paper
| remains a classic.
| will-burner wrote:
| I'd say Grothendieck's proofs of the Weil Conjectures is a
| good example. His proof uses etale cohomology and the
| definition of etale cohomoly uses Category Theory in a
| fundamental way. From the etale cohomoly wikipedia page
| https://en.wikipedia.org/wiki/%C3%89tale_cohomology
|
| "For any scheme X the category Et(X) is the category of all
| etale morphisms from a scheme to X. It is an analogue of
| the category of open subsets of a topological space, and
| its objects can be thought of informally as "etale open
| subsets" of X. The intersection of two open sets of a
| topological space corresponds to the pullback of two etale
| maps to X. There is a rather minor set-theoretical problem
| here, since Et(X) is a "large" category: its objects do not
| form a set."
|
| There's a lot of advanced math in that paragraph, but it
| should be clear that Category Theory is needed to define
| etale cohomology.
| sesm wrote:
| Thanks again! It will take some time for me to digest,
| but at least now I know in which direction to look.
| isotypic wrote:
| One application I like is the use of the Seifert-van Kampen
| theorem to prove that the fundamental group of the circle
| (S^1) is isomorphic to Z. While category theory is not
| strictly needed to prove this (you can compute pi_1(S^1)
| using R as a cover in a way that is purely topological, see
| Hatcher "Algebraic Topology"), if one states the Seifert-
| van Kampen theorem for groupoids (this uses category theory
| through the notion of a universal property/pushout) one can
| compute pi_1(S^1) largely algebraically just from the
| universal property - in fact you can go through the whole
| proof without mentioning a homotopy once (see tom Dieck
| "Algebraic Topology" section 2.7).
|
| This might not meet your criterion exactly, as one can
| extract a more topological proof and relegate the category
| theory to a non-essential role, but this requires some more
| effort and is a harder proof. So I do think it still
| illustrates that the category theoretic approach does add
| something beyond just a common language.
| sesm wrote:
| As far as I understand, fundamental groups were defined
| by Poincare in 1895. And functors in category theory are
| a generalisation of this idea (i.e. proving something for
| fundamental groups and then relating this back to
| topological spaces). So your example sounds backwards to
| me.
| manvillej wrote:
| functional programming seems to rely on it.
| https://en.wikipedia.org/wiki/Category_theory
| will-burner wrote:
| It's annoying that you need so much math to understand the
| utility of Category Theory. I learned a bunch of Category
| Theory before I ever saw it used in a useful way.
|
| Grothendieck wrote modern Algebraic Geometry in the language of
| Category Theory. This is the first time I saw Category Theory
| really used in a useful way. Grothendieck's proofs of the Weil
| conjectures I would say is a good example of using Category
| Theory to solve a famous problem. Category Theory is used to
| define and work with etale cohomology and etale cohomology
| plays a fundamental role in Grothendieck's proofs of the Weil
| conjectures.
|
| https://en.wikipedia.org/wiki/Weil_conjectures
| sesm wrote:
| Thanks, this looks very interesting!
| hughesjj wrote:
| Tragically (for pure mathematicians), there are some real world
| use cases.
|
| Last years SoME3 has this entrant
| https://youtu.be/Njx2ed8RGis?si=-Q0TwT8LKmTC9o0R
|
| Also Oliver lugg has a hilarious overview of the topic
|
| https://youtu.be/yAi3XWCBkDo?si=b5MFcnfMrYyrv_Xd
| red_trumpet wrote:
| > Last years SoME3 has this entrant
| https://youtu.be/Njx2ed8RGis?si=-Q0TwT8LKmTC9o0R
|
| That's not an application of category theory. The important
| theorem here is that the fundamental group is a functor, plus
| computations of the fundamental group of the disc and the
| circle. But that's a theorem from topology, not a theorem
| from category theory. Category theory is merely used as a
| language, to give the proof a structure.
|
| By that I don't want to say category theory is useless. But
| regarding the video it's neither necessary, nor an
| application of category theory.
| Nesco wrote:
| > "There real use-cases"
|
| > Proceed to link to a non-constructive proof
|
| Why are mathematicians like this?
| nihzm wrote:
| Although not explicitly stated this application [1] of codesign
| for engineerring problems is actually built using category
| theory
|
| [1]: https://arxiv.org/abs/1512.08055
| GrantMoyer wrote:
| I found the series of Category Theory lectures by Bartosz
| Milewski[1] extremely helpful and approachable. It indroduces
| the abstract concepts of category theory while giving concrete
| examples of those concepts and tying some key concepts back to
| properties of types in programming languages.
|
| [1]:
| https://www.youtube.com/playlist?list=PLbgaMIhjbmEnaH_LTkxLI...
| js8 wrote:
| > that illustates that we need this apparatus to solve some
| real problem?
|
| I think your question is wrong in a sense. Category theory is
| one of several languagues of mathematics, and there are
| analogies between them. It's kinda like asking "is there a
| computer program that requires to be written in C?"
|
| So I think there is an element of taste whether you prefer
| category theory to some other (logical) language. That being
| said, just like in programming, it's still useful to know more
| than one language, because they potentially have different
| strengths.
| mrkeen wrote:
| I haven't dug far into CT. I'm slowly making my way through
| Modern Foundations of Mathematics (Richard Southwell) [1] that
| was posted here recently.
|
| That said, two comments:
|
| 1) The definition of a category is just objects, arrows, and
| composition. If you're looking for _more_ features, you might
| be disappointed. (If you 've grown up with 'methods' rather
| than arrows, then you don't necessarily have composition.)
|
| Writing your logic with objects and arrows is just damn
| pleasant. If I have bytes, and an arrow from bytes to JSON,
| then I have JSON. If I have also have an arrow from JSON to a
| particular entry in the JSON, then by the property of
| composition, I have an arrow from bytes to that entry in the
| JSON.
|
| 2) The various CT structures are re-used over and over and over
| again, in wildly different contexts. I just read about 'logict'
| on another post. If you follow the link [2] and look under the
| 'Instances' heading, you can see it implements the usual CT
| suspects: Functor, Applicative, Monad, Monoid, etc. So I
| already know how to drive this unfamiliar technology. A few
| days ago I read about 'Omega' on yet another post - same deal
| [3]. What else? Parsers [4], Streaming IO [5], Generators in
| property-based-testing [6], Effect systems [7] (yet another
| thing I saw just the other day on another post), ACID-
| transactions [8] (if in-memory transactions can count as
| 'Durable'. You don't get stale reads in any case).
|
| They're also widespread in other languages: Famously LINQ in
| C#. Java 8 Streams, Optionals, CompletableFutures,
| RX/Observables. However these are more monad-like or monad-
| inspired rather than literally implementing the Monad
| interface. So you still understand them and know how to drive
| them even if you don't know all the implementation details.
|
| However what's lacking (compared to Haskell) is the _library
| code targeting monads_. For example, I am always lacking
| something in Java Futures which should be right there: an arrow
| I can use to get from List <Future<T>> to Future<List<T>>. In
| Haskell that code ('sequence') would belong to List (in this
| case 'Traversable' [9]), not Future, as it can target any
| Monad. This saves on an n*m implementation problem: i.e. List
| and logict don't need to know about each other, vector and
| Omega don't need to know about each other, etc.
| [1] https://www.youtube.com/playlist?list=PLCTMeyjMKRkqTM2-9HXH
| 81tvpdROs-nz3 [2] https://hackage.haskell.org/package/log
| ict-0.8.1.0/docs/Control-Monad-Logic.html#g:2 [3]
| https://hackage.haskell.org/package/control-monad-
| omega-0.3.2/docs/Control-Monad-Omega.html [4]
| https://hackage.haskell.org/package/parsec-3.1.17.0/docs/Text-
| Parsec.html#t:ParsecT [5]
| https://hackage.haskell.org/package/conduit-1.3.5/docs/Data-
| Conduit.html#g:1 [6] https://hackage.haskell.org/package/
| QuickCheck-2.15.0.1/docs/Test-QuickCheck-Gen.html#g:1 [7]
| https://hackage.haskell.org/package/bluefin-0.0.6.1/docs/Bluefi
| n-Eff.html#g:1 [8]
| https://hackage.haskell.org/package/stm-2.5.3.1/docs/Control-
| Monad-STM.html [9]
| https://hackage.haskell.org/package/base-4.20.0.1/docs/Data-
| Traversable.html#t:Traversable
| neonsunset wrote:
| Perhaps not in Java but in C# it is quite common to do
| var tasks = names.Select(GetThingAsync); //
| IEnumerable<Task<Thing>> var things =
| Task.WhenAll(tasks); // Task<Thing[]>, await to get
| Thing[]
|
| Can mix and match with other LINQ methods. There are other
| useful methods like Parallel.ForEachAsync, .AsParallel (Java
| has a similar abstraction) and IAsyncEnumerable for
| asynchronously "streaming back" a sequence of results which
| let you compose the tasks in an easy way.
| Squeeeez wrote:
| Maybe what you wrote is clear to other LINQ users, but as a
| short feedback, your point is not easily understandable for
| people who don't know much about it.
|
| As in, from outside, it looks like you are in there way
| deep, but it might need some more work to go and fetch the
| (assumed) target audience.
| kidintech wrote:
| Why does every category theory primer use this exact formulation:
| (.*) is just an [arrow|object] in the category of (.*)`
|
| Every undergrad course, office hour, research paper, and manual
| that I've ever seen spams it.
| GrantMoyer wrote:
| As I understand it, it's a bit of an inside joke to minimize
| the complexity of mathematical structure. It's frequent use is
| along the same lines as the frequent use of "* Considered
| Harmful" in CS.
| cryptonector wrote:
| Because arrows are functions/mappings, and everything we do in
| programming involves arrows, even in languages where arrows
| aren't used as notation.
|
| The common formulation is that a "monad is just a monoid in the
| category of endofunctors", which is not saying much but with
| big words, and the joke lies in understanding what it's saying.
| Bartosz Milewski has a lecture video series on youtube that's
| all about explaining that joke, and I highly recommend it
| because it's actually a wonderful CS lecture series.
| xelxebar wrote:
| It has struck me for a while that associativity can be seen as a
| higher-order commutativity. Specifically, for the real numbers,
| it's associativity just says that you can commute the order in
| which you evaluate the multiplication map.
|
| To make that more explicit, consider the space of left-
| multiplication maps Lr(x) = rx for real numbers r and x.
| Similarly, for right-multiplication maps Rr(x) = xr. Then the
| associative rule a(xc) = (ax)c can be re-written La[?]Rc(x) =
| Rc[?]La(x), which is precisely a commutativity relation.
|
| The above obviously generalizes to arbitrary Abelian groups, but
| I'm curious if there's more depth to this idea of associativity
| as "higher-order commutativity" than just what I've said here.
| 082349872349872 wrote:
| See also https://www.cs.utexas.edu/~EWD/ewd11xx/EWD1142.PDF
| (which ties in distributivity)
| khazhoux wrote:
| I spent many hours many years ago studying CT and I was left very
| frustrated. Endless definitions without any meaningful results or
| insights. My (admittedly cartoonish) takeaway from Category
| Theory was: " _We can think of all math as consisting of things
| and relationships between things_! "
|
| Like, ok?
|
| It seems to appeal to computer science folks who want to level up
| their math chops, enjoy an exclusive "boutique" branch, and long
| for grand unification schemes. But IMHO it simply doesn't
| deliver. It's a whole lotta talk to say nothing.
|
| I always compare with abstract algebra, where you start with a
| basic definition of groups and within a few pages you reach
| Lagrange's Theorem and now you understand something amazing about
| primes and sets, and you can keep squeezing and twisting the
| basic definitions for ever-more complex and brain-punishing
| results.
| TwentyPosts wrote:
| How much of a background do your have in abstract algebra? I
| don't think category theory makes much sense or is very
| satisfying unless you can already list a bunch of categories
| you interact with regularly, and have results which can be
| expressed in terms of categories.
| khazhoux wrote:
| I'm fairly well-versed in AA, linear alg, topology, a few
| others. I got zero satisfaction from CT.
|
| What would be the first interesting (if even mildly
| insightful) result in CT? I'll pull out my books and take a
| look...
| cryptonector wrote:
| See my other reply. It makes some things way easier in
| real-world programs (and libraries).
| cryptonector wrote:
| It's just a lot of words for saying that you use [fill in the
| blank with your language of choice's words, like classes or
| interfaces] to wrap your classes with such that the wrappers
| provide methods that let you do a variety of things:
| - associate immutable contextual stuff with your data
| (think configuration, in C you'd add a context object
| pointer argument to all your functions, but in Haskell
| you'd just wrap your objects in monads) - associate
| "mutable" contextual stuff with your data (think state,
| in C you'd add a context...) - abstract out I/O so you
| can write fully deterministic code that's easy to test
| - etc. (e.g., tracing, logging, transactions,
| backtracking, and whatever else you can imagine)
|
| along with standard methods that allow you to chain
| "statements" into a single expression while still looking like
| it's "statements".
| layer8 wrote:
| You don't need category theory to understand how type-
| structure-preserving wrappers work in software development,
| and people invented them without knowing about category
| theory.
| Chinjut wrote:
| Categories are very similar to groups. If you can see how
| groups come up often and so it can be useful to think about the
| concept of groups, it's exactly the same thing with categories.
|
| A group models the invertible maps from one structure to
| itself. A groupoid models the invertible maps between a number
| of structures. A monoid models the maps from one structure to
| itself (without presuming invertibility). A category models the
| maps between a number of structures (without presuming
| invertibility).
| khazhoux wrote:
| Again though, where are the derived results? I found very
| very few in CT, where other branches are replete. Back to my
| example, abstract algebra has one derived result after
| another.
|
| CT is just... statements. It's "observational." I suppose
| maybe one should simply understand that going in, that there
| are no (or very few) actual results, it's just a set of
| descriptors.
| Chinjut wrote:
| There are many results, but whether you would find them
| interesting is up to you. (I don't even know what it would
| mean for a result to not be a "statement" or "observation".
| Every group-theoretic result is a statement of an
| observation, and for that matter, the Riemann Hypothesis is
| a statement too.)
|
| Since you mention Lagrange's theorem, I presume you are
| looking for introductory results rather than advanced
| results. E.g., the result that a functor has at most one
| left adjoint up to isomorphism (a direct generalization of
| the fact that inverses are unique in groups). Or the result
| that a functor which has a left adjoint automatically
| preserves limits (and the near converse to this given by
| the Adjoint Functor Theorem). Or the theorem that a
| category has a limit for the entire category if and only if
| it has an initial object. Or the Yoneda lemma, which is a
| direct generalization of Cayley's theorem for groups. Or
| Lambek's theorem that every initial algebra is invertible.
|
| What is a group-theoretic result of interest to you, apart
| from the aforementioned Lagrange's theorem? It might in
| particular be good to see a group-theoretic result which
| you find interesting even outside the context of finite
| groups (as there is not such an emphasis on considering
| finiteness in typical category theory, though one could of
| course say things specifically about finite categories
| too).
| grumpyprole wrote:
| You won't get much insight from a study period measured in
| hours. CT has actually been incredibly beneficial for computer
| science. Monads were first used to give denotational semantics
| to imperative languages. CT has also influenced Haskells
| design, giving many general and consistent abstractions across
| it's libraries. Looking ahead, CT is teaching us how to build
| software in total languages.
| xanderlewis wrote:
| Have you tried learning something like algebraic topology, or
| representation theory, or anything that actually _uses_ it (and
| for which it's truly indispensable)?
|
| I think if you do, you'll discover quickly why category theory
| is so nice -- and useful! Its origins aren't in staring at a
| blank sheet of paper and trying to come up with needlessly
| complicated notations and idea; it comes only after centuries
| of observation and gradual pattern recognition.
|
| Conversely: if you don't, I don't think you'll ever get it. At
| least not without much difficulty.
|
| It's a bit like set theory: basically everyone uses it because
| it's such a useful paradigm; hardly anyone studies it for its
| own sake. Those who _do_ can tell you 'theorems' of set theory,
| and those who do the same for category theory can tell you
| 'theorems' of category theory. The rest of us use it as a
| convenient (and mind-expanding) language.
|
| By the way, you shouldn't consider it to be some kind of
| ontological theory (or even foundation) for mathematics. It
| makes no attempt to tell us what there _is_ , or even
| particularly what is true; it gives us a way of simultaneously
| generalising thousands of definitions and facts, allowing us to
| see commonalities between a priori only distantly related
| concepts and therefore further generalisations more easily.
| Xcelerate wrote:
| As a non-mathematician, I'm confused how category theory relates
| back to formal systems. Is it its own formal system, or is it
| built on top of ZFC or type theory? If it's built on top of
| something else, what sort of algorithm would tell me whether the
| DAG that constitutes a proof from a set of axioms to a theorem
| involves category theory or not?
| Chinjut wrote:
| The answers to these questions are exactly the same as for
| group theory or graph theory or linear algebra or any other
| such thing.
___________________________________________________________________
(page generated 2024-08-14 23:01 UTC)