Typing spec: More consistent, formalized language

[JelleZijlstra]

We should work towards a more formalized specification, likely based on Kevin Millikin's "Python Static Types". In particular, a good start would be to add terms like "consistent subtyping" to the glossary and start using them throughout the spec.

[gvanrossum]

Adopting something based on Kevin's spec seems like a very daunting task (and just using a few terms consistently wouldn't do it justice). Where do you expect to find the time? Or who do you expect to help? I personally couldn't even review Kevin's spec.

[JelleZijlstra]

Yes, this is an ambitious issue and probably would take a long time to fully resolve. I think we should start by adding some introductory material that defines terms like "subtyping" and "consistent subtyping" in the context of gradual typing. After that is done, we can make the sections on individual type system features follow the general terminology. In some cases that will just be a clarification, and in others it may bring to light areas where the type system is currently underspecified. (For example, https://discuss.python.org/t/what-are-the-subtyping-rules-for-tuple-t/39837 is something that also led to discussion in Kevin's document; it's something we'll definitely have to resolve if we want to formalize the section on tuples.)

But the initial step should just be glossary entries and introductory text.

[gvanrossum]

Okay, so the initial steps also include using the glossary terms. (FWIW Kevin's definition of consistent subtyping sounds pretty informal, given its use of the phrase "might plausibly be". (Is this just an equivalence relationship that special-cases Any?)

BTW You might want to create an issue for that tuple question.