Encoding an invariant in the type system is definitely a strong benefit of Haskell and other similar languages. You can do more than simple identity/immutabilit

Encoding an invariant in the type system is definitely a strong benefit of Haskell and other similar languages. You can do more than simple identity/immutability with types. I find the flexibility of the type system to share some similar properties with C++'s more advanced features. Used sparingly they can be quite powerful but come with a complexity that few mortals will be able to comprehend. In a distributed system, for example, you can encode an invariant in the type system that will constrain the execution to only valid states. This is immensely powerful. However you can also model arbitrarily complex computations into the type system which will make sense to no one but the author who wrote it. One thing I do miss in Python that a type system gives you is the compiler's ability to do exhaustive pattern matching. Forcing you to deal with every case explicitly is a huge advantage. In fact, I'm currently working on a formal specification of eventlet's Semaphore class as an exercise (I'm in the process of learning) as we've found just such a bug in a large Python code base where a particular exception is not caught and locks up the whole system. An exhaustive pattern search would have forced the authors to deal with that exception and this bug wouldn't have surfaced.