Type introspection is another thing entirely! That's basically reflection, which is nothing to do with anything mentioned so far. To be clear:

* Dynamic typing: types are not known at compile time

* Static typing: types are known at compile time and written down in the source code.

* Static typing with type inference: types are known at compile time and inferred rather than being explicitly written down

* Dynamic typing with type inference: nonsensical; not a thing

* Type introspection: types can be inspected by code at runtime. Unrelated to any of the above. Can be found (or not found) in both dynamically typed and statically typed languages.

Thanks for the overview. I agree with all, except for the "has nothing to do with" claim.

> Dynamic typing: types are not known at compile time.

That is just a top level description of a feature, the tip of the iceberg. What is needed for a language to support dynamic typing? The answer is not "has nothing to do with x" where x is any of the above features.

Also a lot of types are known at compile time even if your language supports dynamic typing.

Also "compile time" is a vague term for an interpreted language, as the machine compatible code is generated at run time.