Repository navigation
disambiguate booleans on conditions ("and" & "or" operators) #1698
Description
I've noticed many false positive type errors related to "and" and "or" operators because they have the tendency to create union types. I'm working with some program which I reduced to the following example:
REGEX = re.compile(r'(a*)(b*)(c*)')
def example(s: str, ignore_matches: bool) -> int:
match = not ignore_matches and REGEX.search(s)
if match:
x = match.group(1) or match.group(3)
y = match.start(2)
return len(x) + ymypy figures out that the type of match is Union[bool, re.Match] (re.Match actually doesn't exist, so I can't workaround this with an isinstance() check here but this is not the main point here). So inside the if, I get:
foo.py:9: error: Some element of union has no attribute "group"
foo.py:10: error: Some element of union has no attribute "start"
I understand why this happens, but I'm thinking that this could be analyzed statically, if mypy actually has some "always True" and "always False" types as subtypes of "Boolean". This could help in "and" and "or" expressions. The type of the expression above would be Union[FalseType, re.Match]. Which can be analyzed in an if removing the "FalseType" option from the Union, which gives an accurate typing of re.Match.
A dual situation can be found if you have boolexp or other_exp which could be typed as Union[TrueType, other_type].
A possible generalization of this is having additional type information for all types saying "can be true-ish", "can be false-ish"; and that type information can be narrowed down on boolean operators and ifs.
On first sight, these ideas may look like going beyond the idea of a type checker and more into a program verifier but that's not actually what I'm proposing; the thing is that in actual programs this kind of checks are actually a way to narrow down union types, and my increase the effectiveness of mypy as a typechecker.
Activity
gvanrossum commentedon Jun 11, 2016
Mypy does draw conclusions from Boolean operators and conditional statements, but it has limited understanding. Maybe only a slight refinement is needed? Looking at the code it seems that match could have the following values:
Then the
if match:condition should be made to understand that the first bullets cause the block to be skipped, so inside the block it's always a Match.I'm not sure exactly how to fix this but I think it is in principle possible.
It's possible that there's a complication because the current stubs for re.pyi claim that search() returns a Match -- it should be an Optional[Match]. Once strict optional checking lands that should be fixed; but it would be fine to fix now. I don't think it's the cause of this problem though -- I'm just warning that fixing it (and strict optional checking) may interfere with any fix you could come up with for the issue at hand.
JukkaL commentedon Jun 13, 2016
Having separate, internal types for
TrueandFalse(subtypes ofbool) might be the easiest way to fix the issue. This could come in handy in a few other places as well, at least if these would be promoted to user-level concepts. For example, it might be useful to support overloading based on the value of a boolean argument. I would propose the types to be called justTrueandFalse, similar to how the type ofNoneis calledNone.rwbarton commentedon Jun 13, 2016
@pdmccormick suggested the same thing at PyCon in the context of #1477. I like the idea, but we'd need to find a way to continue to infer the types
boolorList[bool]for variables initialized toFalseor[False](rather than the typesFalseorList[False]), while we'd also need the inferred type ofFalseto beFalsein order to use functions overloaded on the value of a boolean argument.JukkaL commentedon Jun 13, 2016
We also discussed the introduction of types like
ASCIIUnicodeat PyCon. These would be semantically similar toTrue/Falsetypes.ASCIIUnicodewould includeunicodeobjects that only have 7-bit characters. I think that the technical term for this concept is 'refinement type'.I agree that when inferring types of variables, mypy should probably promote all refinement types to the corresponding non-refinement type when there is no explicit type annotation.
ddfisher commentedon Jul 12, 2016
I'm not sure we want these to be subtypes of bool, actually, because many other types are also used for their truthiness. Instead, I think we should track the truthiness of all objects. Tracking truthiness universally should be both simpler to implement and more broadly useful.
dmoisset commentedon Jul 14, 2016
@ddfisher I agree on the "broadly useful" aspect, but I'm not sure about the "simpler" to implement. This should require ad-hoc rules for builtins (for example, [] is falsish, list.append always makes a list true-ish). It would help in
andandorexpressions probably, perhaps the rest of the operations can probably leave truthiness to "unknown"?ddfisher commentedon Jul 14, 2016
Yeah, I agree. I didn't intend to suggest that we should track truthiness in all circumstances. I was thinking more along the lines of your initial example when
ignore_matchesis something other than a bool.dmoisset commentedon Jul 19, 2016
OK, I'm starting to work on this, given that it's not a trivial change. Here's an outline of what I'm doing in case you want to suggest a different approach:
can_be_true(t: Type) -> boolandcan_be_false. For most cases they both returnTrue, butcan_be_true(Void) == Falsecan_be_true(UninhabitedType) == Falsecan_be_true(empty tuple type) == Falsecan_be_false(non empty tuple) == FalseThe only possible type returning False for both functions should be UninhabitedType
TrueOnly(t: Type) -> TypeandFalseOnly(t: Type) -> Type. The idea of this is thatTrueOnly(t)behaves liket, except thatcan_be_false(TrueOnly(t)) == False, and symetrically withFalseOnly. Some other details are that:not can_be_true(t)not can_be_false(t)FalseOnlyp: Tandq: U, thenUninhabitedType,p and q,p or qandnot pare alsoUninhabitedTypenot can_be_true(T)thenp and q: T,p or q: U,not p: TrueOnly(bool)not can_be_false(T)thenp and q: U,p or q: T,not p: FalseOnly(bool)p and q: Union[FalseOnly(T), U],p or q: Union[TrueOnly(T), U]find_isinstance_check(which probably should be renamed at this point). If a condition is a literal of type T, we add TrueOnly(T) to the "if" TypeMap, and FalseOnly(T) to the "else" typemap. The rest of the logic on that function to handle negations and logical operators can stay the same, and if the rules above are follow all the information should propagate.The following is an example:
In the original code of this issue,
matchwill get the typeUnion[FalseOnly(bool), re.Match]according to rule 3. Inside theif match, following rule 4, the context will mapmatchtoTrueOnly(Union[FalseOnly(bool), re.Match]). Because of 2, that's equivalent toUnion[TrueOnly(FalseOnly(bool)), TrueOnly(re.Match)]. The first element of the union is, also using rule 2,Union[UninhabitedType, TrueOnly(re.Match)]. Given that a Union of a type with a subtype absorbs the smaller type, this is equal toUnion[TrueOnly(re.Match)], i.e.TrueOnly(re.Match), So inside theifbranch, it's valid to callmatch.groupddfisher commentedon Jul 19, 2016
I see a few issues with this approach. At a high-level, they are:
isinstanceis used widely inside mypy. How are you planning on dealing with that in theTrueOnlyandFalseOnlywrappers?NoneTypecan never be true, andUnions with mixedTrueOnlys andFalseOnlys shouldn't have theTrueOnlys andFalseOnlys discarded.I'd consider adding an
Optional[bool]toInstanceinstead of the wrapper objects. Aside from what I said above, I think you have the right general idea.dmoisset commentedon Aug 5, 2016
I pushed a PR for this at #1989 It handles this case at least. I'll take a look to related issues to see if they improved with this
Fix for #1698 (#1989)
gvanrossum commentedon Aug 17, 2016
Closing since #1989 fixed this.