Category Theory Illustrated: Logic (2021)

(abuseofnotation.github.io)

252 points | by boris_m 8 months ago ago

30 comments

  • Krei-se 8 months ago

    This is such a great page, i love it and came across it multiple times while studying the matter.

    I still would vote to learn it from Milewski though. Learning this is a journey and the author of ct-illustrated is, i think, still in the middle of it.

    Milewski has made that trip multiple times already. The book and his blog are great places.

    https://github.com/hmemcpy/milewski-ctfp-pdf Book https://bartoszmilewski.com/2014/10/28/category-theory-for-p... Blog

    • codethief 8 months ago

      > I still would vote to learn it from Milewski though

      I've read the first dozen chapters of Milewski so far, and while I really enjoyed the first couple chapters, his style of not giving precise definitions or statements, nor using precise notation becomes really annoying after a while and makes the book practically useless as a reference. He seems to think everything is easier to understand when it's written in lighthearted, imprecise prose.

      No, not all.¹

      ¹) https://news.ycombinator.com/item?id=41756286

    • revskill 8 months ago

      I don't understand what bartoszmilewski talked about, so his book seems useless to me. But at work i use category theory for all of my domain model.

  • psychoslave 8 months ago

    Discussed at the time, though with an other URL:

    https://news.ycombinator.com/item?id=28660131 (2 comments)

    https://news.ycombinator.com/item?id=28660157 (112 comments)

  • roughly 8 months ago

    Starting from the beginning of the book, I came across this gem of a sentence, when speaking about math compared to science or engineering:

    > Because of this, mathematicians are in a weird and, I’d say, unique position of always having to defend what they do with respect to its value for other disciplines. I again stress that this is something that would be considered absurd when it comes to any other discipline.

    I think this is a concept that anyone who studied anything that does not directly lead to monetizable outcomes can relate to, but it's nice to hear even those whose gifts skew to the numeric also have to contend with "Milton Friedman's Razor".

    • DiscourseFan 8 months ago

      Its a good thing, then, that so many projects in "cultural studies" are actually funded directly by the DoD and the State Department. Hell, the entirety of "post-colonial" studies today is nothing more than the backend of US soft-power (and, presumably, if a war breaks out, hard power as well).

  • overhead4075 8 months ago

    Circles in circles doesn't really scale well if the inner circles are always vertically centered.

  • tezka 8 months ago

    Any body can share a success story of using category theory gainfully to any CS/SWE problem that couldn't have been solved without? No Monads isn't one, you would invent it naturally when the situation calls for it. I spent a year studying in grad school and I ultimately abandoned it.

    • whatshisface 8 months ago

      There are no problems that can't be modeled without category theory. One of the most foundational category theorems is the Yoneda Lemma, which directly states that any problem phrased in the language of categories can be translated to the language of sets and functions. The same is true of every mathematical object with a definition in terms of sets - you could always replace the name with its definition.

      The contribution of category theoretic language to the implicit framework of a theory can't be larger than the definition of a category, which is very small. You could be asking "why use groups when sets with an associative operation exhibiting closure, an identity and an inverse are more approachable?" Abstract algebra is based on a library of definitions that refer to types of operations on sets that are simple enough to be common. A tool or a technique are not the kind of things you can find in a definition.

      Rings, vector spaces and modules get a sort of instant acceptance for what they are, but categories have believers and disbelievers. I am curious about how that can happen.

    • j2kun 8 months ago

      The closest I know of is the work on UMAP. I interviewed Leland McInnes who explained to me in detail how category theory was a big part of helping him connect the dots, even though the final result does not strictly need it in the actual code. Given the relative improvement over the previous state of the art (t-SNE), it's the only example that really makes me reconsider my poo-pooing the way category theory is discussed in software.

      https://arxiv.org/abs/1802.03426

    • bgavran 8 months ago

      "Anybody can share a sucess story of using a car to go places I couldn't have gone on foot"?

      CT is a language and a tool, meaning anything you can say in the language of CT you can say in other languages.

      Like cars, if you learn how to drive it (and this one has a very steep learning curve), it gets you places faster, but you there's in principle nothing stopping you from going there walking, i.e. without specifically referring to any CT concepts.

    • rnhmjoj 8 months ago

      Reformulating something you already understanding in a more general framework can give more insight into what it really means, isolate the essence from messy details. From my very limited understanding of it, characterising an object with universal properties is an important part of category theory.

      Another practical utility of category theory is providing a common language for computer scientists, mathematicians and physicists to speak. You can imagine collaboration is not easy when everyone calls the same pattern with different names with slightly incompatible definitions that requires you to understand unfamiliar theories.

    • carlskevin 8 months ago

      At the Topos Institute we're working on some new software that we're hoping will be a lot more transparent to people who haven't drunk the CT Kool-Aid yet; the current pre-alpha is mainly for systems dynamics modeling but the category-theoretic basis is, to my mind, indispensable for the range of tasks we're targeting. I'd be very happy to hear anybody's thoughts! https://topos.site/blog/2024-10-02-introducing-catcolab/

    • Krei-se 8 months ago

      You are very close. CT is about structure, not which problem this structure solves. Compilers are closest in what i can think of in this regard: They don't resolve one problem domain, but many. Which one you apply it on is up to you.

      One tool for one job is a simple rule you can adapt as a systems architect allowing you to build clear structure for the problem domain you come across. esbuild comes to mind as an example - the job was solved before, but keeping one purpose in mind and writing it from scratch solves the problem WAAAY faster.

      So no, no problem is solved inside the domain of product software development, but outside of it, you as a developer can (if you want and for speed) derive any structure from the absurd function instead of combining foreign frameworks.

    • dambi0 8 months ago

      Determining whether something is useful because it’s the only way that a problem can be solved is quite a high bar.

      We could say the same about computers in general.

      Admittedly even with a less stringent criteria I don’t have any examples. So I understand your point

    • jiggawatts 8 months ago

      I've heard of some database migration tooling that uses category theory to compute robust data transformations that are automatically composable to achieve the desired outcome.

      There has been seen some research into the fundamentals of machine learning, using category theory approaches for computing the compositions of transformations of expressions. E.g.: simultaneously computing a gradient, the "bounding box" of the error, and other similar derivatives to improve the robustness of gradient descent.

    • 8 months ago
      [deleted]
    • YetAnotherNick 8 months ago

      > any CS/SWE problem that couldn't have been solved without?

      Any computing problem that could be solved with category could be solved by brainfuck.

    • javajosh 8 months ago

      My cynical understanding of category theory is that it's the mathy Peter principle: category theory is when meta mathematics starts to lose all value. Except two professional mathematicians, of course, in which case the value is almost purely economic. "He who is employed to teach something that cannot be understood will always have a job."

    • umanwizard 8 months ago

      It is really not useful at all in software engineering except possibly in some very niche case.

    • platz 8 months ago

      abstractions never solve problems that couldn't have been solved without them.

    • funktour 8 months ago

      [dead]

  • ogogmad 8 months ago

    I think category theory is useful, but not yet in computing.

    I suspect it's hard if you don't really need it for anything. Do you really need to understand universal properties and adjoint functors and the Yoneda lemma? If you don't, you'll struggle to learn what those are.

    Interestingly, experience in functional programming can help you understand category theory, but not so much the other way round. For instance: Parametric polymorphism gives you intuition for natural transformations. And natural transformations are central to every application of category theory.

    The convincing applications of category theory are very mathematical. You'll find them in algebraic topology, representation theory, algebraic geometry, and non-classical logic.

  • cubefox 8 months ago

    There is an error:

    > Modus ponens is a proposition that is composed of two other propositions (which here we denote A and B) and it states that if proposition A is true and also if proposition (A --> B) is true (that is if A implies B), then B is true as well. For example, if we know that “Socrates is a human” and that “humans are mortal” (or “being human implies being mortal”), we also know that “Socrates is mortal.”

    This example is not an instance of Modus ponens (a rule of propositional logic), it is rather a categorical syllogism, which require predicate logic.

  • jawjay 8 months ago

    This says “Logic is the science of the possible” but wouldn’t logic be the science of the definite? I mean the whole point is to be able to definitely say what is or isn’t valid, definitely.

  • 8 months ago
    [deleted]
  • User23 8 months ago

    Interesting diagrammatic notation. Does the author give inference rules for truth preserving transformations of diagrams?

  • Krei-se 8 months ago

    Oh i just realized the blog author himself created this post: Boris we love you! Best of luck on your journey and thanks for your work!

    • boris_m 8 months ago

      Touching. Thanks. And feel free to create some Github issues or write to me if you have some feedback.