Dynamic 'types' are not types, they're tags [1]. Their function, to determine what to do with a piece of data passed to a function at runtime, is common to both so-called statically and dynamically typed languages. The actual function of types, on the other hand, is to prove simple propositions about a program without running it. This feature is unique to statically typed languages.
This is the problem with this entire debate. People act like there are two sides arguing from positions of equal merit. That is not the case. One (static) is a strict superset of the other (dynamic).
Now you're confusing the implementation with the abstraction. Types can be modeled by tags. They can be modeled by trees. Or any other data structure that you can analyze with a program.
>The actual function of types, on the other hand, is to prove simple propositions about a program without running it.
The value of a tag proves something about the program. You're just proving it at run-time rather than compile time.
Which is an artificial distinction anyway, since your static types theorems are being proved during the run-time of your static type checker. All theorems are proven during some run-time.
This is the problem with this entire debate. People act like there are two sides arguing from positions of equal merit. That is not the case. One (static) is a strict superset of the other (dynamic).
[1] https://en.m.wikipedia.org/wiki/Tag_(programming)