5 ms·

> ... but I find the casual chain of events questionable ... When I spoke to the people who actually wrote the RFCs, they said category theory had no part in th

> ... but I find the casual chain of events questionable ... When I spoke to the people who actually wrote the RFCs, they said category theory had no part in their thinking. I think you missed one level of indirection in my argument. I'm not claiming that language designers employ Category Theory explicitly when designing new language features (although this is indeed the case with Haskell, PureScript, and similar languages). Rather, my argument is that Category Theory features typically debut in these purely functional languages and then you will see on the Wikipedia page of mainstream languages something like: “Influenced by Haskell” (e.g. Rust, +20 others) . Category Theory is very abstract by nature, so I think it is only natural that there is some kind of indirect step through e.g. Haskell where people can see it in action first, before such features land in mainstream programming languages. The language designers would then say, 'Well, I have been influenced by Haskell (and not by Category Theory)', although the concept behind it is truly based on CT. Many programmers don't keep math books at their workstation. However, they constantly utilize mathematical concepts in their coding. Often, they refer to programming language tutorials where these mathematical ideas are already implemented, for example, in Python or C++. This is as opposed to learning the concepts directly from a book on Algebra, Geometry, or Trigonometry. However, that still qualifies as applied mathematics. Hence, I see no reason why it shouldn't count as applied CT if you borrow concepts from Haskell that are based on CT.

j2kun 3y ago
> Often, they refer to programming language tutorials where these mathematical ideas are already implemented, for example, in Python or C++. The difference is that _someone_ is actually implementing the features they're relying on, and those people know the math, understand its importance, and deliberately apply it. I know because I dig through their git commits so I can interview them about their work for my book. Your argument puts a lot of faith in Haskell. Let me take one path in your example to make this concrete. Rust was influenced by Haskell, how specifically? [1] claims it was mainly in "typeclasses, type families." Picking one randomly, the GHC user guide [2] describes type families as originating from three specific papers, [3], [4], [5], none of which mention category theory (nor does the much longer Haskell Wiki [6]). It seems to suggest, what is obvious to me, that not _all_ features of Haskell are related to category theory. If every time I trace claims of applied CT I find big holes, how could I possibly believe that so many great ideas that programmers use every day are secretly deliberately based on CT? There is a deeper discussion to be had here, along the lines of "does it count as an application of math if none of the people doing the applying think about the math." I think the answer is no. Math is a modeling language and if nobody models their problems with it then theorems do nothing. And so, if all of the category theory is lost in the translation from some (perhaps itself far removed) language feature of Haskell and later inspired language design, then that tells me category theory is the _wrong_ modeling language for that design problem. If it were good, and if the resulting theorems were essential and useful, then the practitioners would adopt it. That is a failure of CT. [1]: https://doc.rust-lang.org/reference/influences.html https://doc.rust-lang.org/reference/influences.html [2]: https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/type_families.html https://downloads.haskell.org/ghc/latest/docs/users_guide/ex... [3]: https://www.microsoft.com/en-us/research/wp-content/uploads/2005/01/assoc.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/... [4]: https://www.microsoft.com/en-us/research/wp-content/uploads/2005/01/at-syns.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/... [5]: https://www.microsoft.com/en-us/research/wp-content/uploads/2008/01/icfp2008.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/... [6]: https://wiki.haskell.org/GHC/Type_families https://wiki.haskell.org/GHC/Type_families
- tutfbhuf 3y ago
  > describes type families as originating from three specific papers, [3], [4], [5], none of which mention category theory (nor does the much longer Haskell Wiki [6]). It seems to suggest, what is obvious to me, that not _all_ features of Haskell are related to category theory. Since you've mentioned it, one of the inventors of type families is Simon Peyton Jones. He is quite renowned within the Haskell community as he is also a significant contributor to the design of the Haskell language. Now, let's examine what he has to say about Category Theory. > "I say “surprising” because anything with as exotic a name as “monad” — derived from category theory, one of the most abstract branches of mathematics — is unlikely to be very useful to red-blooded programmers. But one of the joys of functional programming is the way in which apparently exotic theory can have a direct and practical application, and the monadic story is a good example." https://gist.github.com/dtchepak/3163428 https://gist.github.com/dtchepak/3163428 In his own words, "apparently exotic theory [Category Theory] can have a direct and practical application," indicating that you hold a differing view from Simon, fair enough, however I believe that few people on this planet have a deeper understanding of Haskell than he does, which is why I hold his opinion in high regard. So, what about the other major language designers of Haskell? Firstly, there's Philip Wadler. For a clearer understanding of his work, you can refer to his presentation titled "Category Theory for the Working Hacker" (https://www.infoq.com/presentations/category-theory-propositions-principle/ https://www.infoq.com/presentations/category-theory-proposit...). The title is quite self-explanatory. Then there's John Hughes, who is renowned for "Generalising monads to arrows", known as Hughes Arrows. His work has a profound correlation with Category Theory, a fact that John Hughes is fully aware of. In my view, these examples provide sufficient evidence to affirm that Haskell's language designers are well versed in Category Theory concepts. These concepts, to varying degrees, have informed the design of Haskell. Of course, discussing individual features such as type families can become contentious when determining the extent of Category Theory's influence. For instance, it could be argued that these features are more closely related to Type Theory. However, many argue that Type Theory is the internal language of Category Theory. > There is a deeper discussion to be had here, along the lines of "does it count as an application of math if none of the people doing the applying think about the math." I think the answer is no I'd like to introduce you to the topic known as the Curry-Howard-Lambek correspondence, which posits a three-way isomorphism between types in programming languages, propositions in logic, and objects within a Cartesian closed category. You may already be familiar with the term "proofs-as-programs". It's important to note that the type system in Haskell isn't sufficient for theorem proving, but it becomes capable of constructing elementary proofs if you enable features like DataKinds, GADTs, PolyKinds, ScopedTypeVariables, TypeApplications, TypeFamilies, and TypeOperators. In contrast, I've also worked with Coq, which undeniably possesses the strength to prove intriguing theorems. What's particularly notable about Coq is its capacity to output Haskell programs based on its proofs, resulting in a Haskell program that lacks the strong guarantees of Coq. In this sense, you could imagine the resultant Haskell program as a "proof sketch" (which is usually correct if it compiles). I don't presume that you would refute this isomorphism. However, it's possible that you have again a differing perspective on what isomorphism actually means. To me, it's pretty much equivalence.

j2kun 3y ago

> Often, they refer to programming language tutorials where these mathematical ideas are already implemented, for example, in Python or C++. The difference is that _someone_ is actually implementing the features they're relying on, and those people know the math, understand its importance, and deliberately apply it. I know because I dig through their git commits so I can interview them about their work for my book. Your argument puts a lot of faith in Haskell. Let me take one path in your example to make this concrete. Rust was influenced by Haskell, how specifically? [1] claims it was mainly in "typeclasses, type families." Picking one randomly, the GHC user guide [2] describes type families as originating from three specific papers, [3], [4], [5], none of which mention category theory (nor does the much longer Haskell Wiki [6]). It seems to suggest, what is obvious to me, that not _all_ features of Haskell are related to category theory. If every time I trace claims of applied CT I find big holes, how could I possibly believe that so many great ideas that programmers use every day are secretly deliberately based on CT? There is a deeper discussion to be had here, along the lines of "does it count as an application of math if none of the people doing the applying think about the math." I think the answer is no. Math is a modeling language and if nobody models their problems with it then theorems do nothing. And so, if all of the category theory is lost in the translation from some (perhaps itself far removed) language feature of Haskell and later inspired language design, then that tells me category theory is the _wrong_ modeling language for that design problem. If it were good, and if the resulting theorems were essential and useful, then the practitioners would adopt it. That is a failure of CT. [1]: https://doc.rust-lang.org/reference/influences.html https://doc.rust-lang.org/reference/influences.html [2]: https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/type_families.html https://downloads.haskell.org/ghc/latest/docs/users_guide/ex... [3]: https://www.microsoft.com/en-us/research/wp-content/uploads/2005/01/assoc.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/... [4]: https://www.microsoft.com/en-us/research/wp-content/uploads/2005/01/at-syns.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/... [5]: https://www.microsoft.com/en-us/research/wp-content/uploads/2008/01/icfp2008.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/... [6]: https://wiki.haskell.org/GHC/Type_families https://wiki.haskell.org/GHC/Type_families

tutfbhuf 3y ago
> describes type families as originating from three specific papers, [3], [4], [5], none of which mention category theory (nor does the much longer Haskell Wiki [6]). It seems to suggest, what is obvious to me, that not _all_ features of Haskell are related to category theory. Since you've mentioned it, one of the inventors of type families is Simon Peyton Jones. He is quite renowned within the Haskell community as he is also a significant contributor to the design of the Haskell language. Now, let's examine what he has to say about Category Theory. > "I say “surprising” because anything with as exotic a name as “monad” — derived from category theory, one of the most abstract branches of mathematics — is unlikely to be very useful to red-blooded programmers. But one of the joys of functional programming is the way in which apparently exotic theory can have a direct and practical application, and the monadic story is a good example." https://gist.github.com/dtchepak/3163428 https://gist.github.com/dtchepak/3163428 In his own words, "apparently exotic theory [Category Theory] can have a direct and practical application," indicating that you hold a differing view from Simon, fair enough, however I believe that few people on this planet have a deeper understanding of Haskell than he does, which is why I hold his opinion in high regard. So, what about the other major language designers of Haskell? Firstly, there's Philip Wadler. For a clearer understanding of his work, you can refer to his presentation titled "Category Theory for the Working Hacker" (https://www.infoq.com/presentations/category-theory-propositions-principle/ https://www.infoq.com/presentations/category-theory-proposit...). The title is quite self-explanatory. Then there's John Hughes, who is renowned for "Generalising monads to arrows", known as Hughes Arrows. His work has a profound correlation with Category Theory, a fact that John Hughes is fully aware of. In my view, these examples provide sufficient evidence to affirm that Haskell's language designers are well versed in Category Theory concepts. These concepts, to varying degrees, have informed the design of Haskell. Of course, discussing individual features such as type families can become contentious when determining the extent of Category Theory's influence. For instance, it could be argued that these features are more closely related to Type Theory. However, many argue that Type Theory is the internal language of Category Theory. > There is a deeper discussion to be had here, along the lines of "does it count as an application of math if none of the people doing the applying think about the math." I think the answer is no I'd like to introduce you to the topic known as the Curry-Howard-Lambek correspondence, which posits a three-way isomorphism between types in programming languages, propositions in logic, and objects within a Cartesian closed category. You may already be familiar with the term "proofs-as-programs". It's important to note that the type system in Haskell isn't sufficient for theorem proving, but it becomes capable of constructing elementary proofs if you enable features like DataKinds, GADTs, PolyKinds, ScopedTypeVariables, TypeApplications, TypeFamilies, and TypeOperators. In contrast, I've also worked with Coq, which undeniably possesses the strength to prove intriguing theorems. What's particularly notable about Coq is its capacity to output Haskell programs based on its proofs, resulting in a Haskell program that lacks the strong guarantees of Coq. In this sense, you could imagine the resultant Haskell program as a "proof sketch" (which is usually correct if it compiles). I don't presume that you would refute this isomorphism. However, it's possible that you have again a differing perspective on what isomorphism actually means. To me, it's pretty much equivalence.