Note that the following was hastily written on my lunch break. It doubtless contains some serious errors. Feel free to correct any of my misconceptions.
I've read a fascinating online article about type systems and it's worth reading a few times. While I'm a far cry from an expert in type theory, I'm quite impressed by the article. The author is clearly well-versed in this topic and has clarified quite a bit about the debate, though I'm disappointed that references are generally not cited (though examples abound).
First, here's the author's definition of static and dynamic types:
A static type system is a mechanism by which a compiler examines source code and assigns labels (called "types") to pieces of the syntax, and then uses them to infer something about the program's behavior. A dynamic type system is a mechanism by which a compiler generates code to keep track of the sort of data (coincidentally, also called its "type") used by the program.
In other words, static typing is not about the kinds of data we have, but about the behavior of a system. Of course, this is often tightly related to the kinds of data. For example, asking for the factorial of an IP address doesn't make a lot of sense and for a proper program, won't be allowed in a static system, but it's trivial to generate a failure like this in a dynamic system. Of course, merely because we have safety (often compile-time) about certain failure modes, this does not guarantee the correctness of the program, but certain kinds of bugs are less common.
Dynamic typing, on the other hand, is primary concerned with tracking the kinds of data used and behavior is up to the programmer. It's not about the syntax and the kinds of data generally cannot be statically inferred. This has an interesting consequence that your type system cannot reason up front about the behavior of any given piece of code. For example, consider this pseudo-code:
total = price + tax;
If $tax is the string "fifteen percent", the above code will not perform as expected in a dynamically typed system but the type system has no way of knowing that this condition will not occur and thus cannot warn you about this failure. However, depending about how the dynamic typing was implemented, that code might continue to run or it might crash.
As a more insidious example, imagine trying to do type inferencing in Perl. Does that array reference contain only integers? You can toss a hashref in there and things will crash badly, but an inferencing system probably can't know this will happen. As a result (and as the author points out), testing tends to be more widely adopted in dynamic languages. Many types of tests are useless in solid static languages, but merely because there is some behavioral safety does not guarantee the correctness of the programs.
Moving on, consider three kinds of programs:
Clearly correct software is preferable, but incorrect software which crashes is far preferable to incorrect software which doesn't crash. This perfectly exemplifies a terrible failure mode in SQL:
WHERE age > id
Not only is that completely useless, but it's likely to not crash. Thus, we have reasoning about type systems forced onto the developer when it should be handled by the type system itself. What we want to do is define the kinds of data we handle, the operations allowed with them and the results of those operations. This could allow the database to properly reason about a statement, something they frequently don't do. Thus, since SQL without user-defined types is more concerned about the kinds of data rather than the uses of the data, we can consider this is a very poorly implemented type system (but I've not had enough experience with user-defined types in SQL to know how solid they are).
Another interesting distinction was structural versus nominal typing. In structural typing, we assume a type whenever it is safe to do this (e.g., does it provide what our code needs?). Nominal typing requires this to be explicit. This appears to be very similar to one distinction between mixins and roles (traits). The distinction in question is that a role is named and mixins merely shove methods into your class. As a result, mixins rely on duck typing and hope that the "bark" method really refers to a dog and not a tree. With traits, you can explicitly check the name to have a better sense of safety that the method in question does what you want (it's not perfect, but it's better than mixins). Note that this makes traits similar to static typing, but it's still pushed on the developer, but Perl 6 might alleviate some of that.
Another interesting bit is the discussion of testing. Testing, as we know, doesn't prove the absence of bugs. It merely asserts that under a given set of conditions, certain behaviors hold.
A proper type system, however, can prove that certain types of bugs don't exist (but a given proof can merely show that the conclusion follows from the premises, not that the conclusion is desirable or that the premises are correct). Mark Jason Dominus once pointed out how a type system caught an infinite loop in his program. This is not a well-known feature of good type systems, but it's not unexpected. However, the author goes on to cite examples of type systems used to prove databases are normalized or that a program contains no "index out of bounds" exceptions on arrays, things which most programmers generally don't consider to be part of type systems.
At its core, the article generally defines a type system as a set of syntactic rules which verifies the absence of certain behaviors in a program (meditate about taint checking for a while). The complexity really comes in when we acknowledge that the needed "absent behaviors" vary greatly from program to program. Needless to say, dynamically typed languages leave much of this up to the programmer.
This paper has taught me a lot and reinforced many of my suspicions about type systems. What I think I ultimately want is a sound, implicitly typed language with nominal types, but what I want even more is a paycheck, so I'll stick with Perl for the time being.
It's also worth noting that taint checking and pragrams such as fatal and strict also alter how Perl's type system behaves. Interesting food for thought.