In JavaScript: The Good Parts by Douglas Crockford, he mentions in his inheritance chapter,


  The other benefit of classical inheritance is that it includes the specification of a system of types. This mostly frees the programmer from having to write explicit casting operations, which is a very good thing because when casting, the safety benefits of a type system are lost.


So first of all, what actually is safety? protection against data corruption, or hackers, or system malfunctions, etc.?

What are the safety benefits of a type system? What makes a type system different that allows it to provide these safety benefits?

Type systems prevent errors

Type systems eliminates illegal programs. Consider the following Python code.

 a = 'foo'
 b = True
 c = a / b


In Python, this program fails; it throws an exception. In a language like Java, C#, Haskell, whatever, this isn't even a legal program. You entirely avoid these errors because they simply aren't possible in the set of input programs.

Similarly, a better type system rules out more errors. If we jump up to super advanced type systems we can say things like this:

 Definition divide x (y : {x : integer | x /= 0}) = x / y


Now the type system guarantees that there aren't any divide-by-0 errors.

What sort of errors

Here's a brief list of what errors type systems can prevent


Out-of-range errors
SQL injection
Generalizing 2, many safety issues (what taint checking is for in Perl)
Out-of-sequence errors (forgetting to call init)
Forcing a subset of values to be used (for example, only integers greater than 0)
Nefarious kittens (Yes, it was a joke)
Loss-of-precision errors
Software transactional memory (STM) errors (this needs purity, which also requires types)
Generalizing 8, controlling side effects
Invariants over data structures (is a binary tree balanced?)
Forgetting an exception or throwing the wrong one


And remember, this is also at compile time. No need to write tests with 100% code coverage to simply check for type errors, the compiler just does it for you :)

Case study: Typed lambda calculus

Alright, let's examine the simplest of all type systems, simply typed lambda calculus.

Basically there are two types,

Type = Unit | Type -> Type


And all terms are either variables, lambdas, or application. Based on this, we can prove that any well typed program terminates. There is never a situation where the program will get stuck or loop forever. This isn't provable in normal lambda calculus because well, it isn't true.

Think about this, we can use type systems to guarentee that our program doesn't loop forever, rather cool right?

Detour into dynamic types

Dynamic type systems can offer identical guarantees as static type systems, but at runtime rather than compile time. Actually, since it's runtime, you can actually offer more information. You lose some guarantees however, particularly about static properties like termination.

So dynamic types don't rule out certain programs, but rather route malformed programs to well-defined actions, like throwing exceptions.

TLDR

So the long and the short of it, is that type systems rule out certain programs. Many of the programs are broken in some way, therefore, with type systems we avoid these broken programs.
