[ty] Implement Python's floor division semantics for Literal ints (#18249)

Division works differently in Python than in Rust. If the result is
negative and there is a remainder, the division rounds down (instead of
towards zero). The remainder needs to be adjusted to compensate so that
`(lhs // rhs) * rhs + (lhs % rhs) == lhs`.

Fixes astral-sh/ty#481.
This commit is contained in:
Brandt Bucher 2025-05-22 10:42:29 -04:00 committed by GitHub
parent 98da200d45
commit 91b7a570c2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 50 additions and 10 deletions

View file

@ -72,6 +72,34 @@ reveal_type(2 ** (-1)) # revealed: float
reveal_type((-1) ** (-1)) # revealed: float
```
## Division and Modulus
Division works differently in Python than in Rust. If the result is negative and there is a
remainder, the division rounds down (instead of towards zero). The remainder needs to be adjusted to
compensate so that `(lhs // rhs) * rhs + (lhs % rhs) == lhs`:
```py
reveal_type(256 % 129) # revealed: Literal[127]
reveal_type(-256 % 129) # revealed: Literal[2]
reveal_type(256 % -129) # revealed: Literal[-2]
reveal_type(-256 % -129) # revealed: Literal[-127]
reveal_type(129 % 16) # revealed: Literal[1]
reveal_type(-129 % 16) # revealed: Literal[15]
reveal_type(129 % -16) # revealed: Literal[-15]
reveal_type(-129 % -16) # revealed: Literal[-1]
reveal_type(10 // 8) # revealed: Literal[1]
reveal_type(-10 // 8) # revealed: Literal[-2]
reveal_type(10 // -8) # revealed: Literal[-2]
reveal_type(-10 // -8) # revealed: Literal[1]
reveal_type(10 // 6) # revealed: Literal[1]
reveal_type(-10 // 6) # revealed: Literal[-2]
reveal_type(10 // -6) # revealed: Literal[-2]
reveal_type(-10 // -6) # revealed: Literal[1]
```
## Division by Zero
This error is really outside the current Python type system, because e.g. `int.__truediv__` and