Haskell is a pretty fun language to learn and if you’re interested in trying to translate concepts from category theory into programming, it’s probably a good language to use.
Haskell is not category theory in the same sense that arithmetic is not group theory: there’s only really one category. Well sort-of because type constructors let you work in different subcategories.
Category theory is about different categories and the nature of the relationships between them. It usually operates at a level of ‘let C be a category…’ with concrete categories or functors being examples. Haskell operates at a level even more concrete than single objects in a single category: the objects are types and Haskell operates on the values of those types. Of course Haskell can work at slightly higher levels too, but it never really escapes categories that look a lot like Hask.
Maybe that statement is too strong though. I’d be keen to see some interesting actual-category-theory level things in Haskell. (Maybe I’m being unfair and these do exist but I am considering them to not count as ‘actual category theory’)
I thought that the ‘categorical theory of patches’ thing was a good example of category theory applied to programming but note that it didn’t require any kind of general notion of e.g. push-outs in a programming language.
Haskell is not category theory in the same sense that arithmetic is not group theory: there’s only really one category. Well sort-of because type constructors let you work in different subcategories.
Category theory is about different categories and the nature of the relationships between them. It usually operates at a level of ‘let C be a category…’ with concrete categories or functors being examples. Haskell operates at a level even more concrete than single objects in a single category: the objects are types and Haskell operates on the values of those types. Of course Haskell can work at slightly higher levels too, but it never really escapes categories that look a lot like Hask.
Maybe that statement is too strong though. I’d be keen to see some interesting actual-category-theory level things in Haskell. (Maybe I’m being unfair and these do exist but I am considering them to not count as ‘actual category theory’)
I thought that the ‘categorical theory of patches’ thing was a good example of category theory applied to programming but note that it didn’t require any kind of general notion of e.g. push-outs in a programming language.