[HN Gopher] Why I am learning category theory
___________________________________________________________________
Why I am learning category theory
Author : larve
Score : 163 points
Date : 2022-11-30 16:13 UTC (6 hours ago)
(HTM) web link (the.scapegoat.dev)
(TXT) w3m dump (the.scapegoat.dev)
| charcircuit wrote:
| Honestly, this is a waste of time and is not going to help as
| much as the author thinks it is. There is no secret from category
| theory that will make one's design 10x better. Not everything is
| even applicable.
|
| >I hope that category theory will allow me to formalize my
| intuitive understanding of abstraction, put words to it, and use
| those words (or, better, words others have written) to explain my
| thinking.
|
| Note how this goal doesn't include anything about improving the
| author's software engineering ability. The goal is to be able to
| use category theory to describe existing concepts. Why not us
| just describe it in ways that 99% of software engineers already
| understand? Why not learn good software design directly instead
| of through a subset of category theory which you have to
| translate?
| larve wrote:
| author here, the way I see it is that nothing about my software
| per se will change. I do indeed like to write things in a
| "plain" fashion instead of littering my code with high-level
| constructs that only a few people understand.
|
| However, it is "generative" knowledge. Having a good intuition
| for monads is what allows me to break down a fair amount of the
| mundane tasks I have to do (say, breaking down and migrating
| infrastructure configuration) in steps that work and stand the
| test of time. That's the thing about say, monad. An applied
| monad just looks utterly trivial, because, really, they are. If
| they weren't they wouldn't be worth using.
|
| It also allows me to mine the literature or reuse things I've
| worked out in the past, for example exploiting monoidal
| structure for optimizing computation by leveraging
| associativity, for example.
| charcircuit wrote:
| >It also allows me to mine the literature or reuse things
| I've worked out in the past, for example exploiting monoidal
| structure for optimizing computation by leveraging
| associativity, for example.
|
| This is an algebraic concept and it is possible to learn this
| idea directly in a software engineering context than a
| mathematical one.
| larve wrote:
| Also, this is very much what works for me. I love to think in
| "structure" and patterns, and category theory diagrams and
| the way concepts are formulated brings me "joy", if that
| makes sense. It resonates with my cognition in the way say,
| common lisp, does, and that makes it quite fun and enjoyable.
|
| Does it for everybody? Most certainly not.
| Mimmy wrote:
| This is a bit unfair. The author never claimed it would make
| them a 10x engineer.
|
| Learning almost anything is useful in some capacity. Is
| everything you learn equally important? Maybe, maybe not, but
| you never know in advance how things might end up useful.
|
| Of all the things one can study, math seems to be a pretty safe
| bet in terms of ROI.
| charcircuit wrote:
| From reading the article he justified his motivation of
| learning category theory to help him learn how to express
| himself better. I feel he is looking for some knowledge he is
| missing from category theory.
|
| I am not against learning category theory because you find it
| interesting, but one should be honest that it isn't going to
| benefit ones software engineering ability at least compared
| to studying good design directly.
|
| >math seems to be a pretty safe bet in terms of ROI.
|
| Ask most people how much math they have used of which they
| learned it university or high school. There are niches of
| math that are useful to niches. Study the wrong niche of math
| when you are in the wrong niche that doesn't use it, it will
| be a poor investment.
| yodsanklai wrote:
| Reading at the comments, people confuse concepts like monoids and
| functors with category theory.
| mrkeen wrote:
| > functor
|
| Google search first result: Functor -
| Wikipedia https://en.wikipedia.org > wiki > Functor
| In mathematics, specifically category theory, a functor is a
|
| > monoid
|
| https://en.wikipedia.org/wiki/Monoid_(category_theory)
| larve wrote:
| They're concepts in category theory? Since category theory's
| goal is to find common abstractions behind concepts from other
| fields (mathematics or otherwise), it makes sense some of those
| concepts appear in other fields. Their definition in a category
| theory context is different, usually, since you can only
| express them using morphisms between objects in a category.
|
| (edit: typo)
| khazhoux wrote:
| As a programmer and hobbyist math reader, I found category theory
| to be very unrewarding (and I gave up on it) because of the lack
| of interesting theorems and lemmas. My takeaway was that there's
| Yoneda lemma and really nothing interesting before you reach
| that. Like, CT describes a set of rules but very little emerges
| from those rules.
|
| My complaint has nothing to do with whether CT is useful or
| practical. By contrast, abstract algebra can be taught (e.g., in
| Herstein's books) as pure abstraction (very dry and without
| presenting any real-world connections), but you reach Lagrange's
| theorem right away -- which is an simple-but-awesome result that
| will wake up your brain. You reach Cayley's theorem and others
| quickly, and each is more exciting that the last. And this is all
| while still in the realm of purely-abstract math.
| solomatov wrote:
| > As a programmer and hobbyist math reader, I found category
| theory to be very unrewarding (and I gave up on it) because of
| the lack of interesting theorems and lemmas. My takeaway was
| that there's Yoneda lemma and really nothing interesting before
| you reach that
|
| One of the most interesting things in CT are adjoints. They
| happen literally everywhere. For example, static analysis via
| abstract interpretation is an example of adjoint (which in this
| case is called Galois connection). Free structures also give
| rise to adjoints.
| Koshkin wrote:
| Sure, but what does the knowledge of something being an
| adjoint give you?
| larve wrote:
| Here's a talk I'm chewing on right now:
| https://www.youtube.com/watch?v=TNtntlVo4LY
|
| as with every abstraction, its value is in the value it
| brings you. That sounds a bit tautological, but I think
| that's the crux of the matter. If you like abstraction, and
| abstractions help you think, you are going to find value in
| them. If you feel they bring you nothing, then there is no
| need for you to use them.
| Koshkin wrote:
| Your answer sounds exactly like category theory to me!
| (Or, if category theory had something to say on this
| topic, that's what it would say.)
| solomatov wrote:
| There are a lot of interesting properties:
|
| - Adjoints preserve limits/colimits.
|
| - Adjoint functors give rise to a monad
|
| - They are connected to universal morphisms
| Koshkin wrote:
| I mean, as a programmer?
| solomatov wrote:
| As a general, i.e. React programmer, there's not a lot of
| value. However, as I said, if you work in some areas,
| i.e. programming languages, or logic it might be even
| requirement in some areas to be productive.
| thr3ads wrote:
| I became very interested in CT from a biological perspective. The
| work originates from Robert Rosen who describes how
| biological/complex systems are not (completely) reducible to
| formal systems (aka any model of a natural system will always be
| incomplete+it is impossible to explicitly list out all the rules
| governing the system) because they "contain a model of
| themselves" to which they anticipate the future and act on
| towards their benifit.
|
| Many relate his work as closely tied to Godel's incompleteness
| theorem but for biology. The purpose of using category theory is
| that it is general enough to not talk about specific parts of an
| organism's construction, but rather how their general functional
| parts relate to each other.
| xupybd wrote:
| I tried this a couple of years ago. However it went over my head
| I think I need more fundamentals before I can approach this
| again.
| aleyva wrote:
| Super cool-- love the discussion around diagrams and why they're
| so critical to humans
| edgyquant wrote:
| I've become increasingly obsessed with set theory. I think we can
| derive set theory from Turing machines and basically "solve"
| incompleteness.
| WFHRenaissance wrote:
| As a former category theorist: don't learn category theory unless
| you're already rich or want to do it for fun.
|
| It will be a lot less rewarding than you expect RE: your
| engineering ability/understanding.
| Koshkin wrote:
| But how do you know (being a theorist)?
| nnoitra wrote:
| Will it make you a better React dev tho?
| revskill wrote:
| Yes. A React Component could be defined as a Functor with
| contramap function which map props with function.
|
| const renderer = props => <h1>Hello {props.pageName}</h1>
|
| const Title = ReactComponent(renderer).contramap(props => {
| pageName: props.title })
|
| Title.fold({ title: 'Home page' }) // <h1>Hello Home page</h1>
| onemoresoop wrote:
| >Will it make you a better React dev tho?
|
| Will it make you write code that is more optimal and yet harder
| to penetrate by others?
| yakshaving_jgt wrote:
| I think the best way to become a better React developer is to
| learn Elm, and then build your React apps the same way Elm
| would have forced you to.
| xedrac wrote:
| Of course Elm is closely related to Haskell, which is a
| playground for category theory. I think learning the why
| behind it all can be useful in subtle ways.
| yakshaving_jgt wrote:
| It might be, but personally I don't know CT and I run my
| business on Haskell and have been writing Haskell
| professionally for most of my career now.
|
| So hopefully nobody is feeling intimidated by fancy mathy
| stuff. Haskell is just this cool, productive programming
| language.
| quickthrower2 wrote:
| ... and Redux was born!
| yakshaving_jgt wrote:
| Quite literally.
|
| https://redux.js.org/understanding/history-and-
| design/prior-...
| nnoitra wrote:
| Isn't Redux only used when the app becomes too complex
| with really complex state?
| quickthrower2 wrote:
| I think so. Despite being an Elm fan I never used Redux.
| My side projects or work projects are small so local
| state and context were more than enough.
|
| Although Redux is like Elm, the language (Typescript or
| ES) make immutability hard so it doesn't feel as natural
| a paradigm.
|
| Also pragmatically calling setState from an event is just
| easier for small projects.
| larve wrote:
| Author here, I actually think so. The rendering of the virtual
| DOM as well as hooks are fairly interesting mathematical
| constructs. A pattern I use a lot in web applications is the
| state reducer, which is really a fold over events and state.
| Seeing the functional nature of it (and reactive programming in
| general) can make for quite composable react code, while it is
| easy to make either a verbose mess of propdrilling or do a lot
| of tricky context mixing.
| tunesmith wrote:
| I'd love to see some examples of your diagrams. Are they all
| hand-written or do you use online tools for them? I do quite
| a bit of graph diagramming but not for detailed planning of
| implementation. Best example I've seen along those lines are
| the xState tools for state charts (https://stately.ai/viz).
| larve wrote:
| I love xstate! I do use plantuml a lot for sketching, but
| most is done on paper or whiteboards and is quite transient
| in nature. I must have hundreds if not thousands of
| sketchbooks pages that look like this:
|
| https://publish-01.obsidian.md/access/017fdca1a82df1fa88d36
| b...
|
| https://publish-01.obsidian.md/access/017fdca1a82df1fa88d36
| b...
|
| https://publish-01.obsidian.md/access/017fdca1a82df1fa88d36
| b...
| tunesmith wrote:
| These are great. You could probably get a lot of mileage
| out of a post that explores how to model a react
| component functionally in diagrams.
| larve wrote:
| https://media.hachyderm.io/media_attachments/files/109/405/
| 5...
|
| This looks very mundane but I do think about it very
| mathematically as well: user interaction with a search
| engine. The "encode" arrow for example is very much about
| NLP and tokenizing, which is a functor from the "category"
| of natural language to the functor of "lucene tokens" which
| then has a functor to "lucene queries". This is of course
| the very mundane typing of functions as:
|
| function parseQuery(query: NaturalLanguageString):
| LuceneQuery
|
| nothing spectacular, but the abstract approach means I know
| I can cache/batch/precompute/distribute/pipeline/modularize
| it.
|
| Similar mathematical concepts apply to all the other
| arrows, even if some are a bit wild (how does a search
| result influence a person's ideas?) But it means I can try
| to model the "wildness", and create say a probabilistic
| model to exercise and understand how my search engine
| actually performs (see for example click models and
| probabilistic graphical models)
|
| I hope that makes sense?
|
| edit: forgot picture link
| antimora wrote:
| I recommend "how to bake pi" by Eugenia Cheng for a high level
| introduction, followed by her in-depth (but still approachable)
| book "The Joy of Abstraction"
| mark_l_watson wrote:
| Cool, I am also spending a little time on this. I bought a CT
| book by Emily Riehl but I am finding it rough going.
|
| I find her YouTube talks and lectures to be easier to follow.
| codekilla wrote:
| Try Eugenia Chang's new book, _The Joy of Abstraction_. Riehl's
| book is very technical.
| mark_l_watson wrote:
| Thanks I will look at it.
| oxff wrote:
| To obviously debunk any and all FP autism coming at your way.
|
| To give credit where credit is due, most of the time some
| application functionality being described through FP jargon gives
| a better spec of its behavior than the same through OOP jargon.
| dboreham wrote:
| This is exactly why I learned about it.
| rslice wrote:
| I strongly recommend this presentation: "John Baez: "Symmetric
| Monoidal Categories A Rosetta Stone"[0]. It is easy to get lost
| in the ocean of theorems and definitions and overlook some
| powerful core concepts.
|
| [0]https://www.youtube.com/watch?v=DAGJw7YBy8E
| dboreham wrote:
| Even though I've done much reading on the subject, and watched
| many of his lectures, my brain still jumps to music and Joan
| Baez.
| wnoise wrote:
| They're cousins. Joan's father, his uncle, was also a
| physicist.
| kevinventullo wrote:
| This crowd may not want to hear this, but as a former
| mathematician, the DS/Algorithms knowledge I gleaned from
| Leetcode grinding has been far more useful in my day-to-day work
| than any of the category theory I once used on a regular basis.
| adamddev1 wrote:
| Bartosz Milewski's series of lectures on YouTube is a really
| engaging and enjoyable introduction to category theory. These are
| really helping me get it.
| https://www.youtube.com/playlist?list=PLbgaMIhjbmEnaH_LTkxLI...
| Tainnor wrote:
| 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 also
| learn the category theory abstraction of it. The same goes for
| semigroups, monoids, folds, functors, ...
|
| I'm sure there's a benefit in category theory once you want to
| unify all these abstractions and talk about all of them together,
| but I see so many people who think they have to learn CT before
| they can understand monads in e.g. Haskell, and I don't really
| understand why.
| larve wrote:
| author here, for context, I do have a reasonable background in
| maths (algebra, analysis, statistics) at a CS master-ish level
| (self-taught and a long time ago, though), as well as spent
| quite some time with programming language / type theory when I
| was younger, and I do use monads quite a bit in my day to day
| programming. In fact, the fundamental algebra concepts (rings,
| groups, etc...) as well as fundamental CS theory (grammars,
| proof theory, semantics, ...) were the only maths I felt
| reasonably comfortable with, compared to say, calculus or
| statistics which really did my head in and ultimately caused me
| to drop out of university.
| bmitc wrote:
| How do you know analysis at a "CS master-ish level" (not sure
| what that means given it's a mathematical subject) but
| calculus did your head in? I'm not being judgmental but am
| just genuinely confused given that analysis is the foundation
| for calculus. :)
| larve wrote:
| Calculus (at least our exams and lecture) were so much
| about "calculating" and applying rules and clever tricks on
| complex functions and multiple dimensions which just...
| didn't work for me. I had a lot of other things going on,
| so this recollection is probably off. Calculus and diff eqs
| started making sense to me when I started working in
| mathematica and systemmodeler, and realizing that it was a
| brilliant tool. It probably also came from the way it was
| taught, which was completely devoid of any historical or
| practical context. It was just a lot of "compute the
| laplacian of e^i_sin(phi) or whatever.
|
| I found groups, limits, continuity, fields to be much more
| amenable to my thinking. It felt way more similar to the
| things I really enjoyed (building software in scheme and C
| and writing exploits in assembly).
| bmitc wrote:
| Oh, I see. So it seems it was more about the presentation
| and interest rather than the concepts. You may like
| _Calculus_ by Michael Spivak if you 're interested in it
| again. It is much more analytical than computational.
| larve wrote:
| That's one of the books I used when I got back into it.
| These days, there is so much great material on youtube
| and edx and coursera (plus maths stackexchange and
| discords) that it's absolutely fantastic to learn maths,
| as fantastic instructors are immediately available.
|
| For me, I realized thst I need to write the code to
| accompany the maths, because it helps me disambiguate
| mathematical notation and put "types" on things.
|
| It helped me a lot to work alongside real maths PhDs and
| realize that they have a very "intuitive" approach to
| maths, and don't necessarily yeet lemmas and proofs
| around all day, instead spending a lot of time
| brainstorming on the whiteboard and discussing things
| out, very similarly to software design. It was one of
| them telling me that my thinking was very mathematical
| that helped me "deconstruct" the fear of maths that I had
| built up.
| athrowaway12 wrote:
| Yeah, [edit: I doubt this]. I have a degree in math and cs.
| It sounds like parent comment doesn't really know analysis.
| The exercises in Rudin 1 are way harder than memorizing
| some rules to evaluate integrals. [Edit: at least for me;
| and I've never heard someone say the opposite before.]
|
| At least for American university-level calculus vs.
| American university-level analysis/topology over metric
| spaces.
|
| > _self-taught_
|
| Ah, makes more sense. I am also mostly self taught for most
| math. From my experience, I find it hard to believe after
| you did the exercises in PoMA, that calculus was harder.
| larve wrote:
| That's how I remember it. I know I had to take calculus
| twice, but passed analysis the first time. To be fair,
| this is 20+ years ago and my memory sucks at the best of
| times.
|
| Looking at it now, I think maybe I just found it too
| boring to remember the tricks, and too tedious to not
| make mistakes, while I found coming up with proofs more
| "interesting" and requiring less rote memorization.
| athrowaway12 wrote:
| Ah, for sure pure math is much more enjoyable to learn.
| I'm glad you find math interesting. Especially as a
| writer; that's really cool. Sorry for my previous
| comment.
| Tainnor wrote:
| It's a common observation that many mathematicians and maths
| students tend to fall into either the algebraic or the
| analytic camp, although of course, there are more nuances and
| some people are genuinely good at both.
|
| I myself find beauty in some parts of analysis, but algebra
| definitely speaks more to me (e.g. I find a proof of
| Lagrange's Theorem more beautiful than one of the
| Intermediate Value Theorem). So I can relate.
| Karrot_Kream wrote:
| How much do you think your predilection for algebra affected
| your interests? Most folks who do CT as a hobby that I know
| are much weaker in analytical concepts than any working
| mathematicians that I knew.
| larve wrote:
| Honestly I'm pretty weak in both, but they seem to reflect
| my intuitions, if that makes sense? I'm nowhere near a
| working mathematician, and proofs usually bore me. I prefer
| writing code.
| Karrot_Kream wrote:
| If you're looking for an alternate perspective, I would
| suggest taking an advanced undergraduate analysis book
| and working through it, proofs and all. It'll teach you
| the same kinds of stuff that you're getting out of CT but
| will give you "working" (lol) knowledge of how to apply
| it. A lot of mathematical work is about creating math
| objects and relations and proving properties of these
| objects through their relations. The exercises in a good
| algebra book _will_ exercise this muscle and make your
| software organization better, at least IMO. Learning the
| definitions just isn 't a substitute.
|
| I can see why categories appeal if you're just looking at
| definitions, but CT often just abstracts/standardizes an
| approach that folks were already working with when
| working with rings, groups, topologies, etc. Going
| through the proofs will teach you when to apply what.
|
| Aluffi (Algebra: Chapter 0) makes a great book that
| teaches the basics of CT and brings it up while teaching
| regular algebra. I highly recommend it.
| larve wrote:
| I studied CS in germany in 1999 and we had "analysis
| 1+2+3" which I think was a fairly rigorous analysis
| treatment, I definitely did more than my fair share of
| proofs. I think that foundation accompanied me through
| all those years of programming and helped me read and
| pick up concepts related to type theory, algebra and
| functional programming.
|
| In parallel I developed this very "visual" way of
| thinking about structure that makes me really resonate
| with CT. In a way I'm less interested in learning new
| maths, more so than learning more about how people
| approach (complex) structures I already know with these
| very rudimentary concepts, and seeing how their
| formalizations match my "folk mathematics".
|
| I'm having a lot of fun!
|
| edit: thanks for the book recommendation! that looks like
| my kind of maths book
| larve wrote:
| i skimmed through aluffi, and it is indeed exactly the
| material I had at university in analysis and algebra,
| augmented with the category theory angle. this is great,
| thanks a lot. Now I have to find an affordable copy
| somewhere.
|
| I also like the focus on quotient groups and galois
| fields, as well as using graphs as recurring examples,
| which have been the only times I really put the pedal to
| the maths metal in my programming (for some crypto and
| error correction stuff).
| nonrandomstring wrote:
| To me it's part of the "stretch your mind" philosophy. Plenty
| of exercises that add some suppleness and help with all round
| problem solving. It's one reason I keep up with Lisp even
| though nobody cares much to learn or pay me to program in it
| these days. Any programme of discrete and abstract maths surely
| has the same benefits, with a little bit of different theory
| areas; number, group, sets, operator... all healthy stuff
| unless taken to extremes :)
| umanwizard wrote:
| But you can study all of that stuff without category theory.
| larve wrote:
| author here, Finding higher abstractions ultimately is
| about being able to draw parallels amongst a wider variety
| of concepts. It doesn't change the concrete thing / the
| lower levels of abstractions in the least, and it often
| makes sense to stay at that lower level when communicating
| or getting things done. Plus I personally enjoy it and I
| feel it gives me a much wider array of things to draw from
| when designing / thinking. It broadens my toolbox, even if
| at the end of the day, all I do is hammer nails.
| dwils098 wrote:
| I concur, the theory is not necessary to understand how to use
| it. Perhaps it is counter-intuitive and one would like hone
| their intuition. Still there are much better approaches to
| developing an adequate intuition than the theory, this is why
| traditional Math textbooks rely on exposition first, to
| establish the context of the theory...
| zozbot234 wrote:
| > 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 describe a category.
| layer8 wrote:
| 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.
| Tainnor wrote:
| I know a fair bit about logic and none of it involves any CT.
| That's not to say you can't find it in there somewhere as a
| unifying concept, but the fundamental theorems such as
| completeness and compactness of FOL, basic model theory,
| Godel's theorems, etc. do not require any CT.
|
| Also, reflexivity, transitivity and symmetry just define an
| equivalence relation, no need for CT there.
| Koshkin wrote:
| Heh, except when you wish to talk about "natural
| equivalence"!
| rssoconnor wrote:
| I agree with you. CT seems mostly useful as a way of devising
| entirely new abstractions, but once those abstractions are
| developed, you don't need CT to use them.
|
| For example if it were 2008 and you want to be inventor
| Applicative functors for use in Haskell, then knowing lax
| monoidal functors from CT might be helpful. But if you want to
| just use Applicative functors, you don't need to learn lax
| monoidal functors first.
|
| So programmers probably don't need to learn CT because they can
| just let the computer scientists devise their abstractions for
| them. But if you want to be a computer scientist and one day
| devise your own abstractions[0], then maybe CT would be
| helpful.
|
| [0]https://news.ycombinator.com/item?id=33805923
| chobytes wrote:
| Yeah Im unsure what the point is. The motivation for CT in
| programming seems weak.
|
| Eg Stuff about types and endofunctors feels like trivial
| examples using the jargon just to use it. OTOH discovering the
| Top->Grp functor in algebraic topology is kind of unexpected
| and revealing.
| umanwizard wrote:
| > 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
|
| Because people think "category theory" means "abstract math" in
| general, due to cargo-culting in and around the Haskell
| community.
| bmitc wrote:
| I also have a math background but am now a software engineer,
| and I agree. One can learn category theory all by itself, but
| it's relatively unimportant in software and computer science
| as far as I can tell. It's really only powerful as a
| unifying, abstraction, and conceptual relating tool in upper
| mathematics where the divisions of mathematics begin to blur.
| Tainnor wrote:
| I mean absolutely no disrespect to anyone doing serious work
| in CT or in Haskell - and I'm actually very interested in
| Haskell as a language per se and have been exploring it more
| in recent months - but having spent some time in Haskell
| communities, I have to agree.
|
| There's a lot of empty posturing by people who don't really
| seem to understand a lot of mathematics but still seem to
| have very strong convictions about certain aspects of it
| (constructivism is another such thing).
| Karrot_Kream wrote:
| Yeah when I read all of this "category theory expands your
| mind" thinking, it makes me think that folks were looking for
| mathematical maturity more than category theory. Work through
| any good book on algebra and analysis and you'll learn and
| prove a bunch of stuff about objects and relations.
| _448 wrote:
| It is not that one has to learn CT to do FP, but not knowing it
| makes it difficult to take part in discussions on the mailing
| lists.
| chowells wrote:
| > Category theory is really the mathematics of abstraction
|
| Mathematics is the mathematics of abstraction. That's all you're
| doing in math, from the beginning to the end. What's the same
| between "I have two sheep in this pen and five in that one" and
| "I have two apples in this basket and five in that one"? Hmm, you
| can abstract out 2+5=7, since it works the same in both contexts.
|
| Everything in math is creating and exploring abstractions. The
| good ones tend to stick around, the bad ones tend to be
| forgotten.
|
| Category theory is the mathematics of composition. How much
| knowledge can you throw away and create reusable patterns of
| composition? How many interesting things can you find by adding
| back the smallest bits of additional structure on top of that
| minimum? How well do those things compose together, anyway?
| criloz2 wrote:
| I am also in the process of learning cat theory, I don't have a
| cs background, but I ending working as full-stack developer
| because it was economically more rewarding, I will recommend to
| programmers to have a good understanding of set theory, binary
| relations and order theory (linear orders, partial orders,
| lattices), it gives you very powerful abstractions that allow you
| to write new algorithms about anything.
| Koshkin wrote:
| I think graph theory covers all this at a reasonable level of
| abstraction.
| qubex wrote:
| As opposed to "why am I learning category theory", which is
| usually screamed deep in the night before an exam.
| IntFee588 wrote:
| You learn category theory for intellectual curiosity. I learn
| category theory to pass a Haskell course. We are not the same.
| i_am_toaster wrote:
| 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 see the reason in something. Can anyone give me
| a practical applied way in which category theory is a benefit to
| your design rather than just creating higher level jargon to
| label your current design with?
| zmgsabst wrote:
| I think the real insight of category theory is you're already
| doing it, eg, whiteboard diagrams.
|
| Category theory is the language of diagrams; it studies math
| from that perspective. However, it turns out that category
| theory is equivalent to type theory (ie, what computers use).
| So the reason _why_ diagrams can be reliably used to represent
| the semantics of type theory expressions is category theory.
|
| My workflow of developing ubiquitous language with clients and
| then converting that into a diagram mapping classes of things
| and their relationships followed by translating that diagram
| into typed statements expressing the same semantics _is_
| applied category theory.
|
| The "category theory types" are just names for patterns in
| those diagrams.
|
| Trying to understand them without first getting that
| foundational relationship is the path to frustration -- much
| like reading GoF before groking OOP.
| mrkeen wrote:
| > I always feel these posts are filled with category theory
| jargon
|
| The 80/20 rule really applies here. Most of the time there's
| only a few key type classes that people use. Pretty much just
| Monad, Monoid, Applicative, Functor. If you grok those, then
| what people say makes a lot more sense.
|
| > Can anyone give me a practical applied way in which category
| theory is a benefit to your design
|
| Monad is probably the best example, because so many different,
| important libraries use it. Once you know how to code against
| one of them, you kinda know how to code against all of them!
|
| The following is code written in the STM monad. It handles all
| the locking and concurrency for me: transfer x
| from to = do f <- getAccountMoney from
| when (f < x) abort t <- getAccountMoney to
| setAccountMoney to (t + x) setAccountMoney from (f
| - x)
|
| This same code could be in the State monad (excluding the line
| with 'abort' on it). Or it could be in the ST monad. Or the IO
| monad. Each of those is doing radically different things under
| the hood, which I don't have the brainpower to understand. But
| because they expose a monadic interface to me, I already know
| how to drive them using simple, readable, high-level code.
|
| As well as the 4 monads mentioned above, parsers are monadic,
| same with Maybe and Either, List. The main concurrency library
| 'async' is also monadic (though it just uses the IO monad
| rather than defining an Async monad).
|
| Often the people writing your mainstream libraries know this
| stuff too. If you're calling flatMap (or thenCompose), you're
| calling monadic code. The writers just shirk from calling it
| monadic because they're worried people will suddenly not
| understand it if it has a scary name.
| deltaseventhree wrote:
| Knowing category theory helps you better design interfaces.
| Exactly like the interfaces in OOP.
|
| Alot of the generic interfaces you design in OOP end up being
| useless. Never re-used and pointless. You never needed to make
| these interfaces in the first place
|
| In category theory, you will be able to create and identify
| interfaces that are universal, general and widely used
| throughout your code. Category theory allows you to organize
| your code efficiently via interfaces and thus enable Maximum
| reuse of logic.
|
| When creating an interface you largely use your gut. Category
| theory allows you to draw from established interfaces that are
| more fundamental. Basically class types in haskell.
|
| If you want to see the benefit of category theory, you really
| need to use haskell. Monads for example are a pattern from
| category theory.
|
| Also a lot of what people are talking about in this thread is
| exactly what I'm saying^^. I'm just saying it in less
| complicated jargon.
| ukj wrote:
| Category theory is to functional/declarative programming what
| design patterns are to OO programming.
|
| Patterns for decomposing problems and composing solutions.
|
| To ask "How is it useful?" Is to ask "How are design patterns
| useful in OO?".
|
| But you already know the answer...
|
| Is there an advantage over just inventing your own vocabulary?
| Yeah! You don't have to reinvent 70+ years of Mathematics, or
| teach your language to other people before you can have a
| meaningful design discussion.
| DalekBaldwin wrote:
| Here are some of the more practical insights for medium/large-
| scale software design that have stuck with me. They apply
| regardless of whether I'm working in a language that lets me
| easily express categorical-ish stuff in the type system:
|
| - Triviality
|
| The most trivial cases are actually the most important. If I
| build a little DSL, I give it an explicit "identity"
| construction in the internal representation, and use it
| liberally in the implementation, transformation phases, and
| tests, even though obviously its denotation as a no-op will be
| optimized away by my little DSL compiler, and it may not even
| be exposed as an atomic construct in the user-facing
| representation.
|
| - Free constructions
|
| When it's difficult to separate a model from an implementation,
| when simple interfaces are not enough because the model and
| implementation are substantially complex, multilayered systems
| on their own, often the answer is to use a free construction.
|
| Free constructions are a killer tool for allowing the late-
| binding of rather complex concerns, while allowing for
| reasoning, transformation, and testing of the underlying
| components without worrying about that late-bound behavior.
| "Late-bound" here does not have to mean OO-style dynamic
| dispatch -- in fact now you have more expressive power to fuse
| some behaviors together in a staged manner with no runtime
| indirection, or to make other behaviors legitimately dynamic,
| differing from one call to the next. Tradeoffs in the
| flexibility/performance space are easier to make, to change,
| and to self-document.
|
| This is particularly useful when you need to start addressing
| "meta" concerns as actual user-facing concerns -- when your
| project matures from a simple application that does Foo into a
| suite of tools for manipulating and reasoning about Foo and
| Fooness. Your Foo engine currently just does Foo, but now you
| want it to not just do Foo, but return a description of all the
| sub-Foo tasks it performed -- but only if the configuration has
| requested those details, because sometimes the user just wants
| to Foo. So you embed the basic, non-meta-level entities
| representing the actual component tasks in a free construction,
| compose them within that free construction, and implement the
| configurable details of that composition elsewhere.
|
| - "Sameness"
|
| Making clear distinctions between different notions of sameness
| is important. Identity, equality, isomorphism, adjointness --
| sure, you might never explicitly implement an adjunction, but
| these are important notions to keep separate, at least
| conceptually if not concretely in source code entities, as a
| piece of software grows more complex. If you treat two things
| as fundamentally the same in more ways than they really are,
| you reach a point where you now can no longer recover crucial
| information in a later phase of computation. In an
| indexed/fibered construction, this X may be basically the same
| as that X, but this X, _viewed as the image_ of a
| transformation applied to Y is quite different from that X,
| _viewed as the image_ of a transformation applied to Z,
| although the images are equal. So can I just pass my X 's
| around everywhere, or do I need to pass or at least store
| somewhere the references to Y and Z? What if _computationally_
| I can only get an X as the result of applying a function to Y,
| but _conceptually_ the functional dependency (that is, as a
| mathematical function) points the other way around, from X to
| Y? Paying attention to these easy-to-miss distinctions can save
| you from code-architecting yourself into a corner. You may
| discover that the true reserve currency of the problem domain
| is Y when it looks like X, or vice versa.
| gilmi wrote:
| If you have 24 minutes, George Wilson's talk about propagators
| is really interesting and demonstrates how we can find
| solutions to problems by looking at math.
|
| https://www.youtube.com/watch?v=nY1BCv3xn24
| rssoconnor wrote:
| 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
| i_am_toaster wrote:
| This is a lot to digest, but I'm responding to this one
| because of I think this attempts to answer my question and
| because of your 4th reference. That being said I need to ask
| some questions.
|
| Would I be correct in saying -- there are less complex
| objects, which are defined in category theory, that are
| useful in a generic way in combination with one another?
|
| If the answer to that question is yes, is there a place I
| look to find the mappings of these software topics/designs to
| these category theory objects such that I can compose them
| together without needing the underlying design? If that were
| the case, I could see the use in understanding category
| theory so that I could compose more modular and generically
| useful code.
|
| I have to admit though, I'm still fairly speculative and my
| thinking on this is very abstract and probably very flawed.
| larve wrote:
| I'm not entirely sure if that is what you are asking, but
| for example pure functions from a type A to a type B can be
| compose with pure functions from a type B to a type C, to
| form a pure function from A to C. A lot of programmer
| oriented CT takes place in the category of types, with
| morphisms being a function from one type to another.
| Programming in a purely functional style makes composition
| of functions... trivial, compared to a function that has
| side-effects due to mutation.
|
| Now of course this sounds trivial, but you can build much
| more refined concepts out of that simple idea. For example,
| creating product and sum types.
|
| And that's where the rabbit hole starts.
| rssoconnor wrote:
| I think your understanding is a little off the mark, at
| least with respect to my not-so-well written comment, which
| was just meant as a rambling story about how category
| theory influenced my and others development of (functional)
| programming "optics" over the last decade.
|
| The new "optics" people are have designed in reference 4
| are not themselves "elements of category theory", but
| category theory provides the theoretical framework that
| these composable optics live in. Once that framework is
| identified, it becomes much easier to say "oh, this new
| optic definition I've just identified, fits into this
| framework, and so does this other optic, and so forth"
|
| To make a loose analogy, one could imagine identifying
| triangles and cubes and such and such that have these
| rotational and reflective symmetries, and notice how you
| can compose those operations, and then see how performing
| specific shuffles of cards is also composable and has some
| properties similar to rotating cubes in that repeated
| operations have a certain period and other such things.
| Then when someone introduces you to group theory and says
| yes both the cube rotations and the card shuffling can all
| be seen as a group and group theory can be used to
| generically answer your questions about these otherwise
| seemingly very different operations. And then you start
| seeing that lots of things are groups, like that Rubik cube
| puzzle you have, or lines through an elliptic curve. Coming
| up with new optics is analogous to noticing various things
| are groups, a task that is much easier when you have group
| theory and know how to recognize a group when you see it.
|
| That said, I think a better answer to your question may be
| in one of my later replies
| https://news.ycombinator.com/item?id=33806744: Category
| Theory has been useful for devising an entirely new
| (functional) programming abstraction, the theory of
| "optics" in my case. But for day-to-day programming you
| don't normally need to invent entirely new programming
| abstractions, you can just use the ones that have already
| been developed by the computer scientists.
| epgui wrote:
| It's not kool-aid, it's applied maths. Just because you don't
| already know and understand it (and hence don't see the benefit
| of it) doesn't mean there's no clear and obvious benefit. But
| you do have to learn before you understand.
| salty_biscuits wrote:
| To be fair though, there is a wide spectrum of "usefulness"
| for pure mathematics concepts in applied mathematics. For
| less contemporary examples you don't need to know about
| Lebesgue measure to do practical numerical quadrature for
| applications. Or you don't need to know that rotation
| matrices are part of the SO3 group to do computer graphics.
| Sometimes the abstractions are powerful and sometimes they
| are kind of a distraction (or even make communication a
| problem). There typically needs to be a super compelling
| application to motivate a shift in baseline knowledge.
| floober wrote:
| For me, I use the simple stuff (Semigroup, Monoid, Monads,
| Functors, ..) the most. Often times I'll be reasoning about a
| problem I'm working on in Haskell and realize it is a monad and
| I can reuse all of the existing monadic control structures. It
| is also helpful the other way, where you start working with
| someone else's code and seeing that it is a e.g. Monad
| immediately tells you so much concrete info about the
| structure, where in a less structured language you might need
| to reed through a bunch of docs to understand how to manipulate
| some objects. The "killer app" is all of that extra structure
| shared throughout all of the codebases.
| picardo wrote:
| Same here. I drank the cool aid a few years back, and started
| using fp-ts in my frontend projects, hoping to use algebraic
| data types regularly. But today all I use is the Monad. I
| can't find any motivation to write abstract algebra to build
| UI widgets.
| floober wrote:
| > I can't find any motivation to write abstract algebra to
| build UI widgets
|
| This made me chuckle, because I am at this very moment
| trying to apply the "tagless final style" described here[0]
| to a custom GUI in a personal-for-fun-and-learning ocaml
| project : )
|
| [0] https://okmij.org/ftp/tagless-
| final/course/optimizations.htm...
| jerf wrote:
| "I've even watched some applied category theory courses online
| and have yet to feel I've gained anything substantive from
| them."
|
| To understand category theory's appeal in a programming
| context, you must understand the duality of power in
| programming languages. Some people call a language "powerful"
| when it lets you do whatever you want in the particular scope
| you are currently operating in, so, for instance, Ruby is a
| _very_ powerful language because you can be sitting in some
| method in some class somewhere, and you can reach into any
| other class you like and rewrite that other class 's methods
| entirely. Some call a language powerful when the language
| itself is capable of understanding what it is your code is
| doing, and further manipulating it, such as by being able to
| optimize it well, or offer further features on top of your
| language like lifetime management in Rust. This type of power
| comes from _restricting_ what a programmer is capable of doing
| at any given moment.
|
| If your idea of "power" comes from the first sort of language,
| then category theory is going to be of very little value to you
| in my opinion. You pretty much _have_ to be using something as
| deeply restrictive as Haskell to care about it at all. I am not
| making a value judgment here. If you never want to program in
| Haskell, then by all means keep walking past category theory.
|
| Haskell is very much a language that is powerful in the second
| way. It restricts the programmer moreso than any other
| comparable language; the only languages that go farther
| essentially go right past the limit of what you could call a
| "general purpose language" and I daresay there are those who
| would assert that Haskell is _already_ past that point.
|
| Category theory then becomes interesting because it is
| simultaneously a set of deeply restricted primitives that are
| also capable of doing a lot of real work, and category theory
| provides a vocabulary for talking about such restricted
| primitives in a coherent way. There is some sense in which it
| doesn't "need" to be category theory; it is perfectly possible
| to come to an understanding of all the relevant concepts purely
| in a Haskell context without reference to "category theory",
| hence the completely correct claim that Haskell in no way
| necessitates "understanding category theory". You will hear
| terminology from it, but you won't need to separately "study"
| it to understand Haskell; you'll simply pick up on how Haskell
| is using the terminology on your own just fine. (Real
| mathematical category theory actually differs in a couple of
| slight, but important ways from what Haskell uses.)
|
| So, it becomes possible it Haskell to say things like "You
| don't really need a full monad for that; an applicative can do
| that just fine", and this has meaning (basically, "you used
| more power than was necessary, so you're missing out on the
| additional things that can be built on top of a lower-power,
| higher-guarantee primitive as a result") in the community.
|
| This mindset of using minimal-power primitives and "category
| theory" are not technically the same thing, but once you get
| deeply into using minimal-power primitives pervasively, and
| composing them together, you are basically stepping into
| category theory space anyhow. You can't help but end up
| rediscovering the same things category theorists discovered;
| there are a hundred paths to category theory and this is one of
| the more clear ones of them, despite the aforementioned slight
| differences. I'd say it's a fair thing to understand it as this
| progression; Haskell was the language that decided to study how
| much we could do with how little, and it so happens the branch
| of math that this ends up leading to is category theory, but as
| a programmer it isn't necessary to "study" category theory in
| Haskell. You'll osmose it just fine, if not better by
| concretely using it than any dry study could produce.
|
| To be honest, I'm not even convinced there's that much value in
| "studying" category theory as its own thing as a programmer. I
| never studied it formally, and I wrote Haskell just fine, and I
| understand what the people using category theory terms are
| talking about in a Haskell context. If nothing else, you can
| always check the Haskell code.
|
| There is a nearby parallel universe where the Haskell-Prime
| community in the late 1990s and early 2000s was otherwise the
| same, but nobody involved knew category theory terminology, so
| "monad" is called something else, nobody talks about category
| theory, and nobody has any angst over it, despite the language
| being otherwise completely identical other than the renames. In
| this universe, some people do point out that this thing in
| Haskell-Prime corresponds to some terms in category theory, but
| this is seen as nothing more than moderately interesting trivia
| and yet another place where category theory was rediscovered.
|
| But I bet their Monad-Prime tutorials still suck.
| AnimalMuppet wrote:
| Then it seems fair to say that, since Haskell is the most
| restrictive language (or at least most restrictive in
| anything like general use), it had to have the most powerful
| theory/vocabulary/techniques for dealing with the
| limitations. (Or, more negatively, nobody else willingly put
| themselves in a straight-jacket so tight that they _had_ to
| use monads to be able to do many real-world things, like I /O
| or state.)
|
| > But I bet their Monad-Prime tutorials still suck.
|
| Funniest thing I've read today. Thank you for that gem.
| rssoconnor wrote:
| > Or, more negatively, nobody else willingly put themselves
| in a straight-jacket so tight that they had to use monads
| to be able to do many real-world things, like I/O or state.
|
| I want to emphasize how true this is. In the Haskell 1.2
| report, before Haskell Monads existed, the type of `main`
| was more or less: type Dialogue =
| [Response] -> [Request] main :: Dialogue
|
| The main function was took a lazy list of, let's call it OS
| responses, and issued a lazy list of requests to the OS,
| whose response you would find at some point on the input
| list. Your task was to keep your lazy generation of
| `Request`s in sync with yourself as you consumed their
| `Response`s in turn. Read ahead one to many `Response`s and
| your `main` would dead-lock. Forget to consume a `Response`
| and you would start reading the wrong `Response` to your
| request.
|
| The suggestion was to use continuation passing style
| (something that later we see conforms to the Continuation
| monad interface) to keep things in check, but this was not
| enforced, and by all accounts was a nightmare.
|
| So yes, Haskell's laziness straight-jacket (Haskell was
| basically invented to study the use of lazy programming
| without having to purchase Miranda) basically means they
| had to invent the use of Monads for programming, or at the
| very least invent the IO monad.
| hosh wrote:
| 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 implement the first concat, but
| not the latter. Without the latter, you couldn't do things
| like, accept an empty user input. You would have to write code
| like: defaults + user_input unless
| user_input_array.empty?
|
| This applies to things like, hashes, or even more complex
| objects -- such as ActiveRecord named scopes, even if they
| don't use a "+" operator. (But maybe, Hash objects can be "+"
| together instead of calling merge())
|
| This is all applicable to how you can design libraries and DSLs
| that seem intuitive and easy to use. Instead of just thinking
| about bundling a number of methods together with a data
| structure, you can make sure that a single method within that
| bundle works the way you expected across a number of objects.
| You might even be using these ideas in your code, but don't
| realize it.
| musk_micropenis wrote:
| 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.
| bo1024 wrote:
| For example, your language can implement sum(Array<X>) for
| any monoid X. And the sum of an empty list of integers can
| automatically return 0, while the sum of an empty list of
| strings can automatically return "". This sounds simple,
| but many programming languages make you learn special
| commands and notation for strings. A compiler could also
| leverage the fact that length() is a homomorphism, so
| length(a + b) = length(a) + length(b).
|
| Monoids are really simple, so you probably won't get a lot
| more examples there. But monads are a different story. Once
| you know the pattern, you really miss them. For example,
| Promises in Javascript are like painful versions of monads.
| There is a lot of special-case language support and
| reasoning around Promises that only apply to Promises. In a
| language with native support for monads, you could use the
| same code or libraries to handle patterns arising when
| using promises, as patterns arising with other monads like
| I/O.
|
| In summary, if you never try it, you may never know or care
| what you're missing, but that doesn't mean you're not
| missing anything...
| jiggawatts wrote:
| I can think of hundreds of "exceptions" to the category
| theoretic approach.
|
| So for example anything you can do to "string" type that
| isn't based on human language you should be able to do to
| an array of bytes, integers, or "well-behaved" objects.
| (Also "escaped" strings or strings in various encodings
| such as UTF-16 or MBCS.)
|
| Show me a language that implements all of those functions
| with interchangeable and uniform syntax!
|
| What does it even _mean_ when I say "well behaved"? It
| means that those objects need to have some traits in common
| with characters, such as: copyable, comparable, etc...
|
| To implement regex for objects would also require a "range"
| trait and perhaps others. Category Theory lets us talk
| about these traits with a formal language with
| mathematically proven strict rules.
|
| With C++ template meta programming it's possible to get
| most of the above, but not all, and it's not used that way
| in most code. It's also weakly typed in a sense that C++
| can't express the required trait bounds properly. Rust and
| Haskell try as well but still fall short.
|
| Category Theory shows us what we should aspire to.
| Unfortunately the tooling hasn't matured enough yet, but
| now that GATs have made it into Rust I'm hopeful there will
| be some progress!
| fdupress wrote:
| 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.)
| musk_micropenis wrote:
| 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.
| larve wrote:
| 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.
| musk_micropenis wrote:
| 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?
| tmoertel wrote:
| Consider the monoid abstraction in the context of batch
| processing. Anywhere you have a monoid, you have a
| corresponding "banker's law" that says you can find the
| generalized sum of a collection of items by partitioning
| the items into groups, computing the sum over each group,
| and then taking the sum of the sums as your final result.
| This idea has many applications in batch processing.
|
| For example, in the MapReduce framework, this idea gives
| rise to "Combiners" that summarize the results of each
| map worker to massively lower the cost of shuffling the
| results of the Map stage over the network prior to the
| Reduce stage.
|
| Another example: In distributed database systems, this
| idea allows many kinds of addition-like aggregations to
| be performed more efficiently by computing the local sum
| for each group under the active GROUP BY clause before
| combining the groups' subtotals to yield the wanted gobal
| totals.
|
| Basically, in any situation in which you have to compute
| a global sum of some kind over a collection of items, and
| some of those items are local to each worker, you can
| compute the global sum faster and with fewer resources
| whenever you can take advantage of a monoidal structure.
| larve wrote:
| Which is exactly the concept between optimizing for
| string concatenation and interning them, ultimately. Sure
| you can make do with the "algebraic" definition of a
| monoid, or entirely without it, but that doesn't mean the
| abstraction isn't there to inform your thinking and your
| research.
|
| One point that really stuck with me is how people who
| apply category theory (say, people at the topos
| institute) use the concepts as little tools, and
| everytime a problem crosses their way, they try out all
| the little tools to see if one of them works, similar to
| how Feynman describes carrying out problems in his head
| until one day a technique unlocks something).
|
| Having more general abstractions just allows them to be
| applied to more problems.
| larve wrote:
| 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.
| hosh wrote:
| 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.
| mettamage wrote:
| I am not great at math. But I learned about complex
| numbers for fun. It took a bit to make them "real" for
| me, 3B1B helped a lot as did asking myself how I find
| negative numbers real (negative integer: if something in
| the future will exist, it won't and the negative integer
| will be incremented, aka a debt to the future existence
| of whatever the number represents).
|
| Complex numbers: the number line is just a metaphor. What
| would happen if you make it 2D? Oh you can solve negative
| roots. Whenever a number needs to spin or have a negative
| root, it's a useful tool. Numbers are tools. Cool, that's
| "real" enough for me.
|
| I know I will never ever use it. Or at least, not in my
| current state of how I live my life. I liked learning it,
| there's something to be said for what is beyond your
| horizon. But I do think just like complex numbers,
| category theory needs a motivation that is compelling. In
| retrospect, learning complex numbers is most likely not
| useful for me.
|
| Oh wait a second, complex numbers helped me to understand
| trig. I never understood it in high school but 3B1B made
| it intuitive with complex numbers
|
| Nevermind, I'll just let this all stand here. It's fun to
| be open and convinced by myself to the other side while
| writing my comment :')
|
| I'm sure if I would have learned category theory, I would
| have written a similar comment as I think there are a lot
| of parallels there.
| hosh wrote:
| Azad has this description of imaginary numbers that
| really tickled me: "numbers can rotate".
|
| I remember my high school teacher teaching imaginary
| numbers in the trig class, and one of the other kids
| asked what they could be used for. This was an honors
| class and the kid skipped a math grade. Our math teacher
| couldn't talk about it off the bat, and unconvincingly
| told us about applications in electrical and electronic
| engineering. We still went through it, but none of use
| knew why any of it was relevant.
|
| I think if he had said "numbers can rotate", maybe some
| of us (maybe not me!) might have been intrigued by the
| idea. It would have been a way to describe how EM rotate.
|
| My own personal motivation for pursuing CT has to do with
| working with paradigms, and how are they related, and how
| they are not. Categories and morphisms seem to talk about
| the kind of things we can talk about with paradigms, yet
| much more precisely.
| tbenst wrote:
| Arguably from a mathematical perspective, the choice of '+'
| is poor as it implies that the operation is commutative when
| it's only associative. Julia used "foo" * "bar" for this
| reason: https://groups.google.com/g/julia-
| dev/c/4K6S7tWnuEs/m/RF6x-f...
| Koshkin wrote:
| Then the length() function would be a logarithm...
| vosper wrote:
| > Instead of just thinking about bundling a number of methods
| together with a data structure, you can make sure that a
| single method within that bundle works the way you expected
| across a number of objects. You might even be using these
| ideas in your code, but don't even realize it.
|
| I think this was GP's point. They complain that no-one
| explains why the category theory _jargon_ is useful. As you
| point out, the jargon is not needed in order to use the
| concept. Someone might even come up with the concept
| independently of the jargon.
| adamwk wrote:
| What language only allows concatenating a non-empty array?
|
| And it still doesn't explain why string concatenation being a
| monoid is useful in ruby. It's useful in Haskell because
| implementing one of their category-theory typeclasses means
| that type now inherits a stdlib-sized API that works for any
| monoid, not concrete types. But even Haskell hasn't proven
| that it's worth the jargon or abstraction after all these
| years; every other language remains productive without
| designing APIs at such a high level of abstraction.
| BenoitP wrote:
| I see no more than Groups in your comment. Which are very
| useful! Also having commutative operations makes for Abelian
| Groups, which enable operations to be reordered, and makes
| for implicit parallelism.
|
| Where is Category Theory?
| larve wrote:
| In category theory, everything has to be defined in terms
| of objects and morphisms, which can be a bit challenging,
| but it means that you can apply those concepts to anything
| that has "an arrow". it's of course just playing with
| abstractions, and a lot of the intuitive thinking in CT
| goes back to using the category of sets. For me however
| seeing the "arrow and composition" formulation unlocks
| something that allows me to think in a broader fashion than
| the more traditional number/data structure/set way of
| thinking.
| BenoitP wrote:
| > 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
| larve wrote:
| 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 concepts of a functor. I
| used to thing of a functor as some kind of data structure
| that you can map a function on, but in CT a functor is a
| morphism between categories that maps objects and
| morphisms while preserving identity and composition. This
| means I can start generating designs by thinking "I
| wonder if there is amorphism between my database schema
| category and my category of configuration files or
| whatever. Maybe something useful comes out, maybe not.
| layer8 wrote:
| 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?
| larve wrote:
| 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.
| layer8 wrote:
| > seeing the category theoretical definition of monoid
| https://en.wikipedia.org/wiki/Monoid_(category_theory)
| inspired me a lot.
|
| What applicable insight did you gain over the normal
| algebraic definition
| (https://en.wikipedia.org/wiki/Monoid)?
| larve wrote:
| Mostly confirm that drawing things as boxes and arrows
| even though I implement them as folds/monoids (state
| machines, binary protocol decoders) and implementing the
| comonoid by "reversing the arrows" (to do log
| reconstruction when debugging) has a name, and thus is a
| fruitful practice for me to continue doing, instead of it
| being "those weird drawings I keep noodling".
|
| Nothing is rocket science, and you can totally get there
| without even the traditional monoid definition, but
| seeing the same diagrams I kept drawing before porting
| something to more "traditional" code patterns was quite
| validating.
|
| completely rough whatever that tries to match stuff I did
| on a ps2 protocol decoder a while ago. Being able to
| invert state machines that use time ticks to advance
| requires adding additional counters to make them work
| properly, iirc. As you can tell none of this is formal,
| in fact I worked on this before starting my CT joint, but
| you can maybe see why I resonate more with the CT
| formulation of things.
|
| The bigger picture here is that when I do embedded dev, I
| only have so much memory to keep an event log, so I need
| to be able to work backwards from my last none state,
| instead of traditionally walking forward from an initial
| state and incoming events. That this whole concept of
| "swapping the arrows around" is something that reputable
| people actually study was super inspiring.
|
| https://media.hachyderm.io/media_attachments/files/109/43
| 4/7...
| hosh wrote:
| > But where is the Category Theory?
|
| I have no idea. I don't think I have really yet to grok the
| ideas around categories and morphisms. I'm very slow at
| learning this stuff.
|
| I do know that each of the small number of intuitions I
| have gained has sharpened how I reason about my code, that
| once I grokked a single intuition, they seem both simple
| and profound, and that there are even more that I don't yet
| understand.
|
| So for example, when you wrote "Also having commutative
| operations makes for Abelian Groups, which enable
| operations to be reordered, and makes for implicit
| parallelism", I never thought about that. Initially, I
| could almost feel like something coming together. After I
| let that sink in for a bit, and then it starts opening
| doors in my mind. And then I realize it's something that I
| have used before, but never saw it in this way.
|
| I was mainly answering the parent comment about why someone
| might want to drink the kool-aide as it were. I suppose my
| answer is, even though I know there are some powerful ideas
| with CT itself, the intuitions along the way each have many
| applications in my day-to-day work.
| Koshkin wrote:
| Actually, it is weird to see groups mentioned in this
| discussion at all. Non-commutative (generally) groups are
| useful in dealing with symmetries, but what symmetries can
| we talk about here? Abelian groups (and modules in
| general), on the other hand, are completely different
| beasts (seemingly only useful in homological algebra,
| algebraic geometry, and topology).
|
| Strings are a (free) monoid with respect to concatenation,
| sure, but it is easier to learn what a monoid is using
| strings as an example, rather to try and "learn" about
| strings by discussing monoids first. Why this is deemed
| useful by some is beyond me.
| layer8 wrote:
| It's monoids, not groups, but yeah, it's just knowledge
| about basic algebraic structures, no particular insight
| from category theory here.
| pinjo333 wrote:
| They describe composable patterns with a clear hierarchy. The
| jargon is useful, since it is the language in which they are
| described. I mean Turing machine, filesystem, socket and pipe
| are also jargon.
|
| A good example is LINQ, they use monads and functors. They just
| gave them other names.
| wisnesky wrote:
| Category theory does provide new algorithms if you unroll all
| of its definitions. For example, it reveals that SQL
| conjunctive queries can be run both "forward" and "backward" -
| an algorithm that is invisible in traditional SQL literature
| because that literature lacks the vocabulary to even talk about
| what "running backward" even means - it isn't an 'inverse'
| relationship but an 'adjoint' one. We also use it to provide a
| new semantics for data integration. Link:
| https://www.categoricaldata.net
| zasdffaa wrote:
| I see nothing in your link to justify what you say. Perhaps
| you can elaborate.
| wisnesky wrote:
| The way to run conjunctive SQL queries forward and backward
| is described in this paper,
| https://www.cambridge.org/core/journals/journal-of-
| functiona... , (also available on the arxiv), where they
| are referred to as query 'evaluation' and 'co-evaluation',
| respectively. We never would have been able to discover co-
| evaluation if not for category theory! The previous link
| includes this paper, and many others.
| charcircuit wrote:
| So what is coevaluation and why is it useful? Please
| don't just point at the paper again.
| franknstein wrote:
| I feel like another application which is maybe not talked about
| all that much is that knowing category theory gives you power
| to name some design pattern, google that, and tap into that
| vast mathematical knowledge that humanity already discovered.
| This becomes incredibly valuable once you become aware of how
| much you don't know. Or maybe just write that bare manimum code
| that works, idc.
|
| Oh and also when you recognize your design to be something from
| ct its probably quality. Shit code cant be described with
| simple math (simple as in all math is simple, not as in math
| that is easy to understand).
| kelseyfrog wrote:
| Category theory as it applies to programming is not dissimilar
| to learning design patterns. Some people go their whole careers
| never touching them and write perfectly fine programs. The same
| is true for category theory.
|
| Those who learn either or both, have a larger set of mental
| abstractions that largely transcend any one programming
| language. They can say, this thing and that thing share a
| common salient property through a certain abstract pattern.
| There is a certain sense of mathematical beauty in recognizing
| common patterns and mechanisms. There is also the choice of
| subtly or drastically altering one's coding style. The same
| with each, a programmer can use just the right design pattern
| in just the right place and perhaps simplify or codify a
| section so that it's easier to understand the next time around
| (or decide not to!) or they can go completely wild and over-
| pattern their code. The same applies to category theory. One
| can recognize that some section is actually a closed reduction
| and accepts any semigroup and then decide to codify this into
| the program or not.
|
| I tend to be a collector of ideas, so learning category theory
| and it's application in programming gives me all these little
| gems and ways to re-understabd code. Sometimes I use them and
| sometimes I don't, but my life is more joyful just knowing them
| regardless.
| OgAstorga wrote:
| Related discussion. https://news.ycombinator.com/item?id=33740089
| schwurb wrote:
| I find CT highly fascinating, worked through parts of 7 Sketches
| in Composability and have a functional programming background. I
| see the appeal, but I came to the conclusion that my time is
| better spent observing, learning about and designing with
| abstractions like monads, applicatives and so on rather than to
| learn the theory behind it.
|
| There seems to be a tiny handful of people that can use category
| theory as a resource to craft something relevant to software (the
| stereotypical example in my mind being Edward Kmett of Haskell
| Fame), but I am certainly not one of them, and that is not
| something that would change with learning more Category Theory
| (whatever that might mean: Proving some theorems, discovering
| more categories, ...)
|
| To the author: I am looking forward to a retrospective at a later
| time. I wish you a good journey, happy diagram-chasing!
___________________________________________________________________
(page generated 2022-11-30 23:01 UTC)