5 ms·

The concepts are intuitive enough, and make sense. But I don’t see what non-trivial insights this gives us. I found the talk frustratingly vague. After all the

The concepts are intuitive enough, and make sense. But I don’t see what non-trivial insights this gives us. I found the talk frustratingly vague. After all the hard work of setting up categories/operads in an example, the talk moved on without using them to do anything interesting.

lidHanteyk 7y ago
Here is one non-trivial insight: Every formal logic corresponds to a category. When we do logical deduction, we have facts and rules. We can apply rules to facts to get more facts. More specifically, formal logic is built from situations where we have some fact P, some rule P => Q, and some conclusion Q. In a category, we have objects and arrows. We can imagine arrows as mapping one object to another, or sending one object to another. We might have objects P and Q, and an arrow f : P -> Q relating them. The connection continues. We can take multiple rules in logic and apply them sequentially, building a proof tree; we can take multiple arrows in a category and compose them sequentially, building a path. In some logics, there is an idea of ex falso quodlibet, or from the false fact, anything can be proven; similarly, in some categories, there are initial objects, which come with arrows from the initial object to every other object. Just like how logical formalism eventually removed the possibility that logic is non-mathematical, category theory removes the possibility that logic is unstructured. Logic is actually incredibly highly structured, and those structures happen to coincide with structures in other parts of maths and physics.
- jiggawatts 7y ago
  Again though, how do I use this to solve everyday problems? I've seen some vaguely cool stuff done with Category theory in Haskell, e.g.: composable tree parsing and traversal, but I've never seen anyone actually use any of this stuff to make a deliverable piece of software that is notably better than what developers can readily produce using traditional procedural languages. I mean sure, I suppose it would be nice if the C# team added some sort of category theoretically "pure" tree processing sub-language akin to some bastard child of LINQ and XSLT, but... meh. I don't think it would see a lot of use in practice.
  - lidHanteyk 7y ago
    A few months ago, while employed at a shop, I wrote about a hundred lines of Python which performed a basic katamorphism on some XML, outputting a PNG. Nobody else on my team could conceive of this, and were mystified by the fact that I could just sit down and do this. It wasn't too hard, though, because I could imagine the entire katamorphism in my mind. The traditional approaches weren't just stymied by this problem, BTW; the other developers wanted to go shopping for off-the-shelf components which transform XML to PNG, as if that would get us the specific katamorphism we desired. The nature of your everyday work will inform what you can do with category theory. I personally use category theory to design programming languages; it's something for which category theory gives a turn-the-key recipe: * Pick some objects of interest * Define a relatively free Cartesian closed category whose objects include your objects of interest * Enrich the category with interesting arrows * Extract a combinator basis The MarshallB programming language [0] is a good example of this recipe in action. [0] https://dl.acm.org/doi/10.1145/3341703 https://dl.acm.org/doi/10.1145/3341703
    - auggierose 7y ago
      But the real interesting part here is the use of exact real arithmetic, not the category theoretic part. Category theory is just used as scaffolding. I would also say it is dangerous to see things only through the category-theoretic lens, because no doubt, as with any generalisation, there will be plenty of situations where it does not provide the right generalisation.
      - lidHanteyk 7y ago
        Better scaffolding leads to bigger, better buildings. Don't knock the auxiliary and ancillary techniques; they're still necessary for this sort of work to be understandable. Also, from my perspective, the exact real arithmetic isn't super-interesting because it's not new; Turing was doing this sort of thing when he first got access to computers. Legend has that one of Turing's first recreational programs was computation of zeros of the Riemann zeta function, and ever since, there's been a tradition of exploring exact real arithmetic with computers and programming languages. MarshallB is one more incremental step forward in a big research programme of overcoming the inconvenient fact that we can't test real numbers for interesting properties with computers alone. At no point have I advocated only category theory. Categories are always composed of some collection of arrows (and objects, but I prefer object-free presentations!), and those arrows are always homogeneous, if not homoousios, composed of a single substance. We can study that substance on its own. Perhaps an analogy to materials science would be appropriate. We ought to study both each building material, be it sets, vector spaces, relations, graphs, or type theories; but also the architectural principles used to make buildings, like abstract algebra and category theory.
iaml 7y ago
Here's a practical example I've been thinking about a lot recently, in the context of frontend/react. You could create out of the building blocks today a very different kind of ide inside your browser. Imagine this: you are creating a component, you start with graphical part then in the browser you open a dev menu that is connected to redux or maybe just a list of api call functions or a bunch of hooks. You compose those to match with component props directly in browser and the hoc with required prop transformations is generated with appropriate typings and possibly test data ready. This covers a sizeable chunk of work I do everyday, and now even designers could do it. Especially if we hide git interactions from them too, which is also not very compicated.
mikorym 7y ago
There are foundational problems that can be studied via category theory, such as the view-update problem [1]. So, if you want to design a database you are faced with the problem of two users trying to update the same data at the same time and you will have to make a design decision about how it should work. I don't know if the video itself maybe fails to properly point out uses of category theory. My opinion on the matter is that if you do want to use mathematics in your everyday work, the main applications will come from the mathematics you know the best. So, whether you are interested in category theory or not will also influence whether you use it. Many of the concepts in category theory can be done instead in algebra and analysis, but it is the spirit of unification that inspires people to study category theory. A lot of functional programmers are delighted when they learn about axioms such as associativity (since you can prove thing about your program) but the concept is much older than category theory. So you can just know associativity if you are not really interested in category theory and that will already take you far. [1] M. Johnson and R. Rosebrugh, Fibrations and universal view updatability, Theoretical Computer Science 388.1, 2007, 109–129.
ssivark 7y ago
To clarify my above comment, since most responses are tangential... I’m comfortable with abstraction. I only want to see a hard/confusing solution become easy with category theoretic ideas. (Need not even be an “everyday” problem; all kinds of examples appreciated) One possibility I can imagine is that in a highly compositional language like Haskell, where structural patterns could be factored out as libraries, identifying patterns in a new problem means that you can now just use the library to take care of the structural “boilerplate” when writing code to solve the new problem, and focus purely on the domain-specific tidbits... in a sense allowing maximal code-reuse and convenience. It’s not Luke one couldn’t have solved the problem without categories — it’s just that there’s less “design pattern” boilerplate and correctness guarantees. I guess this is what it means to “make the trivial into trivially trivial” :-) Tho approach is then not very useful when you’re interested in solving only a single problem. But if you want to solve many problems, then this approach gives HUGE leverage towards reducing incidental complexity in code, and should be particularly useful when designing frameworks/libraries/DSLs/etc for maximal reuse.

lidHanteyk 7y ago

Here is one non-trivial insight: Every formal logic corresponds to a category. When we do logical deduction, we have facts and rules. We can apply rules to facts to get more facts. More specifically, formal logic is built from situations where we have some fact P, some rule P => Q, and some conclusion Q. In a category, we have objects and arrows. We can imagine arrows as mapping one object to another, or sending one object to another. We might have objects P and Q, and an arrow f : P -> Q relating them. The connection continues. We can take multiple rules in logic and apply them sequentially, building a proof tree; we can take multiple arrows in a category and compose them sequentially, building a path. In some logics, there is an idea of ex falso quodlibet, or from the false fact, anything can be proven; similarly, in some categories, there are initial objects, which come with arrows from the initial object to every other object. Just like how logical formalism eventually removed the possibility that logic is non-mathematical, category theory removes the possibility that logic is unstructured. Logic is actually incredibly highly structured, and those structures happen to coincide with structures in other parts of maths and physics.

jiggawatts 7y ago
Again though, how do I use this to solve everyday problems? I've seen some vaguely cool stuff done with Category theory in Haskell, e.g.: composable tree parsing and traversal, but I've never seen anyone actually use any of this stuff to make a deliverable piece of software that is notably better than what developers can readily produce using traditional procedural languages. I mean sure, I suppose it would be nice if the C# team added some sort of category theoretically "pure" tree processing sub-language akin to some bastard child of LINQ and XSLT, but... meh. I don't think it would see a lot of use in practice.
- lidHanteyk 7y ago
  A few months ago, while employed at a shop, I wrote about a hundred lines of Python which performed a basic katamorphism on some XML, outputting a PNG. Nobody else on my team could conceive of this, and were mystified by the fact that I could just sit down and do this. It wasn't too hard, though, because I could imagine the entire katamorphism in my mind. The traditional approaches weren't just stymied by this problem, BTW; the other developers wanted to go shopping for off-the-shelf components which transform XML to PNG, as if that would get us the specific katamorphism we desired. The nature of your everyday work will inform what you can do with category theory. I personally use category theory to design programming languages; it's something for which category theory gives a turn-the-key recipe: * Pick some objects of interest * Define a relatively free Cartesian closed category whose objects include your objects of interest * Enrich the category with interesting arrows * Extract a combinator basis The MarshallB programming language [0] is a good example of this recipe in action. [0] https://dl.acm.org/doi/10.1145/3341703 https://dl.acm.org/doi/10.1145/3341703
  - auggierose 7y ago
    But the real interesting part here is the use of exact real arithmetic, not the category theoretic part. Category theory is just used as scaffolding. I would also say it is dangerous to see things only through the category-theoretic lens, because no doubt, as with any generalisation, there will be plenty of situations where it does not provide the right generalisation.
    - lidHanteyk 7y ago
      Better scaffolding leads to bigger, better buildings. Don't knock the auxiliary and ancillary techniques; they're still necessary for this sort of work to be understandable. Also, from my perspective, the exact real arithmetic isn't super-interesting because it's not new; Turing was doing this sort of thing when he first got access to computers. Legend has that one of Turing's first recreational programs was computation of zeros of the Riemann zeta function, and ever since, there's been a tradition of exploring exact real arithmetic with computers and programming languages. MarshallB is one more incremental step forward in a big research programme of overcoming the inconvenient fact that we can't test real numbers for interesting properties with computers alone. At no point have I advocated only category theory. Categories are always composed of some collection of arrows (and objects, but I prefer object-free presentations!), and those arrows are always homogeneous, if not homoousios, composed of a single substance. We can study that substance on its own. Perhaps an analogy to materials science would be appropriate. We ought to study both each building material, be it sets, vector spaces, relations, graphs, or type theories; but also the architectural principles used to make buildings, like abstract algebra and category theory.

iaml 7y ago

Here's a practical example I've been thinking about a lot recently, in the context of frontend/react. You could create out of the building blocks today a very different kind of ide inside your browser. Imagine this: you are creating a component, you start with graphical part then in the browser you open a dev menu that is connected to redux or maybe just a list of api call functions or a bunch of hooks. You compose those to match with component props directly in browser and the hoc with required prop transformations is generated with appropriate typings and possibly test data ready. This covers a sizeable chunk of work I do everyday, and now even designers could do it. Especially if we hide git interactions from them too, which is also not very compicated.

mikorym 7y ago

There are foundational problems that can be studied via category theory, such as the view-update problem [1]. So, if you want to design a database you are faced with the problem of two users trying to update the same data at the same time and you will have to make a design decision about how it should work. I don't know if the video itself maybe fails to properly point out uses of category theory. My opinion on the matter is that if you do want to use mathematics in your everyday work, the main applications will come from the mathematics you know the best. So, whether you are interested in category theory or not will also influence whether you use it. Many of the concepts in category theory can be done instead in algebra and analysis, but it is the spirit of unification that inspires people to study category theory. A lot of functional programmers are delighted when they learn about axioms such as associativity (since you can prove thing about your program) but the concept is much older than category theory. So you can just know associativity if you are not really interested in category theory and that will already take you far. [1] M. Johnson and R. Rosebrugh, Fibrations and universal view updatability, Theoretical Computer Science 388.1, 2007, 109–129.

ssivark 7y ago

To clarify my above comment, since most responses are tangential... I’m comfortable with abstraction. I only want to see a hard/confusing solution become easy with category theoretic ideas. (Need not even be an “everyday” problem; all kinds of examples appreciated) One possibility I can imagine is that in a highly compositional language like Haskell, where structural patterns could be factored out as libraries, identifying patterns in a new problem means that you can now just use the library to take care of the structural “boilerplate” when writing code to solve the new problem, and focus purely on the domain-specific tidbits... in a sense allowing maximal code-reuse and convenience. It’s not Luke one couldn’t have solved the problem without categories — it’s just that there’s less “design pattern” boilerplate and correctness guarantees. I guess this is what it means to “make the trivial into trivially trivial” :-) Tho approach is then not very useful when you’re interested in solving only a single problem. But if you want to solve many problems, then this approach gives HUGE leverage towards reducing incidental complexity in code, and should be particularly useful when designing frameworks/libraries/DSLs/etc for maximal reuse.