While this is technically correct (the best kind of correct) it also trivializes the argument and somewhat misses the point. For example, in a dynamic language all the values are belong to a single type and carry a tag at runtime to identify their category. Static languages also do that but on more restricted scope - you aren't allowed to accidentally mix strings and integers in Haskell but you can accidentally mix empty/non-empty lists (getting a runtime exception on `head`) or zero/nonzero numbers (breaking division). You can sort of fix this if you go up to dependent types but then the type system gets much more complicated and its not always easy to statically create the proofs for everything so you start to see the appeal of dynamically checking some of the stuff.
Haskell but you can accidentally mix empty/non-empty lists (getting a runtime exception on `head`) or zero/nonzero numbers (breaking division).
This is due to Haskell's support for partial functions. It does induce some weakness in the type system but it brings the benefit of making the language Turing-complete. As for these specific examples, they would be solved if the libraries in question were rewritten.
The problem is that you might be forced to add dependent types to the language to be able to safely define some of those partial functions. This is not a trivial matter since dependent type systems are even more complicated and might demand extra work (proofs) from the programmer.
IMO, there are situations where you are better off doing trivial runtime checks instead of trying to write complex proofs that might themselves contain bugs and that are tightly coupled to your current implementation and choice of datastructures.
An idealized dynamic strong typed language can actually give you the guarantee that all statically valid programs give you well-defined runtime behavior. This is a huge advantage over weakly typed languages that you also get out of the idealized static typed language.
The issue is, outside of languages with very baroque type systems or monstrosities like Java's sandbox, static typing often winds up decaying into weak typing, which offer much weaker behavior guarantees than real-world dynamic languages.
That's not quite true: there are many types, but the type checking is delayed into run time. Though your point of view may be also correct with respect to definitions (if you assume that types exist only during compile time).
Dynamic type checking is a useful concept when classifying languages, but it might not be sensical with respect to certain narrow definitions of what a type system should be.
Yes, shocker of shockers, I agree with Bob Harper. The term type comes from type theory which is an entire discipline (as far as computer languages are concerned) based on the idea of propositions as types. If types are propositions, then what are programs themselves? Proofs of those propositions, of course, with the type-checker doing the work of checking the proofs. With so-called dynamically typed languages you do not have that. What you do have is dynamic dispatch based on the class of a value. This has nothing to do with types!
The term type actually originates way before that, the 19th century meaning is "category with common characteristics", which is how we use the word in normal discourse (Python is a type of programming language....).
Bob Harper has adopted a very narrow definition of type based on one discipline, type theory, but the word "type" itself is much more general than that. I definitely use the word "type" when talking about my Python programs, even if there are no static type theoretic types to be seen.
In a dynamically typed language, your proofs are checked at run-time, which has everything to do with types! Getting a type error at run-time is much better than having the program keep going and produce a wrong result (if it doesn't core dump via memory corruption first).
Getting a type error at run-time is much better than having the program keep going and produce a wrong result (if it doesn't core dump via memory corruption first).
To me that's akin to an airplane ditching in the ocean rather than slamming into a building. Sure, it saved a lot of lives but it'd have been better to solve the problem while it was still on the ground.