I appreciate this as a meaningful application of category theory. True, it's being applied to other theory, but that's still an application. And it is useful.

Category theory describes the semantics of Haskell programs, which can do empirically useful things. The theory can be used to prove the correctness of these programs. That's empirically useful!

Category theory describes the semantics of Haskell programs, which can do empirically useful things. The theory can be used to prove the correctness of these programs. That's empirically useful!