2 ms·
'Category theory is fine but won't give you "anything new"'. This is far from the truth and disregards a significant body of work in programming language theor
by bhewer 7y ago
'Category theory is fine but won't give you "anything new"'.
This is far from the truth and disregards a significant body of work in programming language theory (not to mention algebraic geometry and topology).
Perhaps most famously, monads, which have been widely adopted in the Haskell and Scala communities, originated in the category theory literature. Eugenio Moggi famously described how monads could be used to structure the denotational semantics of a programming language.
Monads are just the most obvious example of 'new' concepts which originate in the category theory literature and are practically realised by the study of categorical semantics of programming languages. A brief investigation of the literature will reveal a vast array of concepts such as initial algebras/final coalgebras (used to implement safe recursion schemes), adjunctions (giving rise to free constructions such as the infamous free monad), profunctor optics (bidirectional data accessors). This is just to give a few examples in PLT and does not even touch upon lesser-known constructions in type theory.
‘In the end, it's a nice theoretical framework to think about how to structure your code but that's it.’
This comes across as overly dismissive of the problem of ‘how to structure code’, which is in no way trivial. Formalising desirable properties of programs, and designing languages/constructs which restrict to programs exhibiting these desirable properties, is a general focus of programming language theory. ’A nice theoretical framework’ in which such problems can be formalised is very significant, and the comments that programming language theorists working on categorical semantics are “incredibly smug and toxic” and “are just trying to get some traction to keep leeching off grants” is especially insulting to many wonderful people working in this domain.