I'm learning category theory to understand haskell better.
I'm finding category theory to be almost a theory about program structure in the context of composition. It's giving me a whole new perspective on one of the least concrete things about programming namely design.
How relevant is abstract algebra to programming? Will it change my perspective on everything related to programming? How much of a mind bender is it compared to category theory?
> I'm learning category theory to understand haskell better.
I would consider myself a fairly expert Haskell programmer and I have (for fun/curiousity) spend some time reading up on/studying category theory and I can say, without a doubt or hesitation that if your goal is to either 1) understand Haskell better and/or 2) become better at writing Haskell, then studying category is a MAJOR waste of your time. I would advise you to spend that time instead on reading up on the lambda calculus, type theory, and some basic algebra (like this post).
Haskell is not/has never been based on category theory (and I keep being baffled by how many people on social media will claim that it is, given how well documented it's origins are) and the common terminology of Functor/Monad that have been pilfered from CT via Wadler have only a passing resemblance/relation to their CT friends.
Some things that I instead would recommend reading up on are:
- Type theory (Benjamin Pierce's "Types and Programming Languages" is the de facto introduction to this. It covers everything from untyped lambda calculus to things way more complex than standard Haskell, including example implementations of type checker, etc.)
- Computer assisted proofs/formal verification of programs (the Software Foundations book series, co-authored by Pierce are a good (and free!) intro: https://softwarefoundations.cis.upenn.edu/)
- The Spineless Tagless G-machine (if you are a more low level/C minded person, this talks about how we compile a lazy functiona language like Haskell to an Intel CPU: http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.37...)
- The Typeclassopedia (which talks about how various CT inspired classes relate to each other and their laws: https://wiki.haskell.org/Typeclassopedia)
EDIT: All of the above is not to say that you shouldn't learn category theory, but that you should have realistic reasons/expectations (even if that reason is just "I'm curious and it's cool"). I just hate seeing people get burned out trying to "get" category theory and (as a result) deciding Haskell must not be for them...
ugh, I see HN bollocksed my list and I can't edit it to fix it, so repeated for readability:
- Type theory (Benjamin Pierce's "Types and Programming Languages" is the de facto introduction to this. It covers everything from untyped lambda calculus to things way more complex than standard Haskell, including example implementations of type checker, etc.)
- Computer assisted proofs/formal verification of programs (the Software Foundations book series, co-authored by Pierce are a good (and free!) intro: https://softwarefoundations.cis.upenn.edu/)
Your insight is valuable and interesting. I'm certainly not an expert on Haskell and I'll take a look at your book recommendations. Thank you.
I have to say though I can't agree with you on category theory yet. Especially the part about functors. The fmap for the functor f looks to me to be 100 percent the definition of the morhphism that maps arbitrary categories to the morphisms in functor f. The resource I am reading on category theory makes it seem highly relevant to Haskell and software design in general. I'm curious as to your opinion on why the functor in Haskell only has a passing relationship to functors in category theory.
> I'm curious as to your opinion on why the functor in Haskell only has a passing relationship to functors in category theory.
If we assume Hask, the universe of Haskell types and functions operating, is a category (which is hotly debated with some regularity, as there is no formal definition of Hask). Then the Functor class in Haskell really only describes one specific subset of functors: endofunctors on Hask (i.e. mapping objects (types) in Hask to objects in Hask).
This is a rather limited subset of all functors. You can also see this in the laws for example. You probably know the 2 functor laws "fmap id x = id x" and "fmap f . fmap g = fmap (f . g)", but Haskell's Functor is limited enough that these are actually redundant. In Haskell having a proof of just 1 functor law gives you the other one for free (as a free theorem, Wadler's "Theorems for Free!" is a good intro, and another paper. It basically covers "why is more generic code easier to reason about").
> The resource I am reading on category theory makes it seem highly relevant to Haskell and software design in general.
I'm not saying there aren't some useful ideas to be gleaned at both the superficial and deeper levels. The whole lawfulness of functors is great for being able to reason about code without knowing what it actually does, and all of lens is deeply inspired by category theory.
All of CT is about composition and reasoning about it, which we could certainly use more of in programming. So I encourage anyone curious to look into. I'm just trying to provide some nuance to the...enthusiastic overhyping of CT, because I don't want people to be scared away of wonderful tools and languages like Haskell, just because they think they're not smart enough to get all that fuzzy math :)
>If we assume Hask, the universe of Haskell types and functions operating, is a category (which is hotly debated with some regularity, as there is no formal definition of Hask).
Isn't the consensus that "Hask is a category as long as you wave your hands profusely and pretend that exceptions and non-terminating functions never happen"?
I'm finding category theory to be almost a theory about program structure in the context of composition. It's giving me a whole new perspective on one of the least concrete things about programming namely design.
How relevant is abstract algebra to programming? Will it change my perspective on everything related to programming? How much of a mind bender is it compared to category theory?