18 ms·

> validating the utility of those abstractions on their "rigorous mathematical foundations" Some Haskell users may think this, but I think the usefulness of th

> 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.
- johncolanduoni 11y ago
  > Easier to reason about by whom? As I said, by those who are aware of the math concepts they are based on. Monads are I think the best example for Haskell; particularly in how they behave with respect to functions, which fits quite nicely with a categorical point of view. > I think that Haskell is better if you are mathematically minded and interested in thinking (a lot!) about abstractions. I'm not sure you can be mathematically minded in the pure mathematics sense (which is what Haskell draws on) without being interested in thinking a lot about abstractions. If you are more focused on concrete mathematics, then Haskell is unlikely to be your ideal language, but when people reference mathematics in regards to the language I suspect they are referring to the pure variant. In any case, I am, which is I think most of the confusion here. > 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. The only built in formal verification I can think of in Haskell is the type system. In that case, I think your analogy breaks down; I'm not sure how one can manage to program (effectively) in any language without understanding its type system. If you are referring to an external static analysis tool, then I'm not sure how you can put that on Haskell itself. > a language designed to make a machine's reasoning easier would also do the same for a human I believe it does for humans who come from a pure math background, in the same way programmers who know an object oriented language will find it easier to grasp another object oriented language. Moreover, it seems pretty clear that this is no a coincidence; it was the driving force behind Haskell's most fundamental design (e.g. Curry Howard) and its library (e.g. monads). So if you (as you say) are not interested in abstract mathematics, then it is no wonder you don't care for its methods. > 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. Unless, of course, they are focusing on humans that are not only well versed and comfortable with certain branches of math, but prefer that mode of thinking. Haskell's unofficial motto of "avoid success at all costs" makes me think that focusing on this demographic is likely one of the language's design features, as opposed to making the best language ever for everybody. In any case, I would argue it is good for mathematicians, but not that all of the effort to move to that way of thinking is something universally useful for programmers.
- 11y ago
nabla9 11y ago
>It could be argued that once a person learns these concepts they are given a better means of reasoning about programs than other languages, This was my challenge. Give concrete examples where you reason about programs better while programming because of the category theory. People have been arguing this for years without any concrete examples. I'm a math person and I would really like to use category theory and mathematical intuition when programming. I argue that there is very little usable structure for reasoning for the programmers after the definitions. There is no buildup of structure that is common when mathematics is used effectively. The gain from math is very small or nonexistent.
- pekk 11y ago
  The gain from maths is that you can tell everyone what an exalted, rarefied experience you are having writing the same programs people write in blub, except more slowly, somehow using elite stuff you know from maths. edit: I have no criticism of maths here, maths is great.
AnimalMuppet 11y ago
> 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. Only if what the language does with monads exactly mirrors what CT does with monads. Otherwise the language subtly lies to you. In fact, this may be the case. I seem to recall that Haskell monads only have to obey two of the three monad laws. That is, they don't have to truly be (CT) monads. That's supposed to not matter, but if nothing else, it kind of makes your argument a bit less well grounded. > This is rather like how doing numerical calculations with matrices benefits from the wealth of knowledge about linear algebra. In the exact same way, this is only true if the matrix package truly implements linear algebra correctly. To the degree that the matrix package doesn't do that, your reasoning based on linear algebra leads you astray.
- tome 11y ago
  > In fact, this may be the case. I seem to recall that Haskell monads only have to obey two of the three monad laws. That is, they don't have to truly be (CT) monads. That's news to me! Mathematicians wouldn't find the monads that appear in Haskell especially interesting, I think (at least not the ones that are instances of `Monad`), but that's beside the point.
  - AnimalMuppet 11y ago
    So I'm repeating what somebody said rather than my own claim, but I think it was that Haskell monads didn't have to be... one of left- or right-associative. But they had to be the other. Wish I knew of a good way to search HN; it was in a comment here maybe 6 months or a year ago...
    - tome 11y ago
      > Haskell monads didn't have to be... one of left- or right-associative. But they had to be the other. That's very puzzling. I wish I knew what you were referring to!

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.

johncolanduoni 11y ago
> Easier to reason about by whom? As I said, by those who are aware of the math concepts they are based on. Monads are I think the best example for Haskell; particularly in how they behave with respect to functions, which fits quite nicely with a categorical point of view. > I think that Haskell is better if you are mathematically minded and interested in thinking (a lot!) about abstractions. I'm not sure you can be mathematically minded in the pure mathematics sense (which is what Haskell draws on) without being interested in thinking a lot about abstractions. If you are more focused on concrete mathematics, then Haskell is unlikely to be your ideal language, but when people reference mathematics in regards to the language I suspect they are referring to the pure variant. In any case, I am, which is I think most of the confusion here. > 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. The only built in formal verification I can think of in Haskell is the type system. In that case, I think your analogy breaks down; I'm not sure how one can manage to program (effectively) in any language without understanding its type system. If you are referring to an external static analysis tool, then I'm not sure how you can put that on Haskell itself. > a language designed to make a machine's reasoning easier would also do the same for a human I believe it does for humans who come from a pure math background, in the same way programmers who know an object oriented language will find it easier to grasp another object oriented language. Moreover, it seems pretty clear that this is no a coincidence; it was the driving force behind Haskell's most fundamental design (e.g. Curry Howard) and its library (e.g. monads). So if you (as you say) are not interested in abstract mathematics, then it is no wonder you don't care for its methods. > 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. Unless, of course, they are focusing on humans that are not only well versed and comfortable with certain branches of math, but prefer that mode of thinking. Haskell's unofficial motto of "avoid success at all costs" makes me think that focusing on this demographic is likely one of the language's design features, as opposed to making the best language ever for everybody. In any case, I would argue it is good for mathematicians, but not that all of the effort to move to that way of thinking is something universally useful for programmers.
11y ago

nabla9 11y ago

>It could be argued that once a person learns these concepts they are given a better means of reasoning about programs than other languages, This was my challenge. Give concrete examples where you reason about programs better while programming because of the category theory. People have been arguing this for years without any concrete examples. I'm a math person and I would really like to use category theory and mathematical intuition when programming. I argue that there is very little usable structure for reasoning for the programmers after the definitions. There is no buildup of structure that is common when mathematics is used effectively. The gain from math is very small or nonexistent.

pekk 11y ago
The gain from maths is that you can tell everyone what an exalted, rarefied experience you are having writing the same programs people write in blub, except more slowly, somehow using elite stuff you know from maths. edit: I have no criticism of maths here, maths is great.

AnimalMuppet 11y ago

> 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. Only if what the language does with monads exactly mirrors what CT does with monads. Otherwise the language subtly lies to you. In fact, this may be the case. I seem to recall that Haskell monads only have to obey two of the three monad laws. That is, they don't have to truly be (CT) monads. That's supposed to not matter, but if nothing else, it kind of makes your argument a bit less well grounded. > This is rather like how doing numerical calculations with matrices benefits from the wealth of knowledge about linear algebra. In the exact same way, this is only true if the matrix package truly implements linear algebra correctly. To the degree that the matrix package doesn't do that, your reasoning based on linear algebra leads you astray.

tome 11y ago
> In fact, this may be the case. I seem to recall that Haskell monads only have to obey two of the three monad laws. That is, they don't have to truly be (CT) monads. That's news to me! Mathematicians wouldn't find the monads that appear in Haskell especially interesting, I think (at least not the ones that are instances of `Monad`), but that's beside the point.
- AnimalMuppet 11y ago
  So I'm repeating what somebody said rather than my own claim, but I think it was that Haskell monads didn't have to be... one of left- or right-associative. But they had to be the other. Wish I knew of a good way to search HN; it was in a comment here maybe 6 months or a year ago...
  - tome 11y ago
    > Haskell monads didn't have to be... one of left- or right-associative. But they had to be the other. That's very puzzling. I wish I knew what you were referring to!