Static typing helps catch bugs and code refactoring. For example, if you add a parameter to a function in ML the compiler will point out for you all the call si

Static typing helps catch bugs and code refactoring. For example, if you add a parameter to a function in ML the compiler will point out for you all the call sites that need to be updated to the new API. The compiler will also be smart enough to notice the times when your function is called via aliases, which is something you can't do via textual find-and-replace. The need for type inference is because in languages with more advanced type systems like ML it would be very annoying if you had to write down the types for everything by hand with no assistance from the compiler. > As I understand this - I'm probably wrong but - dynamically type == type inference. No, this is only a common misconception. The better analogy is "dynamically typed" == "everything belongs to a single type". In Python every value has a type of "object" and can be passed to anywhere you want. The interpreter adds tags to the memory representation of the objects so it knows what to do with them and it raises a runtime error if you try to use a value in the wrong place (for example, when you try to call a method on None). On the other hand, in a language with a sound type system you have a guarantee that there will never be type errors at runtime ("well typed programs do not go wrong"). The type checker enforces that different types never get mixed together, which also removes the need for runtime tags in the memory representation.