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.

[kmillikin]

I think "might plausibly be" was part of my informal intuition behind the rules. The rules themselves are intended to define the relation.

[carljm]

I think #1743, if merged, covers the "glossary and introductory text" as well as an effort to make the rest of the spec align with those terms.

There are some things I would want still want to add, beyond that PR, before I would call this issue complete. One is a clearer discussion of variance (with reference to the core theory in #1743), and glossary entries for "variance", "covariant", "contravariant", "invariant". PEP 483 has this discussion, but I didn't fit it into #1743 in order to keep the PR to a more reasonable size.

There will probably be others I'll think of later.

[carljm]

I haven't thought of any others yet (or if I did, I forgot to make note of them.) I think it'll be clearer to have specific issues for each further area we want to clarify, and consider this issue to be closed by #1743.

I opened #1797 for clarifying variance.