10

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:

  1. What other branches of mathematics are important to a strong understanding of Haskell's type system?

  2. 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.

Improve this question
4
  • 4
    The category theory stuff isn't essential to knowing and working with Haskell, but it can help with some foundational concepts. The only real branch of math to understand this stuff from is the Category Theory stuff, it's not only rooted there, but therein you'll find little dependence on other maths, it's a very isolated area in that way. Pick up Lambda calculus and study the different type systems associated with different lambda varients, and other than that read this SO answer and read about category theory.
    – Jimmy Hoffa
    Commented Oct 3, 2013 at 19:34
  • 3
    I wouldn't get so caught up with mastering the underlying type system. At least don't let not knowing everything stop you from completing a couple projects. Just completing a few simple projects in Haskell has allowed me to see the mathematical beauty behind it and has driven me to understand it.
    – ChaosPandion
    Commented Oct 3, 2013 at 20:19
  • 2
    @ChaosPandion I agree with that point of view, but I've been working on a project that may require writing code in the ST monad. It's tricky to write code that will compile when I don't understand all of the relevant type signatures, so I felt improving my understanding of the type system would be prudent.
    – Rob
    Commented Oct 3, 2013 at 20:56
  • 3
    @robjb - I certainly agree with you that a deeper understanding is prudent. Honestly my comment was directed more at the general audience who might find Haskell too intimidating to even try.
    – ChaosPandion
    Commented Oct 3, 2013 at 21:02

1 Answer 1

Reset to default
11

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.

Improve this answer
3
  • A brief description of Agda and Coq would be useful.
    – ChaosPandion
    Commented Oct 4, 2013 at 2:55
  • @ChaosPandion Updated
    – daniel gratzer
    Commented Oct 4, 2013 at 3:00
  • That seems good. I figured just saying the names won't be enough to pique the interests of many people.
    – ChaosPandion
    Commented Oct 4, 2013 at 3:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.