-
-
Notifications
You must be signed in to change notification settings - Fork 674
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
2
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 all commits
Commits
Show all changes
2 commits
Select commit
Hold shift + click to select a range
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,
Literal
only works for Python literals. SoLiteral[2]
means theint
2, not the SageInteger
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.
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 useLiteral
thenInteger | 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
coerced
should reveal at least these two 'bugs':1
or3
(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 to2
before going ahead, eg using:At this point the type checker is able to deduct that
num
is 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: ignore
comment 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 toint
if half of sage's code is passing inInteger
and 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
Integer
from 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
Literal
for 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 acceptsInteger
as a parameter but a user passes aRational
with 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 runningmypy
orpyright
on 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
Literal
is 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
Literal
for parameters. It's probably best used only as a return type annotation for functions that return a constant (so things like.is_finite
for 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: ignore
defeats 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 positiveInteger
and check at runtime if theInteger
is non-positive and raise an error if so, but I don't think there is a need to have a more specificPositiveInteger
type.Literal
doesn't supportInteger
, so if a function acceptsInteger
then we can't useLiteral
there. I was discussingLiteral
with @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 thinkLiteral
needs 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
Literal
only 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 theLiteral
weirdness (evenbool | Integer | Literal[2]
is weird as thefoo
example above shows). Setting toneeds work
for 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.py
module where we can define common type aliases/unions that are used in Sage (likeInteger | int
).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.
Thanks a lot! I don't have too much time at the moment to properly respond, but please have a look at this playground where I played around with your example:
https://pyright-play.net/?code=GYJw9gtgBALgngBwJYDsDmUkQWEMoAySMApiAIYA2AsAFB0AmJwUwYYAFOQFyHFlUA2gFYAugEooAWgB8mFDG50oKqCBIwAriBRRyUANRQAjHToAjKAF4owum07nJUAMTyAblSQMANFEtIAM5QKGD4%2BpT8FDT0tCia0DamtA4c8RDiZrSopGi8OdZQAORFrlCBkBoAFqgYqJ6RvlBhVWQA7kEksK3yudY2wpjBKCTuZFCjVJrkpAx6wQhwIEhoVfjqAMZgaChIAF4kwTBVM5j4G%2BQoofgnCAgkKHTqY1QA%2BvD3HDkkaJJuOfZ2F8FD9MrEkCxvhgrAMlLRVGpRiQ3h8SMDcn8%2BKRoiJRMpVKkoWCgA
The
foo(b)
call is not marked as invalid in this example, as pyright is able to properly recognize thatb
isLiteral[5]
. Some other code likeis properly marked as invalid.
(Note that the behavior under mypy might be different - in my experience pyright is usually the better option.)