1. I like to refer to some programming languages as “timebomb-typed” and “timesink-typed” in addition to the more conventional division between dynamically-typed versus statically-typed, and the more vague division between “weakly”-typed versus “strongly”-typed languages.

Timebomb typing refers to type systems that do very little at compile time to guard against programmer errors of the kind that could be caught by a type system. Catching programmer errors is, after all, the primary function of a type system; the computer doesn't need it. The ‘timebomb’ refers to the fact that you never know when the program will crash or cause something nasty to happen due to an error that could have been caught by more scrupulous compile-time type checking. Timebomb-typed languages obviously include all dynamically typed languages, as well as quite weakly statically typed languages. Popular examples of the first kind are, of course, Perl, Python, Lua, Ruby and so on, while the latter kind is primarily represented by C and C++.

Timesink typing typing refers to type systems and languages that can catch programmer errors at compile time, but demand time and effort from the programmer in order to do that. Most statically typed imperative languages fall into this category. The already mentioned C and C++ are rather lightly timesink-typed, and languages such as Java are heavily timesink-typed.

Timebomb-typing and timesink-typing are thus not mutually exclusive, but they also do not cover all languages. A third relatively unknown category exists. It might in contrast to the former be called timesaver typing. This refers to (rather strongly) statically typed languages that do not demand time and effort from the programmer to help catch his errors and that consequently reduce time wasted on debugging too. The term refers to type systems that allow type inference. This means that the compiler can infer the type of an expression without the programmer having to write type signatures. Timesaver-typed languages primarily include functional programming languages whose type systems are based on the Hindley-Milner type system: Haskell, OCaml, SML, Clean, and so on, and on the imperative side, at least Nemerle (which also borrows such conveniences as first class functions and tagged unions with pattern matching from the functional world, but unfortunately falls victim to the .BLOAT framework) and Boo (dot-BLOAT as well). Some other imperative languages provide rather limited forms of type inference.

As an example of type inference, I might write the following declaration in Haskell to form the sum of a list of numbers:

sum [] = 0
sum (x:xs) = x + sum xs

Because the compiler knows that the + operation is defined for numbers only (of varying kinds, more specifically members of the Num type class), as 0 is also a number, and thanks to the list pattern matching constructs in the definition, it can infer that sum can only work for lists of numbers, and returns a number. If I wanted to, I could give the type signature

sum :: Num a => [a] -> a

(where a is a type variable) or specialise the function to (machine) integers only with

sum :: [Int] -> Int

Just like in dynamically typed languages, such definitions are however not needed; the compiler can infer them itself (unless you use some more advanced type system hacks). Customarily type signatures are nevertheless given for top-level symbols as a form of documentation.

It should be noted that most practical languages do allow for some sort of dynamic typing, so even the above-mentioned languages do have aspects of timebomb typing. The use of such facilities should, however, be rather the exception than the rule, unlike in languages that only do dynamic typing. The definition of timebomb typing is also a relative one. There are actually type systems relative to which the Hindley-Milner type system is rather weak, namely dependent type systems of such (prototype) languages as Epigram.

2. Dependent type systems are type systems where types can depend on data. With a dependent type system it is possible do such things as encode into the type of a function the relationship between the dimensions of the parameters and the value of the function. For example, the function that returns all but the first element of a finite list of integers (shunning polymorphism here for simplicity), might have the type

tail : ∀n:ℕ ⇒ IntList (suc n) → IntList n

indicating that the length of the parameter list must be the successor of some natural number (the set or type ℕ), or that it can't be zero. (Epigram calls finite lists “vectors”, but I don't like something being called a vector that is not necessarily a member of a vector space.) A slightly more complex and typical example is matrix multiplication:

mult : ∀i,j,k:ℕ ⇒ Matrix i j → Matrix j k → Matrix i k

If you now try to multiply matrices with potentially unmatching dimensions, the compiler (or the interactive editor) will complain of this, before the program is even run, unlike in case of weaker type systems.

It is actually possible to do some “fake dependent typing” with some “type-level programming” hacks using the more advanced features of Haskell's type system, and also with templates in other languages. For such hacks the dimensions and other values must, however, be predetermined at compile time. True dependent typing can work with dynamic dimensions and other data.

Languages with dependent type systems are still at the research stage, and unfortunately full type inference is provably impossible so such languages might fall into the category of timesink typing. Let us wait and see.

3. The point of this story is that, unlike seems to be rather commonly thought, the choice is not between timesink typing and timebomb typing; between dynamically typed languages and writing type signatures; choosing between spending more time debugging and spending time preventing bugs from ever being compiled. There are statically typed languages that do not demand type signatures. Additionally, I've tried to show what kind of programmer errors can potentially be prevented with powerful type systems. Of course, a strong type system can also be suffocating if it is not powerful enough. Java seems to be considered an example of this by some functional programming advocates; personally I'm not experienced enough in Java to comment (I only know enough Java to know that I don't like it).

I'm not saying that timebomb-typed languages should not be used. Some of them have their uses. Dynamically typed languages in particular can be very convenient for quick and dirty scripts. I would recommend against using timebomb-typed languages in big projects, however. In particular I would not use them for code that one should be able to depend on not to crash or corrupt data. An exception to this rule may be some very performance-critical and low-level components, in which case C may be the best choice. Nevertheless, testing is a poor substitute for proving correctness, and the latter is what (static) type systems do, within their expressive power. As for heavily timesink-typed languages, I think most people can stay away from them by themselves, if they have the choice :).