Recently, I’ve become deeply interested in Haskell.
While attempting to learn new concepts (e.g. the forall keyword and ST monad) and Haskell’s type system in general, I continually run into concepts from category theory and lambda calculus. So, I wonder:
-
What other branches of mathematics are important to a strong
understanding of Haskell’s type system? -
Can I forego a rigorous study of these maths and instead focus on certain pertinent concepts? (e.g. quantifiers in lambda calculus.) If so, which concepts are essential?
I’m hoping to pick up Types and Programming Languages soon, however, please suggest any alternative reading resources you feel appropriate.
4
No, you don’t need to pick up a book on category theory to understand Haskell.
I’ve been using Haskell for a few years, and picked up some category theory out of curiosity, it’s really not necessary. On one hand, it’s cool to see how all these abstractions fit in to “the big picture”, but I didn’t go “Oh my gosh I just need to make this a profunctor from the Maybe category to []s and then I can save the princess!”.
Now depending on what you’re doing with Haskell type theory is on the fence.
If you’re just learning haskell don’t go trying to understand every nuance of the type system. Please don’t, it’s like trying to learn C++ template meta-programming first. Fancy types are excellent tools, but having a good understanding of functional programming beats understanding impredicative polymorphism.
Now let’s say after a year or two of Haskell you’re looking to understand every subtle piece of how Haskell’s type system works, then yes, some type theory might be helpful.
It will help you understand some of the logic behind how things work, plus it’s frankly a really cool branch of computer science IMO that is worth looking at. You can cherry pick the parts your interested in and still learn a decent amount.
For Haskell, looking at STLC, HM type systems (System F) and perhaps the lambda cube (Haskell is System Fw iirc) and iso-recursive types. Types and Programming languages is a great resource for starting out and covers all of these and much more.
If you really want to drink the cool-aid and discover you’re a budding type theorist, go poke at Agda or Coq. These feature “dependent types”, one step farther along in the lambda cube than Haskell. Dependent types let types depend on terms. This means the types are powerful enough to actually prove theorems. For the curious, googling “curry howard isomorphism” should bring up some interesting results.
3