* Gregory Collins:
* Andrew Coppin:
Hypothesis: The fact that the average Haskeller thinks that this kind of dense cryptic material is "pretty garden-variety" notation possibly explains why normal people think Haskell is scary.
That's ridiculous. You're comparing apples to oranges: using Haskell and understanding the underlying theory are two completely different things.
I could imagine that the theory could be quite helpful for accepting nagging limitations. I'm not an experienced Haskell programmer, though, but that's what I noticed when using other languages. [Reading TAPL]
Introductory type theory is usually taught in computer science cirricula at a 3rd or 4th year undergraduate level. If you understand some propositional logic and discrete mathematics, then "probably yes", otherwise "probably not."
I think it entirely depends on the amount of work you're willing to put into it. I couldn't bring myself to do it (my copy is mostly unread), but it still helped me to figure out enough of the notation in an emergency. My take on formalization is somewhat unusual anyway---I view it as a necessary evil to ensure intersubjective verifiability, but if you need it to get any results whatsoever, you either don't understand what you're doing, or it's not worth doing in the first place because you're restating trivialities in a pompous way.