PEP 586: Small wording changes from review; expanded example in Abstract

[gvanrossum]

@Michael0x2a please review

The additions to the Abstract example may be controversial, I'm happy
to change these -- or anything else -- if you're uncomfortable with my
suggestions.

[ilevkivskyi]

Potential wording is "Can be rejected" or "May be rejected" to emphasize that type checkers are allowed to reject this (but are not obliged to reject).

[gvanrossum]

But they would be required to reject it if there was intervening code that could possibly assign a different value to four. I don't think we need to split such hairs in this initial example.

[gvanrossum]

Here are some (slightly) more substantial comments on the PEP:

• Literal[(7)] (note the parens around (7)) is accepted by mypy -- should it be? (May be hard to
  detect given ast's behavior, so maybe don't care?)

• The following needs explanation of --follow-imports or something (the "lib_with_no_types -> Any" behavior is unique to Dropbox).

   from lib_with_no_types import SomeEnum  # SomeEnum has type 'Any'!
  

• For "intelligent indexing" I would prefer to use Final over Literal. OTOH what about this example (currently not okay):

    def f(a: Literal[0, 2], t: Tuple[int, str, int])-> int:
        return t[a]  # Should be okay, since t is int at positions 0 and 2?
  

• The Matrix example isn't really usable, is it? How would the runtime
  implementation work? E.g. how would the bounds of a matrix be
  represented at runtime? How would they be derived from the
  constructor arguments?

  (Not that it matters, but for a second I thought that we wouldn't even
  need integer generics to implement Matrix. But I think that's too
  optimistic. :-)

• I guess there's the issue (from Mark Mendoza typing-sig post around March 15-18) about generic functions and literals:

  T = TypeVar('T')
  
  class G(Generic[T]): ...
  
  def f(a: T) -> G[T]:
      ...
  
  a = f(7)
  reveal_type(a)  # G[int] or G[Literal[7]]?
  

• The section on type narrowing leaves me wondering. Why not just
  specify that an if-elif-...-else structure with a literal type should
  do exhaustiveness checking (but formulated more nicely :-). The
  observation that the implementation can be shared with the same
  feature for enums then could get just a brief mention. (Also, how
  much of this is implemented? I assume nothing? Not that it matters
  much from the PEP acceptance POV.)

  Also I'm not sure how much this is related to type narrowing. What is
  the remaining difference between Literal[Status.SUCCESS, Status.INVALID_DATA, Status.FATAL_ERROR] and Status in the example?

• What is 'x' referring to here?

  def parse_status...
      ...
      # Similarly, type checker could narrow 'x' to Literal["PENDING"]
      ...
  

• The is_int_like() example is attractive, but the need to
  exhaustively list all the types that make it return False spoils the
  fun. So this isn't quite the same TypeScript's User-Defined Type
  Guards (from your TypeScript link, [4]).

[gvanrossum]

Although mypy currently doesn't accept this yet.

[ilevkivskyi]

@gvanrossum

For "intelligent indexing" I would prefer to use Final over Literal. OTOH what about this example (currently not okay)

I also prefer Final where possible (but not a strong preference). Also there is a PR in flight that should fix your example.

The Matrix example isn't really usable, is it?

TBH, I didn't like this example since beginning. It is not incorrect, but may be misleading.

The is_int_like() example is attractive, but the need to
exhaustively list all the types that make it return False spoils the
fun. So this isn't quite the same TypeScript's User-Defined Type
Guards (from your TypeScript link, [4]).

I could imagine a similar (maybe even more realistic) function that accepts any object (like isinstance()):

@overload
def is_int_like(x: Union[int, List[int]]) -> Literal[True]: ...
@overload
def is_int_like(x: object) -> bool: ...

There is a subtle point that using such functions for restricting subtype away is not type safe in presence of multiple inheritance (IIUC there is no such problem in TypeScript). But on the other hands many things are already technically unsafe because of multiple inheritance and there were not many complains about this.

I guess there's the issue (from Mark Mendoza typing-sig post around March 15-18) about generic functions and literals:

I don't think this should be specified in any strict way. Type inference can never affect type safety, it can just annoy a user more or less if a type checker (in-)correctly guesses the type arguments. In Python, type inference is probably more important than in other languages because we don't have syntax for type application for functions (i.e. f[int] or f[Literal[7]] in your example), but this is still far from critical. I would rather focus on enabling explicit type applications for functions at some point (which is much more general than the ambiguity for literals).

[Michael0x2a]

I think the first example goes against the "let's not mandate a particular inference strategy" approach we decided on. At least based on talking to Mark, it seemed like the Pyre team wanted to retain the ability to infer that four is of type Literal[4] instead of int in cases like those.

So, I think we should either remove that example or modify the comment to make it clear whether that example is accepted or rejected is implementation-specific.

The second example is sort of similar, but I think the inference strategy we're proposing there is pretty straightforward and non-controversial, so I'm ok with keeping that example.

Everything else looks good to me -- I'm happy merging once we either remove or change the first new example.

[gvanrossum]

Hm, then I think it's better to remove both new examples (esp. since mypy doesn't support either one).

[Michael0x2a]

Literal[(7)] (note the parens around (7)) is accepted by mypy -- should it be? (May be hard to
detect given ast's behavior, so maybe don't care?)

Yeah, I think it's probably fine to not care -- like you said, it's sort of hard to detect. (And also, probably not too many people are going to write code like this, and it's fine even if they do -- the syntax doesn't really imply anything "misleading".)

The following needs explanation of --follow-imports or something (the "lib_with_no_types -> Any" behavior is unique to Dropbox).

Good point; will do.

For "intelligent indexing" I would prefer to use Final over Literal.

I agree, but I also think we probably want to keep the Literal and Final PEPs mostly decoupled from each other.

My current plan is to submit a PR adding a short section about how Literal and Final interact, then add a short note here linking people to that section.

The Matrix example isn't really usable, is it? How would the runtime
implementation work? E.g. how would the bounds of a matrix be
represented at runtime? How would they be derived from the
constructor arguments?

Hmm, it seems like I left out a constructor in that example. I think something roughly like this would work:

class Matrix(Generic[A, B]):
    def __init__(self: rows: A, columns: B) -> None: ...

But yeah, the Matrix example is sort of an attractive nuisance at this point. I'm considering replacing it: the only think stopping me is that I'm having some difficulty thinking of different example using Literals + generics that's at least somewhat realistic.

I guess there's the issue (from Mark Mendoza typing-sig post around March 15-18) about generic functions and literals:

I believe the resolution we came to here is that type checkers should preserve backwards compatibility on a best-effort basis, instead of a mandatory basis. I just need to get around to making a PR for it...

The section on type narrowing leaves me wondering. Why not just
specify that an if-elif-...-else structure with a literal type should
do exhaustiveness checking (but formulated more nicely :-).

We could do that, yeah. I guess just my main worry is that sort of check might end up being inconvenient to some users. For example, mypy currently doesn't do any exhaustiveness checks when we do an if-elif-...-else against Unions in general. I'm guessing there was some reason for that?

Or maybe what we could do is make mypy start reporting errors if any branches containing assert False are inferred to be reachable and/or add that to PEP 484? That would let us get clean opt-in exhaustibility checks that can be used for more than just Literal types: just stick an assert False in the final 'else' block.

There's also the "assert never" pattern discussed here: python/mypy#5818

(Also, how much of this is implemented? I assume nothing? Not that it matters
much from the PEP acceptance POV.)

None of this in master yet. I've been making some some experimental tweaks to the binder over the past few weeks that sort of make this stuff work, but they all feel pretty janky atm.

Also I'm not sure how much this is related to type narrowing.

Hmm, good point. This section should probably be renamed. Maybe something like "Cool stuff you can do with Literals" but more professional?

What is the remaining difference between Literal[Status.SUCCESS, Status.INVALID_DATA, Status.FATAL_ERROR] and Status in the example?

Good point, I'll change that.

What is 'x' referring to here?

Typo -- 'x' should say "status".

The is_int_like() example is attractive, but the need to
exhaustively list all the types that make it return False spoils the
fun. So this isn't quite the same TypeScript's User-Defined Type
Guards (from your TypeScript link, [4]).

I can change this to Ivan's new example above.

[Michael0x2a]

Hm, then I think it's better to remove both new examples (esp. since mypy doesn't support either one).

I think mypy can handle the second example? E.g. it works as expected on this program:

from typing_extensions import Literal, Final

def accepts_only_four(x: Literal[4]) -> None: pass

four: Final = 4
seven: Final = 7

accepts_only_four(four)   # OK
accepts_only_four(seven)  # Error

[gvanrossum]

I think mypy can handle the second example? E.g. it works as expected on this program:

Ah, so it does. Well, I already merged my PR without either example. Anyway, I just added it because I thought it would be a nice contrast to the first example I added, but since that's out, it's probably not essential to have it in the Abstract.

The section on type narrowing leaves me wondering. Why not just
specify that an if-elif-...-else structure with a literal type should
do exhaustiveness checking (but formulated more nicely :-).

We could do that, yeah. I guess just my main worry is that sort of check might end up being inconvenient to some users. For example, mypy currently doesn't do any exhaustiveness checks when we do an if-elif-...-else against Unions in general. I'm guessing there was some reason for that?

Does mypy do any value-based exhaustiveness checks? I guess not. And I didn't realize how subtle all this was. I know the binder does do exhaustiveness checks on types (using isinstance()) and with None. I don't know that it ever warns about exhaustiveness -- but I believe it sometimes silently assumes some block of code is unreachable though (it's been reported as a bug a few times IIRC).

Or maybe what we could do is make mypy start reporting errors if any branches containing assert False are inferred to be reachable and/or add that to PEP 484? That would let us get clean opt-in exhaustibility checks that can be used for more than just Literal types: just stick an assert False in the final 'else' block.

Yeah, I honestly don't believe why exhaustiveness should be so closely tied to Literal types. Is it because the binder mostly looks at types, not values? I guess there's also a concern about subclassing? (The section in exhaustiveness in PEP 484 specifically mentions that enums can't be subclassed.)

I guess I have gotten myself thoroughly confused at this point. :-( Maybe you can attempt to rewrite this section in a separate PR so we can discuss it separately from the other clarifications and improvements you're planning.

For everything I'm not commenting on I am trusting the plans you outlined in your previous comments.