Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[red-knot] Add internal documentation on kinds of types #13878

Open
wants to merge 12 commits into
base: main
Choose a base branch
from

Conversation

AlexWaygood
Copy link
Member

Summary

This PR adds purely internal documentation to assist us, as red-knot developers. By having a common reference with precise definitions for certain terms, there's a reduced risk of misunderstanding.

Test Plan

pre-commit run -a

@AlexWaygood AlexWaygood added documentation Improvements or additions to documentation internal An internal refactor or improvement red-knot Multi-file analysis & type inference labels Oct 22, 2024
@AlexWaygood
Copy link
Member Author

AlexWaygood commented Oct 22, 2024

I wondered whether these docs would be better placed somewhere like https://typing.readthedocs.io/en/latest/. But I'm not sure it would be a great fit for that site, because:

  • Some of the concepts for our internal model of Python's types are not standardised as part of the spec. For example, our concepts of "class-literal" and "function-literal" singleton types are not something that all Python type checkers have
  • It's not clear that these terms are relevant to either the typing spec or the user-facing documentation parts of https://typing.readthedocs.io/en/latest/

Copy link
Contributor

@carljm carljm left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for writing this up! The core ideas look great, I think there are a few issues in some wordings.

crates/red_knot_python_semantic/docs/kind_of_types.md Outdated Show resolved Hide resolved
crates/red_knot_python_semantic/docs/kind_of_types.md Outdated Show resolved Hide resolved
crates/red_knot_python_semantic/docs/kind_of_types.md Outdated Show resolved Hide resolved
crates/red_knot_python_semantic/docs/kind_of_types.md Outdated Show resolved Hide resolved
crates/red_knot_python_semantic/docs/kind_of_types.md Outdated Show resolved Hide resolved
crates/red_knot_python_semantic/docs/kind_of_types.md Outdated Show resolved Hide resolved
crates/red_knot_python_semantic/docs/kind_of_types.md Outdated Show resolved Hide resolved
crates/red_knot_python_semantic/docs/kind_of_types.md Outdated Show resolved Hide resolved
@AlexWaygood
Copy link
Member Author

I updated the PR: I abandoned the attempt to describe a generalised concept of "closed types"; instead, I now just attempt to describe final nominal types (classes explicitly decorated wtih @final, and enum classes).

@MichaReiser
Copy link
Member

I'm looking forward to read this but don't wait on my review :)

Copy link
Contributor

@carljm carljm left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks good! Most of my comments are minor nits.

crates/red_knot_python_semantic/docs/kind_of_types.md Outdated Show resolved Hide resolved
crates/red_knot_python_semantic/docs/kind_of_types.md Outdated Show resolved Hide resolved
crates/red_knot_python_semantic/docs/kind_of_types.md Outdated Show resolved Hide resolved
crates/red_knot_python_semantic/docs/kind_of_types.md Outdated Show resolved Hide resolved
crates/red_knot_python_semantic/docs/kind_of_types.md Outdated Show resolved Hide resolved
crates/red_knot_python_semantic/docs/kind_of_types.md Outdated Show resolved Hide resolved
crates/red_knot_python_semantic/docs/kind_of_types.md Outdated Show resolved Hide resolved
@AlexWaygood
Copy link
Member Author

I've once again reworked the final section of this substantially, because I realised my last draft still had some inaccuracies. For example, I wrote that:

a final type in Python still has subtypes, just no nominal subtypes.

which is pretty obviously wrong when you think about enums: Literal[E.A] is a nominal type (well, it's certainly not a structural type, anyway), and it's obviously a subtype of the enum E.

My conclusion from all this conversation is that while the concept of final classes might be useful, the concept of final types actually isn't that useful at all (and the name is somewhat misleading in some ways). So I scrapped the section defining a concept of "final types" and replaced it with a section describing "final classes".

I'd appreciate it if you could give the last section another once-over @carljm!

Copy link
Contributor

@carljm carljm left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The first several sections of this are really excellent, I have only the most minor of wording nits.

The last section is improved, but I still feel it suffers from a significant "so what?" factor, in that it spends IMO too many words discussing things that I don't think are particularly relevant to red-knot behavior. But this isn't a blocking concern.

crates/red_knot_python_semantic/docs/kind_of_types.md Outdated Show resolved Hide resolved
... # x can be narrowed to `None`
```

All Python singleton types are also sealed types and final types; nearly all are single-value types.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There's still a reference to "final type" here, which may no longer make sense given later changes.

crates/red_knot_python_semantic/docs/kind_of_types.md Outdated Show resolved Hide resolved
crates/red_knot_python_semantic/docs/kind_of_types.md Outdated Show resolved Hide resolved
crates/red_knot_python_semantic/docs/kind_of_types.md Outdated Show resolved Hide resolved
```py
from enum import Enum, auto

class Animals(Enum):
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

minor nit, not related to the core point: I think using plurals is generally not great naming practice for either enums or classes generally, suggest Animal instead

crates/red_knot_python_semantic/docs/kind_of_types.md Outdated Show resolved Hide resolved
For any two classes `X` and `Y`, if `X` is `@final` and `X` is not a subclass of `Y`,
the intersection of the types `X & Y` is equivalent to `Never`, the empty set.
This therefore means that for a type defined as being "all instances of the final class `X`",
there are fewer ways of subtyping such a type than for most types in Python.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I still feel like this section buries the lede in a major way.

From red-knot's perspective, by far the most important thing about final class types is that we know exactly what methods and attributes they define, with what signatures (including especially dunder methods), and we know there can't be infinite possible subclasses overriding those methods and attributes. But we don't even mention that here, beyond a very vague reference in this phrase to "fewer ways of subtypign"; instead we go on to discuss (at relative length, with an example) the edge case of how some final class types can still have proper subtypes, although it remains unclear in the text why the existence or non-existence of proper subtypes should matter to red-knot or the reader.

Comment on lines +245 to +252

Many singleton and sealed types are associated with final classes: the classes
`types.EllipsisType`, `types.NotImplementedType`, `types.NoneType`, `bool`,
and all enum classes are final classes. However, there are also many singleton
and sealed types (some representable, but some merely theoretical)
that cannot be defined as "all instances of a specific final class `X`".
In the above enum, `Literal[Animals.LION]` is a singleton type and a sealed type,
but would not fit this definition.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would probably eliminate this entire paragraph. It's confusing, and really not clear what important point it makes.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
documentation Improvements or additions to documentation internal An internal refactor or improvement red-knot Multi-file analysis & type inference
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants