Types are not just about ruling out invalid expressions, they also *add* information. The type of a variable can determine what piece of code to run in a given expression. This is type-based dispatch, as opposed to value based dispatch (vtables).
Take a function like "read :: Read a => String ->a" in Haskell. It will parse any value of a type that's in the Read class. You don't nead a readInt, or readFloat etc., the type of the *result* of read is used to determine which specific parser to use. A
dynamic language can't do that - it doesn't know the type of the result until after the function has executed, but it doesn't know which function to execute since it depends on the result type!
That type is in turn determined from the context. This really starts shining when you compose it together, e.g. this function which reads a space separated list of values:
readSpaceSeparatedList :: (Read a) => String -> [a]
readSpaceSeparatedList xs = map read (words xs)
Now you can read a list of Ints, or Floats, or MyUserDefinedDataType using the same function. The specific expected type at the call site determines how the parsing happens. And indeed maybe the call site doesn't need to know what the specific type is:
sumSpaceSeparatedList :: (Num a, Read a) => String -> a
sumSpaceSeparatedList str = sum (readSpaceSeparatedList xs)
So again, we've written yet another layer of code and we *still* haven't had to decide exactly what parser to use to read the actual data from the string. We've only narrowed it down to something that's numeric (for the sum). Eventually something will force
it to an Int or Float or something and then the compiler will figure out that it needs to use the Int or Float instance for Read.
Imagine how you'd write that in a dynamic language. You'd need a readInt, readFloat,etc, and similar for the two other functions. Or you'd need to wrap up the parser in an object and thread it through all the functions, but that's hideous (sort of like manual
vtables to do OOP in C).
Anyway, this got longer than intended. The point is that a type system is not just about catching errors - types constitute extremely useful information that can actually be used by the compiler to make decisions, which can let you avoid writing ugly and