14 ms·

Category Theory for Programmers (2014) [pdf]

403 points by furcyd 7y ago

furcyd 7y ago
or: https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ https://bartoszmilewski.com/2014/10/28/category-theory-for-p... or 20-video lecture series: https://www.youtube.com/playlist?list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_ https://www.youtube.com/playlist?list=PLbgaMIhjbmEnaH_LTkxLI...
- walleeee 7y ago
  Highly recommend the lecture series. He makes it accessible and fun
  - guerrilla 7y ago
    Seriously, second this. It was extremely helpful. I had both the background in programming and abstract algebra but it wasn't until this course that I was really on the path to understand what was going on with category theory.
- deleted 7y ago
  [deleted]
- a1369209993 7y ago
  Or direct[-ish] link to TFA's PDF: https://github.com/hmemcpy/milewski-ctfp-pdf/releases/download/v1.3.0/category-theory-for-programmers.pdf https://github.com/hmemcpy/milewski-ctfp-pdf/releases/downlo... -ish: since it's doing something untoward involving AWS, but the link does resolve to a actual PDF file, unlike the original submission.
Y_Y 7y ago
Worth it just for the illustrations, but this book is excellent, especially if you already know Haskell.
jesuslop 7y ago
Also released today, "Notes on Category Theory with examples from basic mathematics" by Paolo Perrone. (preprint state). arXiv:1912.10642v1
- darkkindness 7y ago
  Nice find! Abstract: > These notes were originally developed as lecture notes for a category theory course. They should be well-suited to anyone that wants to learn category theory from scratch and has a scientific mind. There is no need to know advanced mathematics, nor any of the disciplines where category theory is traditionally applied, such as algebraic geometry or theoretical computer science. The only knowledge that is assumed from the reader is linear algebra. All concepts are explained by giving concrete examples from different, non-specialized areas of mathematics (such as basic group theory, graph theory, and probability). Not every example is helpful for every reader, but hopefully every reader can find at least one helpful example per concept. The reader is encouraged to read all the examples, this way they may even learn something new about a different field. > Particular emphasis is given to the Yoneda lemma and its significance, with both intuitive explanations, detailed proofs, and specific examples. Another common theme in these notes is the relationship between categories and directed multigraphs, which is treated in detail. From the applied point of view, this shows why categorical thinking can help whenever some process is taking place on a graph. Form the pure math point of view, this can be seen as the 1-dimensional first step into the theory of simplicial sets. Finally, monads and comonads are treated on an equal footing, differently to most literature in which comonads are often overlooked as "just the dual to monads". Theorems, interpretations and concrete examples are given for monads as well as for comonads. pdf: https://arxiv.org/pdf/1912.10642 https://arxiv.org/pdf/1912.10642
dang 7y ago
A thread from 2017: https://news.ycombinator.com/item?id=14026360 https://news.ycombinator.com/item?id=14026360 A bit more: https://news.ycombinator.com/item?id=15372856 https://news.ycombinator.com/item?id=15372856 2015: https://news.ycombinator.com/item?id=9459520 https://news.ycombinator.com/item?id=9459520
SensateCreature 7y ago
Also by the same author: Applied Category Theory 2020 https://johncarlosbaez.wordpress.com/2019/12/23/applied-category-theory-2020-adjoint-school/ https://johncarlosbaez.wordpress.com/2019/12/23/applied-cate...
playing_colours 7y ago
I liked “An Invitation to Applied Category Theory“, pdf is available here: [1] It is written in a more terse, mathematical language, but it is very clear and friendly for non-mathematicians. The authors provide interesting examples of applicability. Hardcover is quite expensive, but the quality is great [2]. [1] http://math.mit.edu/~dspivak/teaching/sp18/7Sketches.pdf http://math.mit.edu/~dspivak/teaching/sp18/7Sketches.pdf [2] https://www.amazon.com/gp/aw/d/1108482295 https://www.amazon.com/gp/aw/d/1108482295
- deleted 7y ago
  [deleted]
- 74639497 7y ago
  This is probably one of the best introduction to category theory text out there now, but it isn’t exactly as friendly to the non-mathematicians as advertised. The book assumes a level of mathematical sophistication beyond what most non-math majors know and ramps up fast. The average programmer would probably get lost pretty quickly with this book.
  - throwlaplace 7y ago
    >but it isn’t exactly as friendly to the non-mathematicians as advertised. i really chafe at criticisms like this given how much effort was clearly invested by those authors in that book being readable - there are ample definitions (and clearly offset), tons of diagrams, instructive examples, solutions to many exercises, pointers to further readings, motivation and discussion. is the thing that bothers you that there's formal mathematics? it's a math book. i feel like your same criticism translated into a criticism about a programming book would be something like "this book is too unfriendly to people that don't program because it has lots of code and expects people to be able to read code". i don't understand what exactly would qualify for you as "friendly"? >category theory for the average programmer. that's because despite what people would have you believe - category theory isn't for programmers but mathematicians. so a book like that would be like a book about fluid dynamics for plumbers (read: impossible).
heinrichhartman 7y ago
Question to all CS majors, that invested in learning Category Theory: Did you have any concrete take aways from learning it? ( I have a math background, and struggle to find something concrete. Maybe I am just blind. )
- lidHanteyk 7y ago
  Yeah. I couldn't have attempted learning about certain sorts of objects like Chu spaces, posets, or topoi without category theory. After having gone through the change and categorifying my thinking, I now find category-theoretic constructions everywhere in mathematics, and I find the mathematicians who refuse to examine category theory quite insufferable. Edit: More: The connection between type theory, logic, and computation is not specious, but is part of the fabric of reality. I now can understand why chemistry -- being a linear logic -- is time-reversible, or why every DAG is a poset is a system of logic is a language of computation, or why a ring has two interlocking groups, or why social groups tend to include one big conversation and many side chats in a power-law distribution of sizes.
  - dominotw 7y ago
    > I now find category-theoretic constructions everywhere in mathematics, i think gp might have been asking about practical use in CS ( CS majors).
    - heinrichhartman 7y ago
      Yeah exactly. I am interested in practical applications for programmers. I know a thing or two about the prevalance of categories in Mathematics (https://arxiv.org/abs/1012.3121 https://arxiv.org/abs/1012.3121). I heared many people talk about Haskell, Monads and Types <=> Proof duality, but I never heard anyone saying: "I applied the Yoneda Lemma to build this API.", or "I read about Category Theory and now $CONCEPT_XYZ started making sense to me."
    - lidHanteyk 7y ago
      And CS is merely a subfield of maths. What should I say? Scott theory, domain theory, CPOs, Galois connections? The problem here is that, as usual, folks are trying to figure out what category theory is good for, but ignoring the entire point: The definitions are the important part. Once the definitions make sense, then the rest of the system makes sense. Category theory is all about the definitions, and moreover, all about coming to have the definitions at hand so that one can recognize categorical structures in practice. Or, I guess, I could take a lazy route and just say "theorems for free, those are the practical use" and be done. But it's frustrating to hear folks over and over wonder what something is good for, when they clearly aren't reading and trying to find the goodness for themselves.
reykjavik 7y ago
Watched that guy's lectures and conference talks. While it's quite interesting and educative - I still don't get the "for programmers" part of it. I don't quite get how I would jump from understanding categories, morphisms, monoids etc. to building actually better systems. There are zero practical examples in his talks. Is it because i'm not using functional languages or what am I missing here?
- rubyn00bie 7y ago
  Yeah, +100 I have this same problem in general. FWIW, the only real practical example I've seen (which has been rather serendipitous for me) is the "Seven Sketches in Compositionality" linked in the comments below applying category theory to databases. You can even play with the actual an implementation (written Java) to see some real world code here: https://github.com/CategoricalData/CQL https://github.com/CategoricalData/CQL Dunno if that helps your needs much but it was at least some kind of concrete starting point for me.
- philzook 7y ago
  Being into functional programming helps quite a bit I think. In particular, category theory seems to nest well and illuminate some complicated uses of polymorphism and continuation passing style transformations. Categories are also a useful abstraction/pattern for designing interfaces to libraries. It's sort of a more mathematically flavored version of dataflow style libraries like simulink or gnuradio diagrams and stuff. Gluing together lego blocks and building up pipelines. I have been fiddling around with a categorical interface for solve linear equations which I think is pretty neat. http://www.philipzucker.com/linear-relation-algebra-of-circuits-with-hmatrix/ http://www.philipzucker.com/linear-relation-algebra-of-circu...
- d-d 7y ago
  The practical takeaway for me is being able to see patterns and systems I never would have seen otherwise. I avoid a lot more pointless building; sometimes entire projects. The things I do end up creating come from a much deeper place of true need.
  - 7y ago
whatshisface 7y ago
Is there any point in learning category theory without first learning the things that it generalizes? I didn't see any value in learning about geometric algebra until I had learned enough about complex analysis to appreciate what it would mean to connect it with vector calculus.
- lgas 7y ago
  I think category theory generalizes pretty much everything, so that may be tough.
  - whatshisface 7y ago
    The only thing that can generalize everything is something with no structure of its own.
xvilka 7y ago
The book itself is constantly updated by the author and community, people add particular language flavors. Scala flavor[1] (along with the original Haskell one) is already part of the book, OCaml flavor[2] is being worked on and mostly finished. [1] https://github.com/hmemcpy/milewski-ctfp-pdf/releases/tag/v1.3.0 https://github.com/hmemcpy/milewski-ctfp-pdf/releases/tag/v1... [2] https://github.com/hmemcpy/milewski-ctfp-pdf/pull/201 https://github.com/hmemcpy/milewski-ctfp-pdf/pull/201
westoncb 7y ago
The clearest and most concise treatment I've come across on how Category Theory is used is Tai-Danae Bradley's "What is Applied Category Theory": https://arxiv.org/abs/1809.05923 https://arxiv.org/abs/1809.05923 (It's a 50 page PDF) Unfortunately the examples aren't within CS, but at least for me personally, seeing it clearly applied in any context was the most important thing. It may be a good pre-req for looking at (or conjuring up your own) more detailed applications within CS specifically. Also, if you like that, Tai-Danae Bradley has more writing at: https://www.math3ma.com/ https://www.math3ma.com/
- knzhou 7y ago
  I'm familiar with the applications here, and I've never found them compelling. They amount to taking things we already understand perfectly well (chemical reactions, written in terms of differential equations or visualized in terms of graphs) and draping huge amounts of formalism around them. The "theorems" they then prove do not provide any new insight -- they're only called theorems because the excess formalism makes completely trivial things hard to see! For example, the main theorem of one of Baez's very long papers is: > There is a symmetric monoidal functor from the category Petri to the category Dynam. When you plug in the hundred relevant definitions, you find that this is literally just the statement that you can specify a chemical reaction network in terms of differential equations, or pictorially in terms of graphs where the edges represent reactions, which is a standard thing taught in ordinary chemistry classes. The language of categories is not achieving anything here but obfuscation. Category theory is only good when there's a very rich preexisting mathematical structure, so that introducing it simplifies things. That usually isn't true in science.
  - westoncb 7y ago
    I think you may be missing something here. > The "theorems" they then prove do not provide any new insight Knowing that you can model reaction networks using categorical concepts may not provide new insights IF you have no deep familiarity with those concepts—but if you do, then knowing there is a "symmetric monoidal functor from the category Petri to the category Dynam" is a richly useful piece of information. It's probably more accurate to say that the amount of new insight conferred is proportional to your familiarity with the categorical concepts. And yes, it's true the concepts are 'just' being translated into a new language—but if this new language is extremely general, applicable to a wide range of domains, then: 1) You can build a set of skills and knowledge related to concepts in this general language, which become automatically applicable to a wide range of domains (when their concepts are imported into the language). 2) It's possible to build 'machinery' (i.e. theorems or software) which deals with / operates on (representations of) concepts from this very general language—so once again, if you can translate some concept from domain X into e.g a symmetric monoidal category, now your general machinery can operate on things from domain X (which it was built with no awareness of). Additionally, at least in Bradley's paper, the point wasn't to prove new things about e.g. reaction networks; instead it was to illustrate a method. To be more specific she is showing how "functorial semantics" can be applied in this context, using Petri nets as the syntax and dynamical systems as the semantics. From there the categorical classification of these objects gives us guarantees on their behavior under composition (the utility of which I assume is clear). I'm not sure in the context of reaction networks whether modeling the system with compositionality guarantees and a clean mapping between graph representation and differential equations gives scientists something new or not—but the illustration of this method is done clearly, and the generality of the method is enormous. And maybe I'm also missing something. I'm not a mathematician, but that's how the situation looks to me.
philzook 7y ago
People who like this may also be interested in the awesome applied category theory list https://github.com/statebox/awesome-applied-ct https://github.com/statebox/awesome-applied-ct
- philzook 7y ago
  And Conal Elliott's Compiling to Categories, which I've seen discussed here before http://conal.net/papers/compiling-to-categories/ http://conal.net/papers/compiling-to-categories/
CTmystery 7y ago
Can someone please explain to me the excitement for category theory in this forum? I've gone through the first 10 chapters + exercises of this book, and truth be told the content is interesting but the ROI is low for programming (FWIW I started this book as part of a study group in a large unicorn co, and after approximately one month I was the only person left grinding through the exercises, hoping for some payoff). It's cool that I know what a functor is, I guess, but where others tout CT as unlocking a higher level view of programming, all I see are little curiosities (when you do X you are really doing Y, isn't that cool!?). I've heard it said that CT's true power comes as a "refactorer" for what would otherwise be complicated proofs. I.E. we discovered a new tool to make proofs that already existed more elegant. That's cool that it has a use! Does this somehow extend to programming? I don't mean to sound like a grouch, but I'm genuinely baffled by the level of excitement around this topic. If you're looking to scratch a math itch, ML has plenty of opportunities to hobby some math while advancing your career and marketability. For programming in general, there are tens of topics I would pick before reaching for this, with major immediate payoff to our occupation as programmers. Finally, after going through 10 chapters I skipped to the end to see if there was some culminating breakthrough that we were striving towards... and I found more definitions stacked upon other definitions. I suppose memorizing all these definitions is supposed to give me a different mental model about programming. Is that right? I'll quote here the first line of the Analects, "Isn't it a pleasure to study and practice what you have learned?". This is what I look for in studying any topic: something that gives me joy to put into use. In the best cases it gives me a feeling of a super power - something that was previously impossible or extremely difficult is now elegant and clear. Can CT offer that in any way to programming? -Sincerly, Guy that doesn't get it, but wants to
- zug_zug 7y ago
  As a functional programmer myself, I have the same confusion. As best I can tell, category-theory a cargo-cult thing ("I want to look like the type of engineer who CARES about monoids [because if I use words you don't know I'm smart]" much in the same way hipsters claimed vinyl sounds better). I'd like to be wrong about this, but I've already met a handful of "phonies" who rant and rave about this stuff, but when I ask them "How does labeling an array a monad help me?" or even "Is a hash-map a monad?" they are completely stuck.
auggierose 7y ago
I very much like: "Sets for Mathematics", which I currently read and which finally clicks with me. I always found expositions of category theory tiring in that it bombarded me with trivialities and examples that were kind of obvious. Instead, "Sets for Mathematics" describes one particular and probably the most familiar and important category, the category of sets, and I very much like this fresh look at sets.
smcl 7y ago
There's a lecture series he did if anyone's interested: https://www.youtube.com/watch?v=I8LbkfSSR58 https://www.youtube.com/watch?v=I8LbkfSSR58 I must say that there is a slight Tommy Wiseau energy about the guy, but that's no bad thing :-)
jokoon 7y ago
I wish some subjects of mathematics could be summarized in a TLDR fashion. It would make it much more interesting as an introduction. I remember that we used to write very small sheets of formulas and other memos to condense a class into a much shorter thing. Simple.wikipedia.org seems to somewhat be that. I have always liked math, but I can see why people don't like math or get interested in math. The literature is exhaustive, unnecessary long, and just too arcane. I will always be frustrated with the image of mathematics and how laymen often say "math is not for me", but sometimes I can understand why.
mathgenius 7y ago
Here's a really great introduction to CT for the non-mathematically inclined: Lawvere and Schanuel. "Conceptual mathematics: a first introduction to categories." Cambridge University Press, 2009. The authors are two of the "founders" of the subject, so don't be fooled by the elementary appearance of this book.
wellpast 7y ago
Started reading this and was disappointed to find the same disingenuous claims about strong static type systems. I say disingenuous because the people that espouse these beliefs seem to have a minimum modicum of intelligence and do or would certainly (after a moment of reflection) certainly realize their fallacy: > The only serious argument I hear against strong static type check- ing is that it might eliminate some programs that are semantically cor- rect. In practice, this happens extremely rarely and, in any case, every language provides some kind of a backdoor to bypass the type sys- tem when that’s really necessary. This is patently false. Port a correct dynamically typed program to Haskell and it will certainly fail until you satisfy the type checker through no small extraneous effort. And this is not a theoretical matter; it is an enormous cost to the programmer that is not there in weaker or non- typed systems. It is a certainty that type systems ask for far more than is needed to produce correctness. Anyone who tries to dodge this obvious and fundamental truth is operating off of a religious not rational commitment to defending their type system. Note that I am not saying the type system doesn't give you something back but it certainly comes with a inherent cost over alternatives. > Another argument I hear a lot is that dealing with types imposes too much burden on the programmer. I could sympathize with this sen- timent after having to write a few declarations of iterators in C++ my- self, except that there is a technology called type inference that lets the compiler deduce most of the types This is the most heinous and sad lie. Type inference changes nothing. The types are there even if you don't have to type them in and they are significantly constraining your set of accepted programs. I've heard this response before from seemingly smart static typers. I just can't believe a smart person would not see the obvious emptiness of this claim. There is no way anyone would think that having to type characters is the exclusive cost of static typing that inference suddenly whisks away. I want to buy into the strong static typist's promise of utopia but I have yet to meet a static typist enthusiast that doesn't parlay in these lies, wittingly or unwittingly. Because of this I have a serious suspicion that there is nothing else to stand on and that strong static typing is simply a case of the Emperor's New Clothes. Prove me wrong.
- tome 7y ago
  > > The only serious argument I hear against strong static type check- ing is that it might eliminate some programs that are semantically cor- rect. In practice, this happens extremely rarely and, in any case, every language provides some kind of a backdoor to bypass the type sys- tem when that’s really necessary. > This is patently false. Port a correct dynamically typed program to Haskell and it will certainly fail until you satisfy the type checker through no small extraneous effort. And this is not a theoretical matter; it is an enormous cost to the programmer that is not there in weaker or non- typed systems. It seems like this disagreement should be easy to resolve. You are saying that it's hard to satisfy the type checker when porting a dynamically-typed program; OP says this happens very rarely. Therefore you can easily disprove OP's claim by providing some examples that happen commonly in practice. Provide them, please! > There is no way anyone would think that having to type characters is the exclusive cost of static typing that inference suddenly whisks away. OP is not claiming that the benefit of type inference is that it automatically "types characters". > I have yet to meet a static typist enthusiast that doesn't parlay in these lies I don't think it's necessary to bring a moral dimension into this discussion. Let's keep it technical please.

403 points by furcyd 7y ago

or: https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ https://bartoszmilewski.com/2014/10/28/category-theory-for-p... or 20-video lecture series: https://www.youtube.com/playlist?list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_ https://www.youtube.com/playlist?list=PLbgaMIhjbmEnaH_LTkxLI...

walleeee 7y ago
Highly recommend the lecture series. He makes it accessible and fun
- guerrilla 7y ago
  Seriously, second this. It was extremely helpful. I had both the background in programming and abstract algebra but it wasn't until this course that I was really on the path to understand what was going on with category theory.
deleted 7y ago
[deleted]
a1369209993 7y ago
Or direct[-ish] link to TFA's PDF: https://github.com/hmemcpy/milewski-ctfp-pdf/releases/download/v1.3.0/category-theory-for-programmers.pdf https://github.com/hmemcpy/milewski-ctfp-pdf/releases/downlo... -ish: since it's doing something untoward involving AWS, but the link does resolve to a actual PDF file, unlike the original submission.

Y_Y 7y ago

Worth it just for the illustrations, but this book is excellent, especially if you already know Haskell.

jesuslop 7y ago

Also released today, "Notes on Category Theory with examples from basic mathematics" by Paolo Perrone. (preprint state). arXiv:1912.10642v1

darkkindness 7y ago
Nice find! Abstract: > These notes were originally developed as lecture notes for a category theory course. They should be well-suited to anyone that wants to learn category theory from scratch and has a scientific mind. There is no need to know advanced mathematics, nor any of the disciplines where category theory is traditionally applied, such as algebraic geometry or theoretical computer science. The only knowledge that is assumed from the reader is linear algebra. All concepts are explained by giving concrete examples from different, non-specialized areas of mathematics (such as basic group theory, graph theory, and probability). Not every example is helpful for every reader, but hopefully every reader can find at least one helpful example per concept. The reader is encouraged to read all the examples, this way they may even learn something new about a different field. > Particular emphasis is given to the Yoneda lemma and its significance, with both intuitive explanations, detailed proofs, and specific examples. Another common theme in these notes is the relationship between categories and directed multigraphs, which is treated in detail. From the applied point of view, this shows why categorical thinking can help whenever some process is taking place on a graph. Form the pure math point of view, this can be seen as the 1-dimensional first step into the theory of simplicial sets. Finally, monads and comonads are treated on an equal footing, differently to most literature in which comonads are often overlooked as "just the dual to monads". Theorems, interpretations and concrete examples are given for monads as well as for comonads. pdf: https://arxiv.org/pdf/1912.10642 https://arxiv.org/pdf/1912.10642

dang 7y ago

A thread from 2017: https://news.ycombinator.com/item?id=14026360 https://news.ycombinator.com/item?id=14026360 A bit more: https://news.ycombinator.com/item?id=15372856 https://news.ycombinator.com/item?id=15372856 2015: https://news.ycombinator.com/item?id=9459520 https://news.ycombinator.com/item?id=9459520

SensateCreature 7y ago

Also by the same author: Applied Category Theory 2020 https://johncarlosbaez.wordpress.com/2019/12/23/applied-category-theory-2020-adjoint-school/ https://johncarlosbaez.wordpress.com/2019/12/23/applied-cate...

playing_colours 7y ago

I liked “An Invitation to Applied Category Theory“, pdf is available here: [1] It is written in a more terse, mathematical language, but it is very clear and friendly for non-mathematicians. The authors provide interesting examples of applicability. Hardcover is quite expensive, but the quality is great [2]. [1] http://math.mit.edu/~dspivak/teaching/sp18/7Sketches.pdf http://math.mit.edu/~dspivak/teaching/sp18/7Sketches.pdf [2] https://www.amazon.com/gp/aw/d/1108482295 https://www.amazon.com/gp/aw/d/1108482295

deleted 7y ago
[deleted]
74639497 7y ago
This is probably one of the best introduction to category theory text out there now, but it isn’t exactly as friendly to the non-mathematicians as advertised. The book assumes a level of mathematical sophistication beyond what most non-math majors know and ramps up fast. The average programmer would probably get lost pretty quickly with this book.
- throwlaplace 7y ago
  >but it isn’t exactly as friendly to the non-mathematicians as advertised. i really chafe at criticisms like this given how much effort was clearly invested by those authors in that book being readable - there are ample definitions (and clearly offset), tons of diagrams, instructive examples, solutions to many exercises, pointers to further readings, motivation and discussion. is the thing that bothers you that there's formal mathematics? it's a math book. i feel like your same criticism translated into a criticism about a programming book would be something like "this book is too unfriendly to people that don't program because it has lots of code and expects people to be able to read code". i don't understand what exactly would qualify for you as "friendly"? >category theory for the average programmer. that's because despite what people would have you believe - category theory isn't for programmers but mathematicians. so a book like that would be like a book about fluid dynamics for plumbers (read: impossible).

heinrichhartman 7y ago

Question to all CS majors, that invested in learning Category Theory: Did you have any concrete take aways from learning it? ( I have a math background, and struggle to find something concrete. Maybe I am just blind. )

lidHanteyk 7y ago
Yeah. I couldn't have attempted learning about certain sorts of objects like Chu spaces, posets, or topoi without category theory. After having gone through the change and categorifying my thinking, I now find category-theoretic constructions everywhere in mathematics, and I find the mathematicians who refuse to examine category theory quite insufferable. Edit: More: The connection between type theory, logic, and computation is not specious, but is part of the fabric of reality. I now can understand why chemistry -- being a linear logic -- is time-reversible, or why every DAG is a poset is a system of logic is a language of computation, or why a ring has two interlocking groups, or why social groups tend to include one big conversation and many side chats in a power-law distribution of sizes.
- dominotw 7y ago
  > I now find category-theoretic constructions everywhere in mathematics, i think gp might have been asking about practical use in CS ( CS majors).
  - heinrichhartman 7y ago
    Yeah exactly. I am interested in practical applications for programmers. I know a thing or two about the prevalance of categories in Mathematics (https://arxiv.org/abs/1012.3121 https://arxiv.org/abs/1012.3121). I heared many people talk about Haskell, Monads and Types <=> Proof duality, but I never heard anyone saying: "I applied the Yoneda Lemma to build this API.", or "I read about Category Theory and now $CONCEPT_XYZ started making sense to me."
  - lidHanteyk 7y ago
    And CS is merely a subfield of maths. What should I say? Scott theory, domain theory, CPOs, Galois connections? The problem here is that, as usual, folks are trying to figure out what category theory is good for, but ignoring the entire point: The definitions are the important part. Once the definitions make sense, then the rest of the system makes sense. Category theory is all about the definitions, and moreover, all about coming to have the definitions at hand so that one can recognize categorical structures in practice. Or, I guess, I could take a lazy route and just say "theorems for free, those are the practical use" and be done. But it's frustrating to hear folks over and over wonder what something is good for, when they clearly aren't reading and trying to find the goodness for themselves.

reykjavik 7y ago

Watched that guy's lectures and conference talks. While it's quite interesting and educative - I still don't get the "for programmers" part of it. I don't quite get how I would jump from understanding categories, morphisms, monoids etc. to building actually better systems. There are zero practical examples in his talks. Is it because i'm not using functional languages or what am I missing here?

rubyn00bie 7y ago
Yeah, +100 I have this same problem in general. FWIW, the only real practical example I've seen (which has been rather serendipitous for me) is the "Seven Sketches in Compositionality" linked in the comments below applying category theory to databases. You can even play with the actual an implementation (written Java) to see some real world code here: https://github.com/CategoricalData/CQL https://github.com/CategoricalData/CQL Dunno if that helps your needs much but it was at least some kind of concrete starting point for me.
philzook 7y ago
Being into functional programming helps quite a bit I think. In particular, category theory seems to nest well and illuminate some complicated uses of polymorphism and continuation passing style transformations. Categories are also a useful abstraction/pattern for designing interfaces to libraries. It's sort of a more mathematically flavored version of dataflow style libraries like simulink or gnuradio diagrams and stuff. Gluing together lego blocks and building up pipelines. I have been fiddling around with a categorical interface for solve linear equations which I think is pretty neat. http://www.philipzucker.com/linear-relation-algebra-of-circuits-with-hmatrix/ http://www.philipzucker.com/linear-relation-algebra-of-circu...
d-d 7y ago
The practical takeaway for me is being able to see patterns and systems I never would have seen otherwise. I avoid a lot more pointless building; sometimes entire projects. The things I do end up creating come from a much deeper place of true need.
- 7y ago

whatshisface 7y ago

Is there any point in learning category theory without first learning the things that it generalizes? I didn't see any value in learning about geometric algebra until I had learned enough about complex analysis to appreciate what it would mean to connect it with vector calculus.

lgas 7y ago
I think category theory generalizes pretty much everything, so that may be tough.
- whatshisface 7y ago
  The only thing that can generalize everything is something with no structure of its own.

xvilka 7y ago

The book itself is constantly updated by the author and community, people add particular language flavors. Scala flavor[1] (along with the original Haskell one) is already part of the book, OCaml flavor[2] is being worked on and mostly finished. [1] https://github.com/hmemcpy/milewski-ctfp-pdf/releases/tag/v1.3.0 https://github.com/hmemcpy/milewski-ctfp-pdf/releases/tag/v1... [2] https://github.com/hmemcpy/milewski-ctfp-pdf/pull/201 https://github.com/hmemcpy/milewski-ctfp-pdf/pull/201

westoncb 7y ago

The clearest and most concise treatment I've come across on how Category Theory is used is Tai-Danae Bradley's "What is Applied Category Theory": https://arxiv.org/abs/1809.05923 https://arxiv.org/abs/1809.05923 (It's a 50 page PDF) Unfortunately the examples aren't within CS, but at least for me personally, seeing it clearly applied in any context was the most important thing. It may be a good pre-req for looking at (or conjuring up your own) more detailed applications within CS specifically. Also, if you like that, Tai-Danae Bradley has more writing at: https://www.math3ma.com/ https://www.math3ma.com/

knzhou 7y ago
I'm familiar with the applications here, and I've never found them compelling. They amount to taking things we already understand perfectly well (chemical reactions, written in terms of differential equations or visualized in terms of graphs) and draping huge amounts of formalism around them. The "theorems" they then prove do not provide any new insight -- they're only called theorems because the excess formalism makes completely trivial things hard to see! For example, the main theorem of one of Baez's very long papers is: > There is a symmetric monoidal functor from the category Petri to the category Dynam. When you plug in the hundred relevant definitions, you find that this is literally just the statement that you can specify a chemical reaction network in terms of differential equations, or pictorially in terms of graphs where the edges represent reactions, which is a standard thing taught in ordinary chemistry classes. The language of categories is not achieving anything here but obfuscation. Category theory is only good when there's a very rich preexisting mathematical structure, so that introducing it simplifies things. That usually isn't true in science.
- westoncb 7y ago
  I think you may be missing something here. > The "theorems" they then prove do not provide any new insight Knowing that you can model reaction networks using categorical concepts may not provide new insights IF you have no deep familiarity with those concepts—but if you do, then knowing there is a "symmetric monoidal functor from the category Petri to the category Dynam" is a richly useful piece of information. It's probably more accurate to say that the amount of new insight conferred is proportional to your familiarity with the categorical concepts. And yes, it's true the concepts are 'just' being translated into a new language—but if this new language is extremely general, applicable to a wide range of domains, then: 1) You can build a set of skills and knowledge related to concepts in this general language, which become automatically applicable to a wide range of domains (when their concepts are imported into the language). 2) It's possible to build 'machinery' (i.e. theorems or software) which deals with / operates on (representations of) concepts from this very general language—so once again, if you can translate some concept from domain X into e.g a symmetric monoidal category, now your general machinery can operate on things from domain X (which it was built with no awareness of). Additionally, at least in Bradley's paper, the point wasn't to prove new things about e.g. reaction networks; instead it was to illustrate a method. To be more specific she is showing how "functorial semantics" can be applied in this context, using Petri nets as the syntax and dynamical systems as the semantics. From there the categorical classification of these objects gives us guarantees on their behavior under composition (the utility of which I assume is clear). I'm not sure in the context of reaction networks whether modeling the system with compositionality guarantees and a clean mapping between graph representation and differential equations gives scientists something new or not—but the illustration of this method is done clearly, and the generality of the method is enormous. And maybe I'm also missing something. I'm not a mathematician, but that's how the situation looks to me.

philzook 7y ago

People who like this may also be interested in the awesome applied category theory list https://github.com/statebox/awesome-applied-ct https://github.com/statebox/awesome-applied-ct

philzook 7y ago
And Conal Elliott's Compiling to Categories, which I've seen discussed here before http://conal.net/papers/compiling-to-categories/ http://conal.net/papers/compiling-to-categories/

CTmystery 7y ago

Can someone please explain to me the excitement for category theory in this forum? I've gone through the first 10 chapters + exercises of this book, and truth be told the content is interesting but the ROI is low for programming (FWIW I started this book as part of a study group in a large unicorn co, and after approximately one month I was the only person left grinding through the exercises, hoping for some payoff). It's cool that I know what a functor is, I guess, but where others tout CT as unlocking a higher level view of programming, all I see are little curiosities (when you do X you are really doing Y, isn't that cool!?). I've heard it said that CT's true power comes as a "refactorer" for what would otherwise be complicated proofs. I.E. we discovered a new tool to make proofs that already existed more elegant. That's cool that it has a use! Does this somehow extend to programming? I don't mean to sound like a grouch, but I'm genuinely baffled by the level of excitement around this topic. If you're looking to scratch a math itch, ML has plenty of opportunities to hobby some math while advancing your career and marketability. For programming in general, there are tens of topics I would pick before reaching for this, with major immediate payoff to our occupation as programmers. Finally, after going through 10 chapters I skipped to the end to see if there was some culminating breakthrough that we were striving towards... and I found more definitions stacked upon other definitions. I suppose memorizing all these definitions is supposed to give me a different mental model about programming. Is that right? I'll quote here the first line of the Analects, "Isn't it a pleasure to study and practice what you have learned?". This is what I look for in studying any topic: something that gives me joy to put into use. In the best cases it gives me a feeling of a super power - something that was previously impossible or extremely difficult is now elegant and clear. Can CT offer that in any way to programming? -Sincerly, Guy that doesn't get it, but wants to

zug_zug 7y ago
As a functional programmer myself, I have the same confusion. As best I can tell, category-theory a cargo-cult thing ("I want to look like the type of engineer who CARES about monoids [because if I use words you don't know I'm smart]" much in the same way hipsters claimed vinyl sounds better). I'd like to be wrong about this, but I've already met a handful of "phonies" who rant and rave about this stuff, but when I ask them "How does labeling an array a monad help me?" or even "Is a hash-map a monad?" they are completely stuck.

auggierose 7y ago

I very much like: "Sets for Mathematics", which I currently read and which finally clicks with me. I always found expositions of category theory tiring in that it bombarded me with trivialities and examples that were kind of obvious. Instead, "Sets for Mathematics" describes one particular and probably the most familiar and important category, the category of sets, and I very much like this fresh look at sets.

smcl 7y ago

There's a lecture series he did if anyone's interested: https://www.youtube.com/watch?v=I8LbkfSSR58 https://www.youtube.com/watch?v=I8LbkfSSR58 I must say that there is a slight Tommy Wiseau energy about the guy, but that's no bad thing :-)

jokoon 7y ago

I wish some subjects of mathematics could be summarized in a TLDR fashion. It would make it much more interesting as an introduction. I remember that we used to write very small sheets of formulas and other memos to condense a class into a much shorter thing. Simple.wikipedia.org seems to somewhat be that. I have always liked math, but I can see why people don't like math or get interested in math. The literature is exhaustive, unnecessary long, and just too arcane. I will always be frustrated with the image of mathematics and how laymen often say "math is not for me", but sometimes I can understand why.

mathgenius 7y ago

Here's a really great introduction to CT for the non-mathematically inclined: Lawvere and Schanuel. "Conceptual mathematics: a first introduction to categories." Cambridge University Press, 2009. The authors are two of the "founders" of the subject, so don't be fooled by the elementary appearance of this book.

wellpast 7y ago

Started reading this and was disappointed to find the same disingenuous claims about strong static type systems. I say disingenuous because the people that espouse these beliefs seem to have a minimum modicum of intelligence and do or would certainly (after a moment of reflection) certainly realize their fallacy: > The only serious argument I hear against strong static type check- ing is that it might eliminate some programs that are semantically cor- rect. In practice, this happens extremely rarely and, in any case, every language provides some kind of a backdoor to bypass the type sys- tem when that’s really necessary. This is patently false. Port a correct dynamically typed program to Haskell and it will certainly fail until you satisfy the type checker through no small extraneous effort. And this is not a theoretical matter; it is an enormous cost to the programmer that is not there in weaker or non- typed systems. It is a certainty that type systems ask for far more than is needed to produce correctness. Anyone who tries to dodge this obvious and fundamental truth is operating off of a religious not rational commitment to defending their type system. Note that I am not saying the type system doesn't give you something back but it certainly comes with a inherent cost over alternatives. > Another argument I hear a lot is that dealing with types imposes too much burden on the programmer. I could sympathize with this sen- timent after having to write a few declarations of iterators in C++ my- self, except that there is a technology called type inference that lets the compiler deduce most of the types This is the most heinous and sad lie. Type inference changes nothing. The types are there even if you don't have to type them in and they are significantly constraining your set of accepted programs. I've heard this response before from seemingly smart static typers. I just can't believe a smart person would not see the obvious emptiness of this claim. There is no way anyone would think that having to type characters is the exclusive cost of static typing that inference suddenly whisks away. I want to buy into the strong static typist's promise of utopia but I have yet to meet a static typist enthusiast that doesn't parlay in these lies, wittingly or unwittingly. Because of this I have a serious suspicion that there is nothing else to stand on and that strong static typing is simply a case of the Emperor's New Clothes. Prove me wrong.

tome 7y ago
> > The only serious argument I hear against strong static type check- ing is that it might eliminate some programs that are semantically cor- rect. In practice, this happens extremely rarely and, in any case, every language provides some kind of a backdoor to bypass the type sys- tem when that’s really necessary. > This is patently false. Port a correct dynamically typed program to Haskell and it will certainly fail until you satisfy the type checker through no small extraneous effort. And this is not a theoretical matter; it is an enormous cost to the programmer that is not there in weaker or non- typed systems. It seems like this disagreement should be easy to resolve. You are saying that it's hard to satisfy the type checker when porting a dynamically-typed program; OP says this happens very rarely. Therefore you can easily disprove OP's claim by providing some examples that happen commonly in practice. Provide them, please! > There is no way anyone would think that having to type characters is the exclusive cost of static typing that inference suddenly whisks away. OP is not claiming that the benefit of type inference is that it automatically "types characters". > I have yet to meet a static typist enthusiast that doesn't parlay in these lies I don't think it's necessary to bring a moral dimension into this discussion. Let's keep it technical please.