I read a well considered article by Mark Chu-Carrol about the static types debate today. This made a nice change from the typical talking across each other that goes on when this discussion comes up:
My number one preference: strong static typing. That's part of a more general preference, for preserving information. When I'm programming, I know what kind of thing I expect in a parameter, and I know what I expect to return…
…This is my preference. I believe that it's right, but I also believe that reasonable people can disagree. Just because you don't think the same way that I do doesn't mean that you're an idiot. It's entirely possible for someone to know as much as I do about programming languages and have a different opinion. We're talking about preferences.
I value good static type systems. I have enjoyed writing programs in Haskell and F# and dabbling in Roy. And yet, the languages I have chosen to do much of my programming lack this powerful facilityi. For instance my current language of choice, Clojure.
I do not discard a type checker lightly, but it is not the sole defining feature of any programming language. Based on my own preferences, and the type of work I typically do (which is to say, a lot of stuff in the web), other features trump the lack of static types.
Doing web programming, much of the software I write handles very ephemeral data: it passes briefly into my code from external environments such as an HTTP request, or database queries. This diminishes the value of (static) types for me; were I to be working in another context, this would change.
Language choice comes down to many factors (such as tooling, libraries, idioms, packaging and deployment etc), of which types is only one. Like everything it is a trade off. Perhaps in the future I will be able to have my cake and eat it too with the typed-clojure project.
One notion that comes up when people familiar with Type Theory talk about languages is that dynamic types is a misnomer and that the type system of these languages is a strict subset of a real type system. This type is known as the universal type.
Indeed, by the formal definition of types outlined in Type Theory, a type is always static. So called dynamic types are sometimes referred to as tags. This massive discussion of types from Lambda: The Ultimate covers this in detail.