Whose type system is it anyway?

A complaint that I used to hear from programmers who prefer dynamically-typed languages is that typing is "satisfying the whims of the compiler", or words to that effect.

Haskell programmers (or, in general, those who use Hindley-Milner-esque type systems; O'Caml programmers probably know the Zen) know that this isn't true. What seems like satisfying the compiler is, in fact, debugging. Moreover, it's removing bugs that the compiler finds for you. What's not to like about that?

But it occured to me recently that if you're not using a Hindley-Milner-like type system (say, an Algol-like type system), then this accusation is entirely correct.

In HM systems, you don't have to declare the types of variables. It's been a while, but I seem to recall that this took some getting used to. Even in those rare situations when the type inference system needs some help (e.g. advanced Haskell type hackery), it usually doesn't need to know the types of any variables as such; giving a type declaration for the function as a whole, or maybe a let-binding or two, is sufficient.

In retrospect, this property of HM isn't quite so remarkable. Yes, the whole type system is designed around this property of there being a single most general type for every lambda-expression. But what this strongly suggests is that all of those type declarations that you're writing in C or Java are, in a sense, superfluous.

OK, maybe that's a bit strong. C gives you implicit type coercions, and Java gives you a form of polymorphism that Haskell doesn't. But still, coming from Scheme, I can see how you might think that declaring all those variables really is satisfying the whim of a compiler that is too dumb or haughty to do that routine grunt work for you.

So perhaps we shouldn't be too hard on dynamic typing advocates. I don't think like them, since I'm too brainwashed into HM languages. But putting myself in their shoes, I can imagine looking at the type declarations in Algol-like languages with something akin to horror.

So rather than debate static-vs-dynamic, typeful programmers should be concentrating static-vs-static. Who was your type system designed for? For you, the programmer, or for the compiler writer? Does it serve you, or does it make you hold the hand of you insufficiently smart compiler?