Literal types

[Michael0x2a]

Opening a pull request to help make inline commenting easier.

[ilevkivskyi]

Thanks for working on this! I left a bunch of comments. Mostly just typos/style/formatting. I would propose to move from brainstorming doc to more PEP-like (more strict) document, and move all things we are not doing to the "Rejected/postponed ideas" section.

[ilevkivskyi]

This example is problematic because:

class MyInt(int):
    ...

x: Matrix[int, MyInt]  # ?
y: Matrix[MyInt, int]  # ?
y @ x  # Matrix[MyInt, MyInt] ???

TBH, it is in general misleading. I would on the contrary warn against any premature use of literal types in numeric libraries and advise to wait until a dedicated PEP is out.

[Michael0x2a]

I don't think your example is that misleading or weird -- it seems like the kind of thing that could legitimately be useful in the wild. For example, if I were writing some machine learning code and wanted to keep track of the dimensionality of things, it wouldn't be too far of a stretch to try combining NewType with int, Literal int types, and some custom stubs to better keep track of the dimensionality of things, distinguish between dynamic vs static quantities, and so forth.

You could then parameterize Matrix with NewTypes like "BatchSize" or "NumFeatures", with literal int types, or a mixture of both, depending which parts of your model you want to leave dynamic or not -- I think you can add a lot of basic but useful types by creatively combining what we have now + literal types, even without full-fledged integer generics.

But in any case, I cut out some of the discussion and added a more explicit warning, as requested. I do think it's important to have some sort of moderately complex example of using generics with literal types to clarify what the expected behavior is though. I'm not really picky about what example we use though -- maybe the best thing to do is to just switch to an example that uses string literals or something, and side-step the whole integer generics business?

I'll try and come up with an example and swap out the existing one sometime later this week.

[ilevkivskyi]

With the current wording I am actually OK with this.

[ilevkivskyi]

We need to say something about possibility of warnings in case of non-exhaustive checks. This was requested by some users.

[Michael0x2a]

I mentioned this in the email from earlier, but I think talking about warnings in the case of non-exhaustive checks really has more to do with the semantics of Unions more then Literal types.

I did add a note reminding people of the section in PEP 484 that discussions enums and implied that some type checkers could perform reachability/exhaustiveness checks in the same kind of way we imply that in the section about NoReturn in PEP 484.

I think nailing to what degree type checkers should perform non-exhaustive checks vs requiring users to use tricks like assert_never(...), to what degree type checkers should detect and warn about dead code, etc should probably be an entirely separate discussion.

[ilevkivskyi]

Maybe some people from Pyre, pytype also want to be here?

[Michael0x2a]

Sure, I guess -- I have no idea how authorship works on PEPs, to be honest.

[rchen152]

Left a few comments, but I mostly wanted to say that this is a really neat proposal, and I'm looking forward to getting rid of some of pytype's custom overlays :)

[rchen152]

It seems to me like the simplest thing would be for Literal[Any] to be equivalent to Any, which would get rid of the "Literals, enums, and Any" problem below.

[Michael0x2a]

You might be right -- I went back and forth on this a few times, but ended up leaning towards disallowing this because I was uncomfortable with the idea of anybody trying to explicitly construct a Literal[Any]. I was also worried somebody might try and interpret this type as meaning "any literal" instead of "any type" or something like that.

But you're right, being able handle the literal + enums + bad import problem more smoothly would be pretty nice.

[rchen152]

I could see something like this being useful:

Mode = TypeVar('Mode', Literal['r'], Literal['w'])
class File(Generic[Mode]):
  def __init__(self, mode: Mode) -> None: ...
  def get_mode(self) -> Mode: ...

[Michael0x2a]

Ah, right -- I was referring mostly to things like TypeVar('S', bound=Literal["foo"]). I definitely agree there are use cases for literals + typevars w/ value restrictions.

[ilevkivskyi]

Are there any remaining discussion points here? If not, I think this is ready for the second posting on the typing list (and maybe even for a broader discussion).

[Michael0x2a]

@ilevkivskyi -- I might need to tweak or at least think more carefully about some of the enums-related stuff. Right now, it's sort of underspecified, and I haven't yet thought carefully enough about whether or not what we have right now is enough (e.g. how do we want to handle things like IntFlag, and are details like those even worth mentioning?).

I think I also need to update the section about Final slightly. The current description doesn't quite align with the approach you proposed here: python/mypy#6081.

And finally, I vaguely remember getting one more piece of feedback close to the start of the holidays, but I don't remember exactly where. I'll need to track that down and address that as well.

[ilevkivskyi]

and are details like those even worth mentioning?

I would say it is not worth going so deep in details IMO.

[vsiles]

(Sorry if that's not the right place to discuss this, but I didn't find another discussion thread on the subject) Why refusing simple evaluation like Literal(1 + 1). It could help type interesting functions (like PyTorch's torch.diag function) and seems harmless (It's simple beta-reduction, really). I understand that we don't want full evaluation in there but constant only expressions could easily be reduced.

[JukkaL]

@vsiles Can you show a concrete example signature where constant expressions would be helpful? Implementing them wouldn't be hard, but it may not be obvious exactly which operations should be supported.

[vsiles]

For example to type torch.diag: https://pytorch.org/docs/stable/torch.html?highlight=diag#torch.diag

x : Tensor[M, N] = ....
y = torch.diag(x) # should have type Tensor[min(M, N)]
z : Tensor[M, M] = ....
t = torch.diag(z, 1) # should have type Tensor[M - 1]

I think we might need these simple expressions (note that they must reduce to int or generate a type error) to be able to type diag.

[JukkaL]

@vsiles You example would require something that we call "integer generics". It will be a separate PEP that extends this proposal. It may happen some time later in 2019.

[vsiles]

Ok ! I'll go and check that one too :) Thanks !

[vsiles]

@JukkaL dully noted. Just to be sure I got it right. Using only literal types, if I mostly deal with let's say [ 3, 3 ] matrices and I want the +1 diagonal, I could use @overload to write:

@overload
def diag(m : Tensor[Literal(3), Literal(3)], n:Literal(1)) -> Tensor[Literal(2), Literal(2)]

@overload
def diag(m:Tensor[Any], n:int) -> Tensor[Any] 

Did I get that right ?

[ilevkivskyi]

@vsiles Yes, huge overloads are possible workaround for now. But IIUC how diag() works, you have a typo, it should be

@overload
def diag(m: Tensor[Literal[3], Literal[3]], n: Literal[0]) -> Tensor[Literal[3]]: ...
@overload
def diag(m: Tensor[Literal[3], Literal[3]], n: Literal[1]) -> Tensor[Literal[2]]: ...
# etc. you've got the pattern

the problem however is that mypy doesn't allow defining variadic generics (another thing in near term plans), so you should probably have separate Tensor2D and Tensor1D, or even better just wait.

This PEP was not intended for multi-dimensional array support.

@Michael0x2a ^ this is what I warned you about.

[vsiles]

I see, thank you. I'm not in a hurry anyway, just trying to understand your solution to this very complex problem (I'm already familiar to it with other languages, more proof targeted).

[mrkmndz]

Just a heads up that I'm working on pyre's implementation of Literals and may have some thoughts/questions coming up :)

[gvanrossum]

Why is this PR still open? Is it different from what's committed in the branch?

Re: authorship, it's totally up to you, you could invite 1-2 contributors who added a significant idea and/or who were helpful in formulating the text. It's not like scientific papers!

I would recommend renaming this to PEP 586 (the next free number) and submitting it as a PR to the official peps repo ASAP.

[mrkmndz]

What I was trying to say at the meetup is that this kind of inference guidance is too prescriptive in my opinion. As far as I know, inference has so far been unspecified in the typing PEPs, and I think it's better that way, as mypy and Pyre seem to have different behavior.

The key example I'd like to be supported, but not required behavior is

x = 5
x = 6
takes_six(x)

This currently goes against lines like

When assigning a literal expression to an unannotated variable, the inferred type of the variable is the original base type, not Literal[...].

Pyre allows variables without explicit annotations to have different types at different points in a function, and we'd like to maintain this flexibility for literals.

Ultimately, I think Note 2 is more of the spirit of what should be in the PEP, and most of this Inferring types for literal expressions section can and should be removed

[Michael0x2a]

@mrkmndz -- I'm thinking of replacing these sections with something roughly like this:

When type checkers are implementing Literal, it's important they do so in a way that preserves backwards compatibility. Code that currently type-checks should continue to type-check after adding support for Literal.

For example, take a statement like x = 6. It would be incorrect for type-checkers to automatically assume x is of type Literal[6] since that would break code that looks like this:

def expects_int(x: int) -> None: ...
x = 6
expects_int(6)  # Previously type-checked, and so should continue to type-check

In cases like these, type checkers should either perform type inference to determine the correct type of x, or if they are unable to do so, conservatively bias towards assuming that x is of type int instead of a Literal type.

[Add more examples and edge cases of what type checkers shouldn't do here]

...and like you suggested, remove any text that requires a specific inference strategy.

Does this seem good to you? If so, I can make this change later today + ping you once that's ready.

[mrkmndz]

What inference would lead to that example not type checking? If I understand correctly, even with an explicit annotation of Literal[6], that example should still type check as literal integers are subtypes of int?

[Michael0x2a]

Oh whoops, you're right -- that's a terrible example. (Sorry, was rushing
to get the comment out before lunch).

Something like:

x = 6
x = 100

...would be a better example: we can't infer x is of type Literal[6] there.

[Michael0x2a]

Or, you could, so long as you support changing the type of x -- that would also preserve backwards compatibility, which is really we we (the mypy team) ultimately care about.

[mrkmndz]

Couldn't inferring this to be a Literal["foo"] be fine, as that's a subclass of str? I understand there are problems with containers due to variance, but that problem also exists for non-literals, and has also been unspecified so far.

[mrkmndz]

Yeah, something like "reassignment should be always valid i.e. x = 6 followed by x = 100 to preserve backwards compatibility" feels optimal.
Putting all of this in a backwards compatibility heading seems like the right spirit as well.

[mrkmndz]

I think that inferring pure literals to literals should always be backwards compatible because of subtyping (presuming re-typing is allowed), but inferring [1] to be List[Literal[1] could break compatibility. Maybe the PEP should say don't infer literals in more complex literals like lists, dictionaries and lambdas?

[rchen152]

Instead of prescribing specific rules, what if the PEP says, "Type checkers should infer ``Literal[...]`` only in contexts where a Literal type is explicitly requested *or where doing so would not break backwards compatibility*", gives some examples of bad inference that would break backwards compatibility, and leaves it at that? Then each type checker is free to do what makes the most sense in the context of its implementation/philosophy.

…

On Wed, Mar 13, 2019 at 12:31 PM Mark Mendoza ***@***.***> wrote: I think that inferring pure literals to literals should always be backwards compatible because of subtyping (presuming re-typing is allowed), but inferring [1] to be List[Literal[1] could break compatibility. Maybe the PEP should say don't infer literals in more complex literals like lists, dictionaries and lambdas? — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#1 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AD806AIhWyMB408xccCkK7BXbPP7vDizks5vWVIjgaJpZM4Yrqxg> .

[Michael0x2a]

@rchen152 -- yep, I think I'm planning on doing pretty much exactly what you proposed!

Emphasize the importance of backwards-compatibility, give some examples of where naive inference would break things, and stop there.

[Michael0x2a]

@mrkmndz and @rchen152 -- I edited the section on type inference as we discussed; let me know if there are any additional changes you think we should make!

I also adjusted the "Interactions with type narrowing" section that appears later in the doc -- it previously used to state that type checkers need to do narrowing with things like equality or containment checks, but I decided those kinds of things are probably better off being optional. Setting aside the whole "let's not be prescriptive with how inference is done" thing, we haven't implemented that behavior in mypy yet/haven't confirmed it's actually a useful thing to have.

The blurb on enums and exhaustion checks is still required though, mostly because PEP 484 apparently requires it.

We also added an example of how type checkers might optionally use Literal bools to allow for the construction of "custom type guards". (The idea is mostly borrowed from TypeScript's user type guards, actually). Mypy hasn't implemented that either, but it seems like a nice thing to eventually have.

[mrkmndz]

Thanks for your changes, just a few more concerns/questions

[mrkmndz]

I think this paragraph is kind of confusing, and ultimately doesn't matter because it says that these are only some of many possible strategies. I think the section would be more readable if it were just removed.

[Michael0x2a]

I'm not sure I feel comfortable with removing this paragraph entirely -- although the exact strategy for performing inference is now left unspecified, I do think it'll be helpful for readers if they see some examples of what type checkers are likely to do here in practice.

In particular, I want to make sure readers don't leave with the impression that type checkers are necessarily obligated to do something complicated here, and I think mentioning the "it's fine to do nothing new" strategy would help set user expectations.

I do agree this paragraph is worded poorly though. I went ahead and rewrote it -- does the new version seem better to you?

[mrkmndz]

I think this is potentially problematic re: backwards compatibility.
If we allow having typevariables bound to literals, then we run the risk of having variance issues crop up. Avoiding these requires a degree of lookahead that seems like a big burden to push onto type checkers.
I think it might be prudent to ban them being propagated through normal typevariables, and instead wait for the IntVar proposal or something like that to specifically take them.
Short of that, perhaps we could only allow them in type variables like the ones in your example, upper bounded by the corresponding type?

[Michael0x2a]

Sorry, I'm not quite sure what you mean -- could you perhaps provide an example of a variance or lookahead situation you're worried about?

If I had to guess, I'd imagine you're perhaps worrying about how to handle examples like this one?

T = TypeVar('T')
class MyContainer(Generic[T]): pass
x = 5

# Is y of type MyContainer[int] or MyContainer[Literal[5]]?
# We might need to see how y is used to know for certain?
y = MyContainer(x)

I think it would be reasonable if Pyre decided against doing anything complicated here, in the same way that mypy doesn't try doing anything complicated w.r.t. inferring the type of unannotated variables. For example, it would be fine if you defaulted to having MyContainer(...) be of type MyContainer[int] in this case -- or maybe if you decided to only try the lookahead thing you described if the TypeVar had an upper bound.

I think Mypy would basically do something similar anyways, though that's really more a consequence of how we chose to handle variable assignments.

Anyways, while writing this section, the only thing I meant to require is that it should be possible to parameterize generics with Literal types -- e.g. write type hints that look like MyContainer[Literal[5]], or explicitly set the type by doing something like:

y = MyContainer[Literal[5]](5)

And once you do/once the typevars are bound, the type system should behave exactly as one might expect.

But I don't think it makes sense to prescribe any particular strategy or restriction on how Literals are propagated through TypeVars or how to infer what gets bound to a TypeVar in this PEP, in the same way we decided it didn't make sense to prescribe a particular strategy on how to handle type inference with variable assignment and the like.

(Let me know if I totally misunderstood your concern!)

---

FWIW, the motivation behind allowing Literals and generics to interact in this way is that we wanted to make Literal types behave as closely as possible to existing types -- the underlying story this PEP is painting is that Literal[1] is "just" a subtype of int. The concern is that users would find it confusing if we disallowed Literals from binding to TypeVars: it would feel like a weird special case.

I think this concern would hold even if we added IntVars. Then, I'd imagine users would start to wonder why they can't parameterize generics with Literal strings or Literal enum values.

Also, not sure if this helps, but when we were implementing this in mypy, we found we were able to directly apply the bulk of our generics and type inference related code to handle Literals with minimal special-casing. We treat Literals just like any other subtype, and only add in one special case to handle which "default type" gets picked when we encounter an expression with no real constraints on what type it could be.

Of course, I'm not at all familiar with how Pyre is implemented, so maybe it's not possible for you to adopt this strategy.

[mrkmndz]

This seems much better, but I think still doesn't need this e.g. (as I think it begs more questions about what that context means than it clarifies).
Not super hung up on it though.

[Michael0x2a]

Sure -- I removed the e.g. I'm trying to find ways to make this doc shorter anyways.

[rchen152]

The section on type inference looks good to me now! By the way, I like the section on custom type guards - it's a neat use of literals that wouldn't have occurred to me if not pointed out.

[rchen152]

Just a wording nit: the previous section uses "infer" in a technical sense, so I think it's confusing to use it in a colloquial sense here. Maybe "should not be automatically cast to Literal" or "should not be considered subtypes of Literal"?

[Michael0x2a]

Thanks! I made the fix you suggested here: python#929

[gvanrossum]

Now that this has been merged into the peps repo, further discussion should probably go to typing-sig, and this issue should be closed (just to avoid crossed messages).

[Michael0x2a]

@mrkmndz -- I left a comment responding to your TypeVar question up above; not sure if you've seen it yet.

We can maybe finish up the discussion there or continue it on typing-sig. I'm fine with either; up to you.

But I think all of the other feedback given in this thread has been incorporated, so I'm going to close it now as suggested. Thanks all!