[pjc50]

Types are not for efficiency of programmer or machine, they're for correctness. They're a form of test that can be run statically on the program. And unlike tests, they potentially offer a proof that some kinds of error cannot occur.

Without types you end up with a different sort of monstrosity - the corner cases that you get when comparing ints to strings in Javascript, for example.

[pitaj]

That's a bad example, as it has really nothing to do with types, but instead the semantics of the coercion-implicit equality operator (==) vs the strict equality operator (===). Javascript has types, they are just dynamic, tied to values, not variables.

[edejong]

I don't think it's such a bad example. In a strongly typed language, it would be relatively difficult to 'type' the '==' operator which would be reflected by its horrific signature. The '===' operator, especially in language supporting type classes, would instead be relatively easy to define. The type indicates whether a concept, which might seem simple, is complex.

However, where static languages are lacking is in supplying proof of the rules associated with these operators. In the case of equality, that would be associativity, reflexivity and transitivity.