[HN Gopher] Applied category theory in chemistry, computing, and...
___________________________________________________________________
Applied category theory in chemistry, computing, and social
networks [pdf]
Author : larve
Score : 76 points
Date : 2022-11-01 16:28 UTC (6 hours ago)
(HTM) web link (www.ams.org)
(TXT) w3m dump (www.ams.org)
| hackandthink wrote:
| "A goal of the ACT community is to bridge the gap between
| theorists using category-theoretic modeling tools and those who
| want to use the models to say something useful and true about the
| world"
|
| This is key. Sure category theoretic abstractions are useful as a
| common language. Lot's of theorems are applicable in many
| domains.
|
| The hard thing is understanding all this stuff and mapping it
| into your domain.
| whatshisface wrote:
| Is it just me, or does "applied category theory" never use
| anything from category theory other than boxes being connected by
| arrows?
| jmt_ wrote:
| I can see why you're saying that, but the use of commutative
| diagrams communicate the structure between the functions and
| objects of interest - it is this perspective which is core idea
| to category theory. So I'd argue that the diagrams are a result
| of communicating a category-theoretic model rather than the
| end-result itself, and therefore have much deeper meaning than
| just "boxes being connected by arrows".
| [deleted]
| abelaer wrote:
| If you're talking about string diagrams, then these are
| actually just 2D notation for very precise category theory.
| Manipulating the diagrams is equivalent to proving things in
| the category, provided you've shown soundness and completeness.
| moralestapia wrote:
| >other than boxes being connected by arrows
|
| Well, that's because that's basically it, lol.
|
| But I get your sentiment and, sure, there's a lot of things
| where this could be applied and that hasn't happened already.
| It's definitely a field with a prolific future, though. I've
| personally applied many ideas I got from there into my smallish
| ventures with good results.
| whatshisface wrote:
| But that's _not_ "basically it," there are lots of high-
| flying theorems that make it an entire area of mathematics.
| moralestapia wrote:
| Well, then I have no idea why you asked your previous
| question. -\\_(tsu)_/-
| whatshisface wrote:
| Because applied category theory stops at translating
| everything into boxes and arrows. There's no "applied
| Yoneda lemma."
| vladf wrote:
| lol, you picked the one thing category theory actually
| has examples of not being abstract nonsense for
|
| https://mathoverflow.net/questions/12511/what-is-yonedas-
| lem...
| larve wrote:
| I'm not sure that's true. This is a surface /
| introductory article, but if you go deeper into say,
| categorical databases, modeling of attacks
| (https://arxiv.org/pdf/2103.00044.pdf), there sure is
| some wilder CT at work. I'm leaving out programming as
| applied category theory because there is no shortage of
| refined concepts there (type theory, all the haskell
| libraries, many things I don't even comprehend).
|
| But to me, the value in ACT is actually learning how
| "simple" some of the other fields could be, because it
| allows me to communicate with non-software engineers, and
| actually have them contribute to software.
|
| I did a lot of work with state machines as composable
| abstractions for concurrency and flow control, and
| mechanical engineers were able to find some really subtle
| say, race conditions, just by pointing out "hey, isn't
| there an arrow from this to this, if the limit switch
| catches early?"
| lgdw wrote:
| It's the actual process of translating everything into
| boxes and arrows that's the core of ACT.
| hackandthink wrote:
| In computing you can apply Yoneda for optimizations.
|
| "Each of the steps is fairly compelling, except perhaps
| the second one, which rests on the Yoneda Lemma"
|
| see "Kan Extensions for Program Optimisation"
|
| https://www.cs.ox.ac.uk/ralf.hinze/Kan.pdf
| YetAnotherNick wrote:
| Well, not exactly. Things till functions and functor are part
| of almost every big enough theory like set theory or even
| just natural numbers and used everywhere, and if arrows are
| only used for describing that, I wouldn't say it is
| application of category theory.
|
| Only point of category theory starts when you go higher than
| that and deal with more abstract and generalizable things e.g
| monads(which again is used in other theories), bigger
| infinities, ordering of infinities etc.
| dqpb wrote:
| So, if I already model systems via boxes and arrows, and use
| things like petri nets, then am I good, or do I still need to
| learn category theory?
| larve wrote:
| Arrows and boxes is pretty much what category theory is about.
| You have objects connected by morphisms, and all further
| structure and concepts are derived from that.
| whatshisface wrote:
| Yeah, but you can only be said to be applying category theory
| if you use some of those structures or concepts.
| larve wrote:
| I am asking myself that question regularly, as I'm trying
| to get more comfortable with "real" category theory. My
| background is programming, and I've become familiar with a
| lot of the applied CT (functors, monads, monoids,
| applicatives, ...).
|
| I think the point of category theory, especially applied
| category theory, is recognizing what can be further
| abstracted as an arrow and an object. This turns something
| that originally is complex and has no apparent structure
| into a simple dot and arrow, again. Then rinse and repeat.
|
| For example, you can take a for loop that applies a
| function to a list and then creates a new list. You can't
| "easily" add another for loop that then applies a second
| transformation. But if you recognize the functor from the
| category of types to the category of types, then you can
| formulate your 2 composed for loops as `list.map(f1 | f2)`,
| and everything is "trivial" arrows and objects again.
|
| Turn that into a function that returns a list, and you want
| to concatenate the result. "Annoying" to write, you have to
| flatten your list. Recognize the monad, back to a simple
| composition of two morphisms, even though the morphisms
| encapsulate a lot.
|
| Learning and applying CT I think is recognizing which
| things can be conceptualized as a morphism, which then
| magically makes things appear "simple." Yet it is only
| simple if you have done that recognition work, and more
| advanced concepts in CT are there to assist you.
| lgdw wrote:
| If anyone is interested in Applied Category Theory, definitely
| check out the Topos Institute in Berkeley [1]. They do weekly
| seminars that they post on youtube and a really intriguing blog.
| I must say that David Spivak is a treasure to hear speak. 7
| Sketches in Compositionality [2] was my introduction into
| Category Theory (written by Spivak and Brendan Fong, another
| member of Topos), and it really sold the idea of Category Theory
| as a field that's not just a mathematical meta-language but also
| a field that can stand on its own. I recommend it over Mac Lane's
| CWM if you're not a mathematician.
|
| [1] https://topos.site/ [2] https://arxiv.org/abs/1803.05316
| jesuslop wrote:
| Agreed on the institute and Spivak. But CWM is, er, for working
| mathematicians. Leinster's Basic Category Theory, or Awodey
| Category theory are more unassuming.
| lgdw wrote:
| Yes, that's why I recommend starting out with 7 Sketches.
| zozbot234 wrote:
| The nLab https://ncatlab.org/nlab/show/HomePage is a useful
| reference for category theory terminology and results.
| cwzwarich wrote:
| Which of the results mentioned in the article are proven by
| applying some result of category theory to another field, and
| which are just stated using category theory (with the real
| mathematical insight lying elsewhere)?
| whatshisface wrote:
| If you translate everything to being stated in terms of
| category theory, it clarifies how it all works and makes it
| easier for people to go from one area to another. It is a bit
| like what Grothendieck did with abstract algebra. Imagine if
| every sub-field of mathematics had their own word for group,
| and that's something like how category theory fans see the
| present world.
|
| There's no such thing as a theorem that can only be proven with
| category theory, because whatever specific thing you're
| applying category theory to already has all of the properties
| that would make the theorem true _without_ category theory
| being involved - if it didn 't, you wouldn't be able to treat
| it as if it was a category. Categories are not the kind of
| mathematical invention that, for example, ordinary differential
| equations or matrices are.
| cwzwarich wrote:
| You could say the same thing for any abstract mathematical
| construct, e.g. metric spaces. There's no theorem (that's not
| itself about metric spaces) that can only be proven using
| metric spaces. It's always possible to make new abstractions
| (simply take the antecedent of any theorem), so whether you
| adopt a new abstraction is a matter of taste and fashion.
|
| In Grothendieck's early work on abelian categories,
| categories are themselves the objects of mathematical study,
| and nontrivial results about them are established.
| hackandthink wrote:
| I agree: "There's no such thing as a theorem that can only be
| proven with category theory".
|
| But sometimes it feels like Category Theory is rebuilding the
| world and there are genuine theorems.
|
| Epilogue: Theorems in Category Theory
|
| https://emilyriehl.github.io/files/context.pdf
| isitmadeofglass wrote:
| > If you translate everything to being stated in terms of
| category theory, it ...
|
| ... makes it incomprehensible to experts in the field and
| laymen alike!
| bmitc wrote:
| Anyone interested in category theory might be interested in the
| brand new book _The Joy of Abstraction: An Exploration of Math,
| Category Theory, and Life_ by Eugenia Cheng.
|
| https://www.amazon.com/Joy-Abstraction-Exploration-Category-...
|
| Then there's of course the classic introduction _Conceptual
| Mathematics_ by Lawvere and Schanuel.
|
| https://www.amazon.com/Conceptual-Mathematics-First-Introduc...
| mhh__ wrote:
| Baez's blog is basically mathematical crack cocaine
| Karrot_Kream wrote:
| Only if you're an algebraeist. There's a lot more to math than
| algebra.
| jesuslop wrote:
| He moved recently from Twitter to mathstodon.xyz
___________________________________________________________________
(page generated 2022-11-01 23:01 UTC)