new "type system concepts" section

[carljm]

This is an expanded "type system concepts" document for the typing specification. It intends to improve clarity of the spec by giving definition to important terms that can be used throughout the remainder of the spec. See #1534

This PR largely owes its existence to, and includes some text drawn directly from, https://bit.ly/python-subtyping, authored by @kmillikin. (Any errors introduced are mine.) It also draws on concepts described in PEP 483.

[carljm]

cc typing council members @JelleZijlstra, @hauntsaninja, @gvanrossum, @rchen152, and @erictraut -- I'd be grateful for your review and feedback here.

[kmillikin]

A few quick comments, I'll have more later.

[JelleZijlstra]

Thanks, this looks good

[carljm]

Also cc @superbobry, since you've expressed interest in this area

[erictraut]

@carljm, thanks for taking on this task! This is an important addition to the typing spec. These are foundational concepts. It's important to standardize the terminology and provide clear definitions. Thanks also to @kmillikin for starting this work a few years ago and giving us something to build upon.

I've included a bunch of comments in my first-pass review. Many of them are minor suggestions for readability. As for the overall content, I think this is directionally on the right path. There are many parts that I really like including the definitions of subtyping, materialization, consistent subtyping, and the "assignable to" relationship.

The one part that I really dislike is the use of the terms "static type" and "dynamic type". I think these are really confusing in the context of Python. They make more sense in a gradual type system implemented with a compiler that emits dynamic checks when a type is not statically known, but that doesn't describe Python. With Python, dynamic type checks are performed at runtime regardless of whether static type annotations are present. All type annotations are "static" in the sense that they are present in the code, and static type checkers can (and do) reason about them. So, I find it very confusing and counterintuitive to call Any a "dynamic type" or to say that list[Any] is not a "static type". I feel strongly that we should explore other ways to talk about these concepts. My concerns can perhaps be addressed by simply choosing better terms than "static type" and "dynamic type". Or better yet, perhaps we can eliminate these concepts entirely from the spec and therefore avoid the need to name them.

One other part that I'm lukewarm on is the proposed definition of Any. I'm not a fan of defining it as "should not be subject to static checking". First, I find this definition to be imprecise. Second, our collective understanding of gradual type systems has progressed since PEP 484, and I think there's a good argument to be made for defining Any differently. Third, Any is not the only gradual typing affordance in the Python type system; I'd prefer to come up with a more general definition that covers all gradual typing affordances (including ... in callables and tuple[Any, ...]).

I think I saw some of these points already made in the comments, but I think we need more discussion before converging on a final draft. This PR is probably not the ideal forum for such discussions. Maybe we should move these open topics to Discourse to improve visibility and solicit input from other members of the typing community.

[carljm]

Thanks once again for all the excellent reviews! I think I've addressed all comments. Some required non-trivial additions (e.g. regarding structural vs nominal subtyping/assignability, and equivalence of gradual types) which previous reviewers may want to take a look at.

I'll wait a few days for review of these changes, and then I'll submit this to the typing council for consideration.

[sliedes]

It's very good. In my view, it's more than ready. I'm adding a couple of thoughts in case someone finds them useful, but IMO this PR is large enough and probably a product of enough work that I don't think these really need to be considered here.

[erictraut]

I've left a couple of comments for very minor issues. I'm fine with ignoring these or deferring them to another PR.

[AlexWaygood]

This is fantastic work. I think it's mergeable now, and I don't want to hold it up. I left some comments below, but they're nearly all very minor copyediting nits that I don't think should block this from being landed if/when it's approved by the Typing Council. Please feel free to simply ignore any you disagree with.

[AlexWaygood]

LGTM

[JelleZijlstra]

Congratulations and thanks @carljm for getting this change through! This puts the spec on a much firmer footing.