-
-
Notifications
You must be signed in to change notification settings - Fork 904
Add typing to sage_input methods #40897
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
Open
tobiasdiez
wants to merge
14
commits into
sagemath:develop
Choose a base branch
from
tobiasdiez:typing_sage_input_
base: develop
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Open
Changes from 2 commits
Commits
Show all changes
14 commits
Select commit
Hold shift + click to select a range
62b5191
Add typing info for _sage_input_
tobiasdiez c76581b
Add future annotations import
tobiasdiez ea7409d
Introduce CoercionMode type
tobiasdiez 71f7484
Add almost complete typing in sage_input
tobiasdiez d147b4f
Add more typing for SageInputBuilder usages
tobiasdiez 98cbe9f
Fix imports in sage/rings/infinity
tobiasdiez f2a6991
Merge remote-tracking branch 'upstream/develop' into typing_sage_input_
tobiasdiez 23aee20
Merge branch 'develop' into typing_sage_input_
tobiasdiez c20e362
Merge remote-tracking branch 'upstream/develop' into typing_sage_input_
tobiasdiez 793855e
Fix missing import
tobiasdiez 524f17e
Allow `Integer` as argument in `SageInputBuilder.__call__`
tobiasdiez 6e3f79d
Merge remote-tracking branch 'origin/develop' into typing_sage_input_
tobiasdiez 377eb91
Merge remote-tracking branch 'upstream/develop' into typing_sage_input_
tobiasdiez b5b4619
Merge remote-tracking branch 'upstream/develop' into typing_sage_input_
tobiasdiez File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Oops, something went wrong.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't understand why you have
Literal[2]here, where is this behaviour for_sage_input_documented?Also,
Literalonly works for Python literals. SoLiteral[2]means theint2, not the SageInteger2.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's defined here:
sage/src/sage/misc/sage_input.py
Lines 56 to 66 in 899d400
I don't think there is a good way to express this as a type.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If
Integer(2)is acceptable input (which I believe it is from some of the examples) then we can't useLiteral[2]here. If onlyInteger(2)is acceptable then useInteger. IfInteger(2)andint(2)are both acceptable then eitherInteger | int, or if you want to useLiteralthenInteger | Literal[2].There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is a good, simple example of the sage vs python integer typing issue we were discussing in the other PR.
My impression is that python is not aiming to become strongly typed but that the purpose of these type annotations is to mainly help developers write better code. Applying this philosophy here, the typing for
coercedshould reveal at least these two 'bugs':1or3(or another integer) as an argument to sage_inputSo in particular, if you have an integer and you would like to pass it as
coerced, you would want to check that it's equal to2before going ahead, eg using:At this point the type checker is able to deduct that
numis the literal 2 (although it's not, it's only equal to it)I feel like supporting (and highlighting the need) for such a pattern is more important than being 100% right about the typing info. One can always add a
pyright: ignorecomment if the typing is to strict/wrong, but one is sure to have covered the case correctly. Of course, you don't want to force to many such comments - it would be stupid to artificially restrict the possible input tointif half of sage's code is passing inIntegerand that works well.Curious what you think about it.
Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This ended up being a longer response than I expected, I've been thinking about type annotations a lot lately.
Just thinking out loud, definitely don't do this in this PR and don't do this without a sage-devel discussion, but is there anything preventing
Integerfrom being a subclass ofint? It would solve a lot of annoyances withInteger. I'm guessing it would be too slow for such an important Sage object.Interesting, I think about it differently. My impression is that type annotations are for linters/type checkers to check that typing rules are respected without having to enforce type checking at runtime. But using
Literalfor parameters I think is beginning to veer into the territory of validating the values of inputs rather than just their types. So to me the utility of type annotations is the ability to have most of the benefits of strongly typed code without the runtime overhead by running a linter/type checker on the code which enforces the rules strictly. The more we adhere to this approach the more useful the type checkers will become (and the more bugs they'll be able to find). Perhaps user code does weirder things that respect the spirit but not the letter of type annotations (for example, a function that acceptsIntegeras a parameter but a user passes aRationalwith denominator1). Users shouldn't have to worry about details like that, and the nice thing about types not being checked at runtime is that something like that will (usually) work fine. I don't think many Sage users are runningmypyorpyrighton their Sage scripts. On the other hand, Sage developers should be expected to write slightly more explicit code that doesn't rely on the coercion system handling incorrect types (if only because relying on the coercion system will introduce overhead that could be avoided by more explicit code).A big reason I favour the stricter annotations approach is that in theory it could be used by Cython to generate more efficient code one day (Cython's ability to use Python annotation is currently a bit limited though, but if we have strict type annotations then as Cython improves here so will the speed of Sage).
Something to consider: when
Literalis used for a parameter, arguments cannot be a variable. So this is invalid:That's kind of awkward, so I don't think I like
Literalfor parameters. It's probably best used only as a return type annotation for functions that return a constant (so things like.is_finitefor objects that are always/never finite).I think that we should use the most specific type annotation that is correct (doesn't require
pyright: ignore). Having to usepyright: ignoredefeats the purpose of type checking the function, the only time I'd use it is if there is a bug in the type checker and we don't want to wait for the type checker to get fixed before merging the PR. If it's legitimately too hard to come up with a correct annotation then we shouldn't annotate it. Or, just annotate it with the most specific correct thing (even if that annotation is more permissive than the function in reality). I don't think an annotation that is slightly too permissive is an issue. We probably have plenty of functions in Sage that accept only a positiveIntegerand check at runtime if theIntegeris non-positive and raise an error if so, but I don't think there is a need to have a more specificPositiveIntegertype.Literaldoesn't supportInteger, so if a function acceptsIntegerthen we can't useLiteralthere. I was discussingLiteralwith @fchapoton in #40972 and he thinks we should probably avoid it for now, and this situation seem like a good example of why we might want to avoidLiteral. Personally I don't thinkLiteralneeds to always be avoided, but the only situation where I think it is likely to be useful is for return annotations, not parameter annotations (in #40972 (comment) I give an example of a hypothetical optimization Cython could make usingLiteral, but the Cython compiler doesn't currently have that optimization so it's a somewhat moot point).(@fchapoton curious what you think about using
Literalonly for return but not parameter annotations.)So for this PR, my suggestion is to change the annotation to
bool | Integer | int, as this is the most specific correct annotation that avoids theLiteralweirdness (evenbool | Integer | Literal[2]is weird as thefooexample above shows). Setting toneeds workfor now.If you want to do a bit more as a separate PR, there is also my suggestion from #40634 (comment) to have a
types.pymodule where we can define common type aliases/unions that are used in Sage (likeInteger | int).Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Good to know, I did use mypy for that example (I happened to have mypy but not pyright already installed).
Still, my suggestion is the same. Let's not use
Literalfor parameters for now (at least not for integers because the wholeintvsIntegerthing makes it too complicated). I don't want to rely on implementation-specific behaviour of one of the two major type checkers. From a quick reading of the differences, it seemspyrightis probably the best choice for our CI at least since it's faster right now, but it looks likemypyalso has some advantages. Andmypymight get improvements in the future that make it preferable (mypyc looks very interesting, but it's in alpha right now).Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It would be indeed nice if the typing info could be used to increase performance. The PEP that introduced typing in Python stated that as a non-goal and said
I looked around and it seems typing info is still not used for performance. There were some initial discussions about using it to warm up the JIT compiler and there are some promising experiments like https://github.com/facebookincubator/cinder?tab=readme-ov-file#static-python. But all of those go into the direction of optimizing the performance without changing the runtime behavior (eg removing complete parts of the code execution path based on typing as in #40972 (comment) is not considered as far as I can see).
Okay, this is actually not that different to what I have in mind. I only would add "better intellisense" to the advantages of typing (eg if you type
vector(...).your IDE is suggesting methods that are defined on the type that is returned by the vector function).I would use
Literalonly where the allowed space of inputs is very restricted, mostly in cases where you should actually use an enum but for historical reasons it's another set of fixed input values. For me,coercedis such a case as it only allowsTrue/False/2.So we essentially have two options:
coerced: bool | Literal[2]:3as input, and makes it clear that the code in the method doesn't need to worry about other integersInt(2)coerced: bool | int | Integer:Int(2)3orInt(3)(both to the callee and to the one implementing the method)I honestly cannot come up with a scenario where one would need to input
Int(2)instead of just a python2. Just because most implementations actually handle theInt(2)case as well, doesn't mean the typing info should necessarily reflect that - in fact you can also pass floats like2.00000000000000000000000000000000000001into the method and it might work - but that doesn't mean it's desired. When it comes to finding bugs, the option using Literal seems to be more robust/helpful.For me
coercedis just an enum, with three values - that happen to be calledTrue, False, 2.Just to emphasize: I don't have a strong opinion about this particular case, and see the discussion more about a means to extract general principles that could guide how we use typing in the future.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, it would change runtime behaviour and hence not happen in CPython. But it could happen in Cython or by something like mypyc, as these only aim to have correct type annotations not impact runtime behaviour. Cython does do some basic analysis to remove dead code, for example
if False: ...is optimized out by Cython.Yeah, it's an interesting case! The only part of this I feel strongly about is that we shouldn't rely on
pyright-specific behaviour. Putting aside issues of CI usage limits, I think it would be reasonable to run bothpyrightandmypyon CI (perhapspyrightas a first pass, and if it passes then we run the slower but potentially more detailedmypy. There are some interesting things that onlymypycan do, notably the currently alpha mypyc looks like it could be very useful for Sage once it matures.Agree.
There is a third option, and this would be my preferred option if we use
Literalhere:coerced: bool | Integer | Literal[2]3as input, acceptsInteger(2). So it accepts all correct inputs, and rejects some incorrect inputs.Integer(3). The type annotation is somewhat confusing, but one can just read the docstring to understand it.I would also add
a = 2; foo(a)not working inmypyto the "bad" list for all of these. This specific function seems unlikely to be called in a way where this is an issue though, so I can let it go as long as we understand thatLiteralshouldn't be used in places where one would reasonably use a variable as the argument (unlessmypybehaviour changes to allow this of course, and I hope it does).The reason to accept
Integeris that the preparser changes2toInteger(2). However looking at it again now, isSageInputBuilder.__call__the only path to_sage_input_through the public API? If so, then my point about the preparser is mostly moot if we just convertIntegertointinSageInputBuilder.__call__(but the annotation for__call__would still need to allow forInteger). It's only mostly moot because some of our doctests call_sage_input_directly with Sage doctests, so we would be testing it withInteger(2)there, but I'm not sure if we use2in any of those tests.Do you know if there is anywhere in the code that we actually use a value of
2forcoereced? I couldn't find any places where we do.Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this might be a reasonable option:
bool | Literal[2]for_sage_input_since it is internal.bool | int | IntegerforSageInputBuilder.__call__since it is public (and thus can be called with the preparser in effect). Validate thatcoercedis eitherboolor2at runtime. Ifcoercedis anIntegerconvert it to anintbefore calling_sage_input_.There is still the matter of if/where
2is currently used and any potential doctests that are testing_sage_input_withInteger(2)directly.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not sure if we really should worry about the preparser. The type checkers will most likely never understand sage code (and even then, they should probably understand that Integer(2) is a valid input for
Literal[2]). But anyway, I've added theIntegerarg to SageInputBuilder.call as you suggested above.The problem with mypy is that it's not adhering to the official typing specs: https://htmlpreview.github.io/?https://github.com/python/typing/blob/main/conformance/results/results.html