This is flat out not true. In the academic literature of type theory, "type" has a very particular meaning and is a construct for reasoning about programs befo

This is flat out not true. In the academic literature of type theory, "type" has a very particular meaning and is a construct for reasoning about programs before execution. The community may use "tag" but mostly as a means of distinguishing between "types" in type theory, and a runtime tag. Often the term "dynamic type", or "runtime type" will be used as well all as means of differentiation.