Hello!
Following on some discussion at the Typing Summit, I’ve proposed a significant addition to the Python typing specification in https://github.com/python/typing/pull/1743
The aim is to offer a clear theory of the Python type system, and clear definitions for core terms that can be used consistently throughout the specification. In a sense, this PR could be considered an attempt to update PEP 483 and bring it into the typing spec as a living document, rather than frozen in 2014. The text draws from PEP 483, from @kmillikin 's Python Static Types I: Subtyping document, and from some recent academic work in the field of gradual typing. Any errors are solely mine.
The PR as it stands today is already much improved from my initial effort, thanks to thoughtful review from @erictraut, @kmillikin, @Jelle, @AlexWaygood, @mikeshardmind, Zeina Migeed, @stroxler, @grievejia, @superbobry, and other reviewers.
I look forward to your comments as well!