I'm aware the Haskell designers like category theory, and so yes, the question boils down to the degree of influence of category theory on particular language features.
Still, to your last point, the existence of an equivalence doesn't automatically count as an application of all sides of the equivalence. Coming up with a post-hoc math explanation for some practical idea doesn't make the practical idea an application of the math. The practitioners have to adopt that framing or rely on theorems proved via the math that they didn't otherwise rely on. It would be like saying that all mathematical theorems are an "application" of the typed lambda calculus because of the Curry–Howard correspondence. It's a disingenuous and fruitless way to think about what it means to apply an idea to solve a problem.
Automated theorem verification may use category theory (does it?), and I'd love to talk to the main contributors to Lean, which appears to be the system that's gaining the most traction among average mathematicians, to discuss that.
> I'm aware the Haskell designers like category theory, and so yes, the question boils down to the degree of influence of category theory on particular language features.
So, if only a segment of Haskell's language design is based on Category Theory (CT), and only a fraction of popular programming languages are based on Haskell, then this percentage, possibly in the single digits for a given mainstream language, is too minor for you to consider it a valid application of CT. That's a valid perspective; I'll leave it at that.
> Still, to your last point, the existence of an equivalence doesn't automatically count as an application of all sides of the equivalence. ... The practitioners have to adopt that framing or rely on theorems proved via the math ...
I really don't agree with your definition of application. If I have an equivalence between three different concepts - types, propositions, and objects within CCC, then, in my viewpoint, you don't need to explicitly consider your application of a concept in the other two fields for it to be recognized as an application. To me, that's akin to saying that you can only do math in a certain way, exactly how mathematicians portray it in their textbooks. If you don't know that because you learned math more indirectly, like from programming blogs with code snippets that encapsulate the same definitions, then, according to that view, you won't be doing applied math.
To me, it simply boils down to a different perspective on the term application, one that isn't specifically about CT.
> Automated theorem verification may use category theory (does it?), and I'd love to talk to the main contributors to Lean
I have listen to some podcasts with the main contributors and creators of Lean. Lean is based on (Lean's kernel) homotopy type theory (a flavor of type theory – specifically of intensional dependent type theory).
> most traction among average mathematicians
Yes. Many math graduate students are using Lean to apply concepts from textbook math, such as HoTT, which has a strong connection to Category Theory. Basically, you can't read the HoTT book without knowing CT, and can then apply it in Lean. I think this would even satisfy your definition of applied math.
Still, to your last point, the existence of an equivalence doesn't automatically count as an application of all sides of the equivalence. Coming up with a post-hoc math explanation for some practical idea doesn't make the practical idea an application of the math. The practitioners have to adopt that framing or rely on theorems proved via the math that they didn't otherwise rely on. It would be like saying that all mathematical theorems are an "application" of the typed lambda calculus because of the Curry–Howard correspondence. It's a disingenuous and fruitless way to think about what it means to apply an idea to solve a problem.
Automated theorem verification may use category theory (does it?), and I'd love to talk to the main contributors to Lean, which appears to be the system that's gaining the most traction among average mathematicians, to discuss that.