3 ms·
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 reo
by BenoitP 4y ago
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 4y agoIn 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 4y ago> 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 4y agoIt'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 4y agoMorphisms 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 4y agothat'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) 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 4y ago> seeing the category theoretical definition of monoid https://en.wikipedia.org/wiki/Monoid_(category_theory) 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 https://en.wikipedia.org/wiki/Monoid)?
- larve 4y agoMostly 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/434/730/254/651/352/original/01eedf5b15567413.jpeg https://media.hachyderm.io/media_attachments/files/109/434/7...
- hosh 4y ago> 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.
- layer8 4y agoIt’s monoids, not groups, but yeah, it‘s just knowledge about basic algebraic structures, no particular insight from category theory here.
- Koshkin 4y agoActually, 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.