Hacker News new | ask | show | jobs
by throwaway17_17 1000 days ago
I would argue that the last 30 years (if you arbitrarily begin at Moggi’s paper on Monadic computation). Have shown ample impact of category theory on programming language theory and type theory more generally. Additionally, there are earlier work on the semantics of programming languages dating to the early 80’s with strong category theory roots. There is a large body of work (I’m on mobile and don’t have links) that uses category theory to backstop the development of algorithms and generic code solutions for all types of algebraic data types and container types for instance.

There is a thriving ‘school’ of computer science that views category theory as the third leg of the category theory, type theory, proof theory triangle that forms their basis for all computer science. This is very evident in the CS department at Carnegie-Mellon. If you are interested I’d recommend checking the backlog of lecture videos and presentations at the Oregon Programming Language Summer School program.

1 comments

Turing award winner Dana Scott already mentions categories in his work on models for the untyped lambda-calculus, for example in his 1971 monograph on Continuous Lattices, which set the foundations of domain theory. Moggi monads came about, in parts, as a way of understanding domain theoretic constructins better.