[dmytrish]

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

[chongli]

That's not quite true: there are many types, but the type checking is delayed into run time.

Runtime checks are not type checks[0], they are class checks.

[0]. https://existentialtype.wordpress.com/?s=dynamic+typing

[seanmcdirmid]

You mean in Bob Harper's opinion?

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.

[chongli]

You mean in Bob Harper's opinion?

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!

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