Yup! Haskell borrows heavily from category theory, and there's a lot of value in knowing the stuff, but people have also been productive in SQL for decades without any formal knowledge of relational algebra.
Asking as a practioner interested in learning the conceptual underpinnings :)
There is an important part about using an SQL DB which is about the engineering side of things, such as access patterns, indexing, efficient storage and so on. And then there is the side that is about relational expressions.
An intuition of mine is that people who feel more comfortable with the second part, lean on SQL (and DB features in general) to do work for them, while eschewing things like ORMs.
I'd say CT is FP. FP is about doing algebra to derive programs and CT is the math that describes that. In Manfred von Thun’s article "Joy compared with other functional languages" ( https://www.kevinalbrecht.com/code/joy-mirror/j08cnt.html ) he asks,
> Could the language of categories be used for writing programs? Any lambda expression can be translated into a categorical expression, so the language of categories is expressively complete. But this does not make it a suitable language for writing programs. As it stands it is a very low-level language.
I think this book could be seen as the (affirmative) answer to that question.
I don’t think I can agree. Clojure is a functional programming language, but is far from doing any algebra.
[1] https://amturing.acm.org/award_winners/backus_0703524.cfm then click on "ACM Turing Award Lecture" or just -> https://dl.acm.org/ft_gateway.cfm?id=1283933&type=pdf
The historical story is that "functional programming" just meant purity, originally. Now it seems to mean purity + higher order functions + other strong, fancy types (which I'd claim include algebraic structures such as monads).
This current meaning, exemplified by the ML/Haskell tradition, spiritually comes from Peter Landin's ideas in his paper "The mechanical evaluation of expressions" and its supporters don't revere Backus. Sure, algebraic laws characterise monads etc., and his work was foundational—but the Turing Award paper is not a script that everyone is following.
On the specific topic of deriving programs with algebra, there is the book "Algebra of Programming" by Bird and de Moor from the 90s, (https://themattchan.com/docs/algprog.pdf) but it is difficult to look at the functional programming scene now and conclude that deriving your program algebraically is a more essential aspect of the activity than using referentially transparent expressions. It may well be or become an important idea, but it's hardly the bread and butter of functional programming in practice (while maybe in your headcanon it is functional programming). I think part of the problem here is complexity/irregularity: it's simply not practical or helpful to describe typical desired systems algebraically and then derive code from that description.
Yah, that's my point.
> it is difficult to look at the functional programming scene now and conclude that deriving your program algebraically is a more essential aspect of the activity than using referentially transparent expressions.
Again, that's my point. It's not now but it should be. We are missing out.
It's like we are still using Roman numerals even though the Indo-Arabic numeral system has been invented and is ever-so-slowly diffusing into common knowledge.
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/
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.