[seanmcdirmid]

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).

Dynamic dispatch doesn't even play into it.

[chongli]

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.

[seanmcdirmid]

Whether you think ensuring safety later rather than earlier is a good or bad thing is kind of irrelevant; the fact is that one can still technically check type properties at run-time. Pragmatically speaking, even Haskell must rely on a few run-time checks to ensure complete type safety (e.g. match not exhaustive exceptions...).