Here’s a great quote from Yaron Minsky about the use of types in functional programs.
[…] most of the advantage of types in a language like ML comes from completely vanilla uses of the type system. One of our programming maxims at Jane Street is to “make illegal states unrepresentable”. Algebraic datatypes, parametric polymorphism and abstraction can be used to great effect in this regard.
I think that people who are new to ML think of the type system as merely a constraint, that is to say, you write code as you did before, and then you see whether the compiler accepts it. As people get more experienced, they start to use the type system as a tool in its own right, and one of the things that is constantly on one’s mind is how to pass off as much of the proof burden as possible to the compiler. Most of this work can and should be done using boring old vanilla ML types.
This is a wonderful point. From the outside, the type systems of languages like Haskell and ML tend to look like a sort of archaic ecstatic religious rite. The bleeding mendicants pause as they shuffle past, sing a verse in praise of the purifying pain of strong typing, then prod themselves with pointy sticks and progress along their lonely road.
In practice, though, the type system is a powerful tool that helps to prevent mistakes, by forcing you to do some thinking up front. It’s not something you put up with; it’s something you value, albeit after a while.
One of the difficulties of crossing the Rubicon from type system outsider to insider is that it’s hard to find motivating examples in small, easily understood chunks of code, the sort of code that one writes as a beginner. The value doesn’t really begin to accrue until you’re either writing something moderately complex or refactoring existing code.