Literal type math

I am working on feature where reveal_type(1 + 2) will reveal Literal[3].

Types that I want to support:

int
str
bool

And these operations:

_SUPPORTED_LITERAL_OPERATIONS: Final = {
    int: ('+', '-', '*', '//'),  # `/` returns `float`
    str: ('+',),
    bool: ('and', 'or'),
}

So, True or False is revealed as Literal[True].

I will finish some test later today and send a PR in the morning.

I presume this is intended to work generally for any expression that involves these types, not only expressions that are used as arguments to reveal_type calls? In other words, do you expect this to work?

a: int
a = 1 + 2
reveal_type(a) # Literal[3]

You might want to consider adding 'not' to the list of supported operators for bool and '%' and the unary form of '+' and '-' to the list of operations for 'int'.

For int operations, you'll need to decide what to do about numeric overflows and divide-by-zero conditions. Probably OK to fall back on int.

Out of curiosity, are you planning to support unions?

def func1(a: Literal[1, 2], b: Literal[0, 4], c: Literal[3, 4]):
    reveal_type(a * b + c)  # Literal[3, 4, 7, 8, 11, 12]?

def func2():
    greeting = "Hi " + ("Steve" if random() > 0.5 else "Amy")
    reveal_type(greeting) # Literal["Hi Steve", "Hi Amy"]?

One challenge to consider... If you're evaluating types in a loop, you need to be careful about literal math.

def func1(loop_count: int):
    x = 1
    reveal_type(x) # Literal[1]
    x = x + 1
    reveal_type(x) # Literal[2]

    for _ in range(loop_count):
        x = x + 1
        reveal_type(x) # int

I think this is a good feature idea, so I implemented it in pyright. If you haven't already completed your PR for mypy, perhaps I can save you some time by sharing the unit tests I wrote.

Could * potentially be a supported operation for strings? 'foo' * 2 seems pretty similar to 'foo' + 'foo'.

Out of curiosity, are you planning to support unions?

def func1(a: Literal[1, 2], b: Literal[0, 4], c: Literal[3, 4]):
    reveal_type(a * b + c)  # Literal[3, 4, 7, 8, 11, 12]?

def func2():
    greeting = "Hi " + ("Steve" if random() > 0.5 else "Amy")
    reveal_type(greeting) # Literal["Hi Steve", "Hi Amy"]?

You of course need to trust the code you run your LSP on, but what is the handling for bad input?

Intentionally trying to OOM:

from typing import Literal

fifty_primes = Literal[2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97, 101, 103, 107, 109, 113, 127, 131, 137, 139, 149, 151, 157, 163, 167, 173, 179, 181, 191, 193, 197, 199, 211, 223, 227, 229]

def func(
    a: fifty_primes,
    b: fifty_primes,
    c: fifty_primes,
    d: fifty_primes,
    e: fifty_primes,
    f: fifty_primes,
    g: fifty_primes,
    h: fifty_primes,
    i: fifty_primes,
    j: fifty_primes,
    k: fifty_primes,
    l: fifty_primes,
):
    reveal_type(a * b * c * d * e * f * g * h * i * j * k * l)

I'm not sure how possible it is to accidentally create such a situation though.

@erictraut

You might want to consider adding 'not' to the list of supported operators for bool and '%' and the unary form of '+' and '-' to the list of operations for 'int'.

Thanks! I haven't touched unary operations right now. But, they are on the list!

For int operations, you'll need to decide what to do about numeric overflows and divide-by-zero conditions. Probably OK to fall back on int.

Yes, this is a plan. In case of any problems / errors we escape from Literal special path to ordinary check_op

I think this is a good feature idea, so I implemented it in pyright. If you haven't already completed your PR for mypy, perhaps I can save you some time by sharing the unit tests I wrote.

Thank you, @erictraut!

One challenge to consider... If you're evaluating types in a loop, you need to be careful about literal math.

Yes, looks like a good unit-test.

Out of curiosity, are you planning to support unions?

They are not supported right now. Probably in the future 🙂

Could * potentially be a supported operation for strings? 'foo' * 2 seems pretty similar to 'foo' + 'foo'.

Yes, I also tought about that. But, right now the logic is that type never changes for both operands. str * int produces str which is the corner case. I will try it!

TODO:

UnaryOp
OperatorAssignmentStmt?
More operators for int: like ^, |, **, etc
'a' * 2
Union literals
Better 1 // 0 error message, we can totally catch that case and warn our users
a: Final = 'a'; reveal_type(f'{a}b') should reveal Literal['ab']?, probably this can be a separate feature

Strings explode a bit more easily in similar fashion if they're added a few times.

Intended to OOM:

from typing import Literal
mode = Literal["a","b","c","d","e","f","g","h","i","j","k","l","m","n","o","p","q","r","s","t","u","v","w","z","y","z"]

def func(
    a: mode, b: mode, c: mode, d: mode, e: mode, f: mode, g: mode, h: mode, i: mode
):
    reveal_type(a + b + c + d + e + f + g + h + i)

EDIT: This is far too much unneeded work, but I was thinking you can probably handle these cases without bailing to int or str if you avoid eager evaluation and instead put the corresponding problem into a SMT solver when you need to type check against a literal. 😄

@GBeauregard

@GBeauregard we don't support union type at the moment, but this is going to be a great corner-case in the future! 🎉

@GBeauregard

@GBeauregard, that test case is evil! I love it. :)

Navigation Menu

Repository navigation

Literal type math #11990

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Literal type math #11990

Description

Activity

erictraut commented on Jan 13, 2022

erictraut commented on Jan 14, 2022

erictraut commented on Jan 14, 2022

erictraut commented on Jan 14, 2022

AlexWaygood commented on Jan 14, 2022

GBeauregard commented on Jan 14, 2022

sobolevn commented on Jan 14, 2022

sobolevn commented on Jan 14, 2022

GBeauregard commented on Jan 14, 2022

sobolevn commented on Jan 14, 2022

erictraut commented on Jan 14, 2022

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions