I am aware that some type theorists insist on this distinction and it does have some some merits, but (afaik) type theorists didn't invent the word "type" and "

I am aware that some type theorists insist on this distinction and it does have some some merits, but (afaik) type theorists didn't invent the word "type" and "runtime tags" are commonly and widely known as "dynamic types", even if they do work quite differently from static ones, so I always feel that insisting on this distinction is somewhat pedantic. But yes, arguing about semantics never got anyone anywhere, what I wanted to highlight was that it's not just coincidence that interpreted languages are by and large dynamically typed.