Make static type checking work better with symbolics #1156
Merged
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This change adds
TypeIsto the signature ofis_symbolic, thereby making spurious static type checker errors less likely and enabling us to remove uses ofcastandassert.Motivation
A common pattern in the codebase is as follows:
Unfortunately, this pattern doesn't play well with static type checkers such as mypy, which we use.
As an example we actually encountered, consider this snippet from #1089 (just prior to commit 23577b2):
Given the above code, mypy fails with the error:
This overly conservative type checking error occurs because in general, a static type checker cannot infer that the type of the argument of
is_symbolicshould be narrowed tointfromUnion[int, Expr]whenis_symbolicreturns False. Such inference is normally reserved for specific language patterns, such asisinstance:We do sometimes use
isinstancein the codebase for this purpose, but it is less general and we would prefer not to replaceis_symbolicwith it.Solution
Fortunately, we can do better and get the benefit of type narrowing using the recently introduced
TypeIstype annotation. In brief, by annotating the return type ofis_symbolicasTypeIs[sympy.Expr]rather thanbool, the static type checker will infer that whenis_symbolic(arg: Union[int, Expr])returns True, thenarg: Expr, and otherwisearg: int.This PR makes the above change. Consequently, it safely removes numerous instances of
cast(int, ...),assert [not] isinstance(...),int(...), and similar patterns from the code.There are some caveats due to limitations of the Python type system:
is_symbolic. To get the benefit, it is necessary to rewriteis_symbolic(x, y)asis_symbolic(x) or is_symbolic(y).is_symbolic(self)method defined on a class rather thansymbolics.types.is_symbolic.HasLengthandShaped. However, in one scenario, it was necessary to explicitly annotatek: SymbolicFloatso that the type checker would inferk: Exprrather thank: Union[HasLength, Shaped, Expr]whenis_symbolic(k)returns True.Tuple[SymbolicInt, ...]toTuple[int, ...].