3 ms·

Not at all. Lambda Calculus is a much better mathematical foundational for functional programming that Category Theory is. I can teach a programmer Lambda Calcu

Not at all. Lambda Calculus is a much better mathematical foundational for functional programming that Category Theory is. I can teach a programmer Lambda Calculus in a few minutes and they will be able to use it for programming. Not so with CT. You need to add a lot of structure to get anything close to Lambda Calculus. Basically about 50% of a Typical CT book to get there.

carapace 4y ago
> I can teach a programmer Lambda Calculus in a few minutes and they will be able to use it for programming. Which programmer? Bare Lambda Calculus? Wouldn't that be pretty useless? > Not so with CT. You need to add a lot of structure to get anything close to Lambda Calculus. I'm not sure I follow, I've heard that "the simply typed lambda-calculus is modeled by any cartesian closed category (CCC)." http://conal.net/papers/compiling-to-categories/ http://conal.net/papers/compiling-to-categories/
- mbrodersen 4y ago
  > Wouldn't that be pretty useless? Not at all. It is way more useful than learning CT. LC is the foundation used in almost all of computer science. You need to understand it to read any advanced Type Theory papers for example and you can directly use it as a starting point when designing a functional programming language. > “the simply typed lambda-calculus is modeled by any cartesian closed category (CCC) That is correct. You can model pretty much anything in Category Theory. The same way you can model pretty much anything in Type Theory or Set Theory. However IMHO it takes a lot more structure to build up to CCC than it does to simply use LC. The paper you are referencing is great. However the author might as well have used LC to achieve the same goal.
  - carapace 4y ago
    I dunno, I've been messing around with Joy recently and it's put me off LC. https://en.wikipedia.org/wiki/Joy_(programming_language) https://en.wikipedia.org/wiki/Joy_(programming_language)

carapace 4y ago

> I can teach a programmer Lambda Calculus in a few minutes and they will be able to use it for programming. Which programmer? Bare Lambda Calculus? Wouldn't that be pretty useless? > Not so with CT. You need to add a lot of structure to get anything close to Lambda Calculus. I'm not sure I follow, I've heard that "the simply typed lambda-calculus is modeled by any cartesian closed category (CCC)." http://conal.net/papers/compiling-to-categories/ http://conal.net/papers/compiling-to-categories/

mbrodersen 4y ago
> Wouldn't that be pretty useless? Not at all. It is way more useful than learning CT. LC is the foundation used in almost all of computer science. You need to understand it to read any advanced Type Theory papers for example and you can directly use it as a starting point when designing a functional programming language. > “the simply typed lambda-calculus is modeled by any cartesian closed category (CCC) That is correct. You can model pretty much anything in Category Theory. The same way you can model pretty much anything in Type Theory or Set Theory. However IMHO it takes a lot more structure to build up to CCC than it does to simply use LC. The paper you are referencing is great. However the author might as well have used LC to achieve the same goal.
- carapace 4y ago
  I dunno, I've been messing around with Joy recently and it's put me off LC. https://en.wikipedia.org/wiki/Joy_(programming_language) https://en.wikipedia.org/wiki/Joy_(programming_language)