It's a technical term so the colloquial definition has little relevance to it's use in computing. You can read the definition in TAPL or PFPL.

> tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.

> It's a technical term so the colloquial definition has little relevance to it's use in computing. You can read the definition in TAPL or PFPL.

Technical books often define terms in a way convenient for the material and approach they are presenting, not in a way that is general to the field; particularly, if terms are used in different ways within the field at the time they are written, they typically have to choose for consistency within the book -- that doesn't make that definition the right one for the field, it simply means that's what the term means in the context of the work.

And, ultimately, the semantic argument is meaningless. It doesn't really matter whether you have static and dynamic types in different languages or you call the former "types" and the latter "tags" (except that the former terminology actually explains the difference in a way that tells you what the difference is every time you use the terms.) The substance is the same, and getting worked up over line-drawing regarding the boundary of "type" is a distraction from any discussion of substance.

Type is pretty much used by most programmers to mean "type" as it is stated in the dictionary; so dynamic type checking is not a misnomer to them. Only type theorists are diligent about the colloquial definition, but they can only really use it like that when talking to other type theorists.

Well, if the other person doesn't at least understand that much, speaking to them is probably a waste of time anyway.

Yes, perhaps type theorists are best talking to other type theorists and not people who actually program.

Agree.