Lambda the Ultimate

This is a continuation of this discussion. The main points for soft typing are as follows.

• Compile time type checks. Soft typing can catch the same amount of provable errors at compile time as static typing.
• Automatic downcasts. Downcasts are done automatically assuming the program passes type checking. The main argument for explicit casts is that it provides the programmer with more information, but this is a misnomer. One does not have to write down information for it to be shown to him, so long as said information is inferrable. Note: whether or not you believe OCaml doesn't have casting is irrelevant, simply assume that, when I refer to casting, I also mean situations in which it's emulated.
• Unimposing. Unless a piece of code is provably incorrect at compile time, the compiler can insert runtime checks.