-
Notifications
You must be signed in to change notification settings - Fork 1.1k
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] more precise types from chained boolean expressions #13632
Comments
If I understand correctly
I have some questions:
|
Those are great questions! Any type "makes sense" independently as long as we can describe it as some set of possible runtime values. So these types can stand alone, in principle: In practice, I expect that we would only create these types in intersections, wherever we are able to determine that a type must be truthy or falsy. If we introduce this type, we accept (at least for now) the fact that it may leak to users, since we won't be able to simplify it in all cases. We will often have this tradeoff, where we can more fully represent our type knowledge, at the cost of displaying more complex types to users. In general, I would prefer to represent the most precise type knowledge we can be confident of, and then find ways to simplify the user type display if that proves to be necessary. For instance, we could later implement logic in the display code for intersections to just hide these types in the output, if we end up feeling that it becomes too noisy otherwise. My hope, though, is that users will find these types reasonably intuitive, and will appreciate more precise typing. One thing to note here is that currently (since we've so far only implemented support for one form of narrowing, |
So, I started working on this. I have the following question: when expressing Let's take the following example: def f(x: int):
if x:
... # here, `x` is `Truthy` or `x` is not `Falsy` |
Related to @Slyces's question here... do we need a |
As pointed out by @Slyces in #13571 (comment)
Copying my comments from there:
I think the logic here is that when we have an actual
bool
type in a chained boolean expression, in non-last-position, rather than addingbool
to the union we can instead addLiteral[False]
(for AND) orLiteral[True]
(for OR).There's a more generalized version of this where we add
Falsy
andTruthy
types, and then we'd always intersect any type in that position (not justbool
) withFalsy
orTruthy
, and then for bools that would simplify out in the intersection (e.g.bool & Falsy
isLiteral[False]
). I think it's likely we end up doing this for type narrowing anyway, but I don't have strong feelings about whether we go straight for the generalized solution or start with a bool-specific implementation.The text was updated successfully, but these errors were encountered: