
(1)
the union of all possible literal types is equivalent to the wider class upon which those literals are based. For example, the type `bool` is equivalent to the union of `Literal[False]` and `Literal[True]` and vice versa. An enum type is the union of its literal element types and vice versa.
There is a nuance here. That "equivalence" is not true when it comes to checking overloads. [1] For example, just because a `bool` can only be a `True` or a `False` doesn't mean these two overloads are enough to match any given bool [2]: ``` @overload def foo(x: Literal[True]) -> Foo: ... @overload def foo(x: Literal[False]) -> Bar: ... def bar(y: bool) -> None: foo(y) # Type error ``` Likewise, there's an observable difference between `Union[Literal[True], Literal[False]]` and `bool` - compatibility doesn't go both ways. The same concept applies to enums, strings, etc. The type system currently allows us to express: 1. a known literal (`Literal["a"]`) 2. a union of known literals (`Literal["a", "b"]`) 3. arbitrary strings (`str`) There is no way to express a union of arbitrary, unknown literals. Hence this proposal. (2)
A literal expression does evaluate to a literal type, but other (non-literal) expressions can also evaluate to literal types. Type checkers are allowed to compose and decompose these types during type narrowing and type merging.
Joining of types is fine. As mentioned earlier in the thread, `"a" if foo else "b"` is still compatible with `Literal[str]` because we join the two types to get `Literal["a", "b"]`. Narrowing is also fine (such as the enum or bool cases you mentioned). As long as the revealed type is a literal string, it should be acceptable. Even for strings, let's say a typechecker narrows the type based on a literal equality check (`message == "hello, %A"`). That's still acceptable for our purposes because we can't arbitrarily go from a str to a Literal[str] without some explicit narrowing in the code. Likewise for the `clear_or_die` narrowing function that Guido shared. ``` def my_format_string(s: Literal[str], x: object) -> str: ... def foo(message: str, a: object) -> None: if message == "hello, %A": print(my_format_string(message, a)) # OK if the revealed type is a literal type print(my_format_string(message, a)) # Not OK ``` (3)
In the case of `int` and `str`, the number of enumerable literal types is very large, but "the union of all int literals" is still equivalent to `int` and vice versa. So I don't see the need to add the notion of `AnyLiteral[int]`. From a type perspective, that's the same as `int`.
Lastly, if you still feel it is unnecessary, it would help to share how you would handle the motivating examples without `Literal[str]`. Specifically: ``` def my_format_string(s: Literal[str], x: object) -> str: ... def print_request(user_request: Dict[str, str]) -> None: # OK because the type of the format string is a literal string print(my_format_string("hello, %A", user_request["name"])) # Not OK because the type is an arbitrary str print(my_format_string(user_request["message_format"], user_request["message"])) ``` [1]: https://www.python.org/dev/peps/pep-0586/#interactions-with-overloads [2]: Mypy snippet for overloads: https://mypy-play.net/?mypy=latest&python=3.8&gist=92f7c56aae6678c7a3fc13aaa19be309 On Fri, Aug 6, 2021 at 9:47 AM Eric Traut <eric@traut.com> wrote:
I find this proposal confusing. It appears to be based on a misunderstanding that the only way to generate a literal type is through the use of a literal expression. Literal types and literal expressions are not the same thing. A literal expression does evaluate to a literal type, but other (non-literal) expressions can also evaluate to literal types.
In type calculus, the union of all possible literal types is equivalent to the wider class upon which those literals are based. For example, the type `bool` is equivalent to the union of `Literal[False]` and `Literal[True]` and vice versa. An enum type is the union of its literal element types and vice versa.
Type checkers are allowed to compose and decompose these types during type narrowing and type merging. For example:
```python class Color(Enum): red = 0 green = 1 blue = 2
def func(x: Color): if x is not Color.red and x is not Color.blue: reveal_type(x) # Literal[Color.green] ```
Or consider this: ```python v1: Literal[False] = False reveal_type(v1) # Literal[False] v2: Literal[True] = True reveal_type(v2) # Literal[True]
v3 = v1 or v2 reveal_type(v3) # Literal[True] v4 = v1 and v2 reveal_type(v4) # Literal[False]
v5 = v1 if random() > 0.5 else v2 reveal_type(v5) # bool ```
In the case of `int` and `str`, the number of enumerable literal types is very large, but "the union of all int literals" is still equivalent to `int` and vice versa. So I don't see the need to add the notion of `AnyLiteral[int]`. From a type perspective, that's the same as `int`.
-Eric
--- Eric Traut Contributor to pyright & pylance Microsoft Corp. _______________________________________________ Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://mail.python.org/mailman3/lists/typing-sig.python.org/ Member address: gohanpra@gmail.com
-- S Pradeep Kumar