9 ms·

Personally I find category theory to be a red herring when it comes to Haskell and really programming. I feel that people learn a bit of CT, then quote it endl

by kzhahou 11y ago

Personally I find category theory to be a red herring when it comes to Haskell and really programming. I feel that people learn a bit of CT, then quote it endlessly as a sort of elevation of programming from lowly code-slinging to a high mathematical pursuit. Except CT doesn't really provide all that much insight. At least not unless you're knee-deep in advanced type theory. But who has really read Benjamin Pierce's books (as beautiful as they are), or the original Hindley texts? A side comment, this one's more about CT itself, is that the standard texts don't seem to really have many results. Not compared to, say, any undergrad book on algebra or number theory, where cool theorems come at you every few pages to twist up your brain. Category Theory always felt almost mechanical to me. Lots of definitions and rules for assembling diagrams and such, but then what. Just the Yoneda Lemma and that's it? If anyone can point me to the fun CT theorems, I'd love to hear about them.

nabla9 11y ago
>CT itself, is that the standard texts don't seem to really have many results. Oh man. If you like math, CT gives nice mathematical definitions for stuff. I would love to use my algebra skills to do general programming like I can use my linear algebra knowledge in numerical programming. I'm making bold claim that I hope someone can debunk with awesome counterexamples: "CT HAS ZERO APPLICABILITY IN PROGRAMMING" Using CT to Linear algebra analogy: CT in programming is like learning definitions of vector spaces, subspaces, span, and basis and stopping there. No CT equivalent for solving linear systems, linear transformations, least-squares or eigenvalues. Just because you have rooted programming in cool algebraic notation does not mean anything in itself.
- pron 11y ago
  This is a kind of marketing trick Haskell has pulled, which some people fall for (regardless of the merits of the language), namely that Haskell is somehow more "mathematical" than other languages. The truth is that Haskell -- like all programming language -- has made a design choice, which was to bake in correctness proofs based on the Curry-Howard correspondence into the language. This means that instead of bringing the math to your program like other verification methods do[1], it takes you to the math, requiring your participation. Haskell just feels more mathy because C-H puts the math in your face. Another trick Haskell uses is preferring abstractions that are based on concepts from CT[2], and validating the utility of those abstractions on their "rigorous mathematical foundations". This is again just another case of taking you to the math rather than the other way around. Programming languages are first and foremost human languages, meant to be written and read by humans. As such, their power is drawn from a single source: their interaction with human cognition. Whether an abstraction is "mathematical" (whatever that means) has absolutely no relevance to its power, which comes from cognition (and psychology in general) rather than math. All this "in your face" math does is make the machine's job of verifying your software easier. A Haskeller tried convincing me that such a language is a good fit for human programmers, too, because all it is is a subset of more traditional, impure languages. But the notion of subset => simpler is a mathematical notion with no relevance to cognition. If humans operated in this way, natural languages would have been much more mathematically simpler, too. [1]: See KeY: http://www.key-project.org/ http://www.key-project.org/ [2]: To be fair, I'm not sure that Haskell, given its original design philosophy, has much choice in the matter.
  - johncolanduoni 11y ago
    > validating the utility of those abstractions on their "rigorous mathematical foundations" Some Haskell users may think this, but I think the usefulness of the foundations is not derived from rigor. Instead, it is derived from the wealth of knowledge we have about mathematical structures which makes them easier to reason about. So by linking the programming structures you are using (e.g. monads) with associated mathematical structures (also called monads[1]), all of the mathematical knowledge surrounding that structure suddenly becomes available. This is rather like how doing numerical calculations with matrices benefits from the wealth of knowledge about linear algebra. Another "mathy" aspect that Haskell and similar languages have is that they like to start with a few fundamental constructs and build everything else within that system. This is more a design philosophy than anything, but I think it does have its advantages in that it results in better composablility, since everything "comes from the same place". As far as the relationship to cognition, I think Haskell will be better in this regard if you are mathematically minded, because you will understand programming constructs from their mathematical roots. For example, I had an easy time picking up monads because I knew the category theory version. It could be argued that once a person learns these concepts they are given a better means of reasoning about programs than other languages, but I suspect that largely depends on one's intellectual leanings. [1]: https://en.wikipedia.org/wiki/Monad_(category_theory) https://en.wikipedia.org/wiki/Monad_(category_theory)
    - pron 11y ago
      > which makes them easier to reason about Easier to reason about by whom? Most programming models have their own calculi which are exploited by their respective verification tools. They don't, however, expose that to the developer. > I think Haskell will be better in this regard if you are mathematically minded I think that Haskell is better if you are mathematically minded and interested in thinking (a lot!) about abstractions. I like to keep my abstractions cognitively simple (primitive, even), and my algorithms sophisticated and powerful. I'd rather the people writing the verifier put their mathematical leanings to use on the relevant calculus, while I use mine on the algorithmic domain I'm working in. Just like I don't require the developer using my database to be familiar with data structures and concurrency, I don't want those interested in formal verification requiring me to change my programming style to make their job easier. In fact, their job is quite the opposite: provide verification tools that are useful for the programming languages that make for a good cognitive fit, rather than design languages that make verification easier with the (possibly misplaced) hope that by some unexplained coincidence, a language designed to make a machine's reasoning easier would also do the same for a human. Software verification is a fascinating algorithmic topic. Language design is a fascinating UI endeavour tasked -- like all UI -- with coming up with great cognitive abstractions. The two should, of course, cross-pollinate one another, but shouldn't become the same. Language designers should spend their time thinking how humans think about computation and how they interact with computers, not how to make programming models fit certain branches of math.
- nilkn 11y ago
  I know this isn't really the answer anyone's looking for, but I legitimately found some basic knowledge of category theory to be very useful with Haskell. Maybe it's a red herring -- I don't really know -- but when I was able to intuitively see the connection between a monad in Haskell and a monad in category theory it was almost like a switch went off in my brain and the abstraction was easier to work with and just less intimidating. The epiphany I had from this is that, while linear algebra's utility comes in the form of designing efficient algorithms, CT's utility (in Haskell) comes in the form of understanding structures. It's similar to thinking of modular arithmetic in terms of remainders vs. quotient groups. I get lost doing anything complex with the former way of thinking, but when I switch to thinking in terms of basic abstract algebra suddenly the foliage clears and the way ahead is clear.
  - AnimalMuppet 11y ago
    Then, from the better understanding of structures, does CT help you design better types for your program? Or better algorithms?
- marcosdumay 11y ago
  Well, algebra is a language created with the goal of making simple things easy to communicate. Yes, I'm getting in a tangent and calling operations in an infinite and non-countable basis "simple", but just try to do anything complex in non-linear algebra and it all falls apart already, never mind completely discontinuous functions. Category theory is a language created to communicate complex models. If it's not obvious yet that you can't use CT the same way you use algebra, let me state so: you can't. CT must be less powerful than algebra, because you can't reason about complex stuff as easily as you can reason about simple stuff. Yet, one mostly can not write a program nowadays without using CT. There's no language that does not implement a subset of it. You don't notice it for the same reason that fish do not notice the water. But as powerless as CT must be, it gives you plenty of tools for simplifying your models, and not having those tools available can only make your program more complex, never simpler.
johncolanduoni 11y ago
> Category Theory always felt almost mechanical to me. Lots of definitions and rules for assembling diagrams and such, but then what. Category Theory is more about getting (as one of my professors put it) "a God's-eye view of mathematics". What I have found to be the most deep and useful is the way it provides concrete definitions which unite constructions that mathematicians were already calling the same thing (e.g. products, co-products). It is also absolutely amazing at showing links between different (seemingly unrelated) parts of mathematics. In this way, it forms a sort of lingua-franca for mathematics. This math StackExchange answer[1] gives some really good concrete examples. If you want a book which gives a lot of more concrete results along with category theory, you should try Algebra: Chapter 0. It is more focused on abstract algebra, but it does it all from a categorical perspective while not assuming you know one iota of category theory (at the start). [1]: http://math.stackexchange.com/questions/312605/what-is-category-theory-useful-for http://math.stackexchange.com/questions/312605/what-is-categ...
- kzhahou 11y ago
  I've seen Algebra:Ch0 around but haven't picked it up yet. Thanks for the recommendation!
tel 11y ago
They are mechanical because CT is more a language than a field in its own right. They're mechanical in the same way that a lot of logic or universal algebra is—the interesting stuff arises when you start making choices and using the tools to express your ideas. On the other hand, CT was invented to talk about homology, so if you want to see a ton of examples of CT being used "in its natural habitat" then look there.

by kzhahou 11y ago

nabla9 11y ago

>CT itself, is that the standard texts don't seem to really have many results. Oh man. If you like math, CT gives nice mathematical definitions for stuff. I would love to use my algebra skills to do general programming like I can use my linear algebra knowledge in numerical programming. I'm making bold claim that I hope someone can debunk with awesome counterexamples: "CT HAS ZERO APPLICABILITY IN PROGRAMMING" Using CT to Linear algebra analogy: CT in programming is like learning definitions of vector spaces, subspaces, span, and basis and stopping there. No CT equivalent for solving linear systems, linear transformations, least-squares or eigenvalues. Just because you have rooted programming in cool algebraic notation does not mean anything in itself.

pron 11y ago
This is a kind of marketing trick Haskell has pulled, which some people fall for (regardless of the merits of the language), namely that Haskell is somehow more "mathematical" than other languages. The truth is that Haskell -- like all programming language -- has made a design choice, which was to bake in correctness proofs based on the Curry-Howard correspondence into the language. This means that instead of bringing the math to your program like other verification methods do[1], it takes you to the math, requiring your participation. Haskell just feels more mathy because C-H puts the math in your face. Another trick Haskell uses is preferring abstractions that are based on concepts from CT[2], and validating the utility of those abstractions on their "rigorous mathematical foundations". This is again just another case of taking you to the math rather than the other way around. Programming languages are first and foremost human languages, meant to be written and read by humans. As such, their power is drawn from a single source: their interaction with human cognition. Whether an abstraction is "mathematical" (whatever that means) has absolutely no relevance to its power, which comes from cognition (and psychology in general) rather than math. All this "in your face" math does is make the machine's job of verifying your software easier. A Haskeller tried convincing me that such a language is a good fit for human programmers, too, because all it is is a subset of more traditional, impure languages. But the notion of subset => simpler is a mathematical notion with no relevance to cognition. If humans operated in this way, natural languages would have been much more mathematically simpler, too. [1]: See KeY: http://www.key-project.org/ http://www.key-project.org/ [2]: To be fair, I'm not sure that Haskell, given its original design philosophy, has much choice in the matter.
- johncolanduoni 11y ago
  > validating the utility of those abstractions on their "rigorous mathematical foundations" Some Haskell users may think this, but I think the usefulness of the foundations is not derived from rigor. Instead, it is derived from the wealth of knowledge we have about mathematical structures which makes them easier to reason about. So by linking the programming structures you are using (e.g. monads) with associated mathematical structures (also called monads[1]), all of the mathematical knowledge surrounding that structure suddenly becomes available. This is rather like how doing numerical calculations with matrices benefits from the wealth of knowledge about linear algebra. Another "mathy" aspect that Haskell and similar languages have is that they like to start with a few fundamental constructs and build everything else within that system. This is more a design philosophy than anything, but I think it does have its advantages in that it results in better composablility, since everything "comes from the same place". As far as the relationship to cognition, I think Haskell will be better in this regard if you are mathematically minded, because you will understand programming constructs from their mathematical roots. For example, I had an easy time picking up monads because I knew the category theory version. It could be argued that once a person learns these concepts they are given a better means of reasoning about programs than other languages, but I suspect that largely depends on one's intellectual leanings. [1]: https://en.wikipedia.org/wiki/Monad_(category_theory) https://en.wikipedia.org/wiki/Monad_(category_theory)
  - pron 11y ago
    > which makes them easier to reason about Easier to reason about by whom? Most programming models have their own calculi which are exploited by their respective verification tools. They don't, however, expose that to the developer. > I think Haskell will be better in this regard if you are mathematically minded I think that Haskell is better if you are mathematically minded and interested in thinking (a lot!) about abstractions. I like to keep my abstractions cognitively simple (primitive, even), and my algorithms sophisticated and powerful. I'd rather the people writing the verifier put their mathematical leanings to use on the relevant calculus, while I use mine on the algorithmic domain I'm working in. Just like I don't require the developer using my database to be familiar with data structures and concurrency, I don't want those interested in formal verification requiring me to change my programming style to make their job easier. In fact, their job is quite the opposite: provide verification tools that are useful for the programming languages that make for a good cognitive fit, rather than design languages that make verification easier with the (possibly misplaced) hope that by some unexplained coincidence, a language designed to make a machine's reasoning easier would also do the same for a human. Software verification is a fascinating algorithmic topic. Language design is a fascinating UI endeavour tasked -- like all UI -- with coming up with great cognitive abstractions. The two should, of course, cross-pollinate one another, but shouldn't become the same. Language designers should spend their time thinking how humans think about computation and how they interact with computers, not how to make programming models fit certain branches of math.
nilkn 11y ago
I know this isn't really the answer anyone's looking for, but I legitimately found some basic knowledge of category theory to be very useful with Haskell. Maybe it's a red herring -- I don't really know -- but when I was able to intuitively see the connection between a monad in Haskell and a monad in category theory it was almost like a switch went off in my brain and the abstraction was easier to work with and just less intimidating. The epiphany I had from this is that, while linear algebra's utility comes in the form of designing efficient algorithms, CT's utility (in Haskell) comes in the form of understanding structures. It's similar to thinking of modular arithmetic in terms of remainders vs. quotient groups. I get lost doing anything complex with the former way of thinking, but when I switch to thinking in terms of basic abstract algebra suddenly the foliage clears and the way ahead is clear.
- AnimalMuppet 11y ago
  Then, from the better understanding of structures, does CT help you design better types for your program? Or better algorithms?
marcosdumay 11y ago
Well, algebra is a language created with the goal of making simple things easy to communicate. Yes, I'm getting in a tangent and calling operations in an infinite and non-countable basis "simple", but just try to do anything complex in non-linear algebra and it all falls apart already, never mind completely discontinuous functions. Category theory is a language created to communicate complex models. If it's not obvious yet that you can't use CT the same way you use algebra, let me state so: you can't. CT must be less powerful than algebra, because you can't reason about complex stuff as easily as you can reason about simple stuff. Yet, one mostly can not write a program nowadays without using CT. There's no language that does not implement a subset of it. You don't notice it for the same reason that fish do not notice the water. But as powerless as CT must be, it gives you plenty of tools for simplifying your models, and not having those tools available can only make your program more complex, never simpler.

johncolanduoni 11y ago

> Category Theory always felt almost mechanical to me. Lots of definitions and rules for assembling diagrams and such, but then what. Category Theory is more about getting (as one of my professors put it) "a God's-eye view of mathematics". What I have found to be the most deep and useful is the way it provides concrete definitions which unite constructions that mathematicians were already calling the same thing (e.g. products, co-products). It is also absolutely amazing at showing links between different (seemingly unrelated) parts of mathematics. In this way, it forms a sort of lingua-franca for mathematics. This math StackExchange answer[1] gives some really good concrete examples. If you want a book which gives a lot of more concrete results along with category theory, you should try Algebra: Chapter 0. It is more focused on abstract algebra, but it does it all from a categorical perspective while not assuming you know one iota of category theory (at the start). [1]: http://math.stackexchange.com/questions/312605/what-is-category-theory-useful-for http://math.stackexchange.com/questions/312605/what-is-categ...

kzhahou 11y ago
I've seen Algebra:Ch0 around but haven't picked it up yet. Thanks for the recommendation!

tel 11y ago

They are mechanical because CT is more a language than a field in its own right. They're mechanical in the same way that a lot of logic or universal algebra is—the interesting stuff arises when you start making choices and using the tools to express your ideas. On the other hand, CT was invented to talk about homology, so if you want to see a ton of examples of CT being used "in its natural habitat" then look there.