A good way of getting at this is to call things at runtime "classes" or "tags" to make it apparent that their discrimination happens at runtime, not compile-time. The problem is that if you call both things types, you quickly run into a situation where you are essentially talking about different concepts entirely.

Note that most sum-types are implemented by having a runtime tag on which you can discriminate.

Classes exist statically also. Tags are meaningless outside of implementation discussions.

I don't think type theorists reject that at all. They just don't call them "types". Which I don't know why anyone would care in the context of a technical argument.

If an "average programmer" here and a type theorist spent 1 minute at the beginning of the conversation normalizing terms then nobody would have any argument here. I don't think anyone tries to claim that "types" and "static types" (or, in the type theorist's parlance, "tags" and "types") are the same... they just try to argue whether or not it's "right" to call one or the other by the name "type".

Most type theorists reject that dynamic typing is meaningful and not a misnomer, hence Noel Welsh's assertion that Python has only one type. It doesn't start the conversation off very well.

I don't think anyone argues that Python has more than one (static) type. It however has a dynamic type system. Significantly, static types and dynamic types do not behave the same way and their corresponding theories have somewhat minor overlap.

In particular, many things I can state about static types do not carry over to dynamic types and visa versa.

I believe many conversations get derailed early because among static type researchers, static types are known merely as "types" and dynamic types as "tags" or "classes". There are meaningful ways to compare these two kinds of things but somehow or another they ought to have different words since confusing the concepts will inhibit understanding quite severely.

Did you mean that to be a restatement of what tel said? It seems to be.

All but the "if we just listened to each other, we'd understand each other." The type theorist's and programmer's different perspective s means basically that we'd fight over the meaning of type for our entire conversation.

It wasn't "if we listened", but "if we normalized terms". I agree that getting people to normalize terms with the aim of successfully communicating can be difficult...