PEP 742: TypeNarrower

[JelleZijlstra]

---

📚 Documentation preview 📚: https://pep-previews--3649.org.readthedocs.build/pep-0742/

[carljm]

Looks good, thank you for pushing this forward!

[carljm]

FWIW, I really like the name TypeIs. I think it reads naturally in the code, communicates the two-way nature of the check (true means it is, false means it is not), and is concise.

In comparison, I find "TypeNarrower" to be unnecessarily long and somewhat grammatically clumsy.

I'm also not sure how well the term "narrow" (as it relates to types) communicates to the typical static typing user.

I also think there is benefit to having the name TypeIs be shorter and simpler than TypeGuard -- it implies (correctly) that the former is more commonly useful and less niche.

[JelleZijlstra]

Yes, I think it's a good candidate. I will mention this as a leading alternative when I post the PEP, and see if people like it.

We could go even shorter with simply Is: def some_func(o: obj) -> Is[int]:. But that might be a bit too short, and becomes hard to Google.

[gvanrossum]

I also think there is benefit to having the name TypeIs be shorter and simpler than TypeGuard -- it implies (correctly) that the former is more commonly useful and less niche.

Agreed -- I find this an important criterion for choosing the name, and TypeNarrower fails. I find TypeIs slightly awkward (like all classes whose name is a verb) and would prefer TypeCheck.

[JelleZijlstra]

I don't like TypeCheck because it feels like that term is already in use by the term "type checker", and we say that a program "typechecks". But I could live with it if that's the consensus.

[erictraut]

I find TypeNarrower really cumbersome too.

Other ideas to consider: Narrowed (which is not unlike Annotated) or NarrowedTo.

[JelleZijlstra]

Added those to the list.

[carljm]

I think it would be valuable for the PEP to include a rationale for this. I think it was really unfortunate that PEP 647 included this restriction without providing any rationale. There may be good reasons for this restriction (I would guess maybe it has to do with losing the benefits -- and maybe even back-compat implications? -- of having bool no longer be a final type?), but they are not obvious and so they should be clearly recorded. It seems useful to be able to pass a type-narrower function as a predicate callback (whose signature would be Callable[..., bool], so the burden of proof should be on the rationale for not allowing it.

[JelleZijlstra]

I'm not sure what the rationale was here; maybe @erictraut remembers why this restriction was put in. In any case, if we change this, we'd likely want to change it for both TypeGuard and this PEP's new construct, and we could probably do that with a smaller (non-PEP) modification of the spec.

[erictraut]

IIRC, this statement wasn't in my early drafts of PEP 647 and was added near the end at the suggestion of @gvanrossum, who sponsored the PEP. I agree that the restriction should either be removed or a better rationale or formulation should be provided.

[JelleZijlstra]

python/mypy#11307 might be part of the reason, though that issue postdates the acceptance of the PEP.

[JelleZijlstra]

FYI I opened https://discuss.python.org/t/compatibility-between-typeguard-and-bool/46364 about this point.

[carljm]

Suggested change

	not subtypes of ``R``.
	not consistent subtypes of ``R``.

[JelleZijlstra]

I did write "subtypes" here on purpose. My understanding is that Any is a consistent subtype of any concrete type T, but not a subtype. If we start with a type A | Any and have a narrower that narrows to A, then in the else case the type should be narrowed to Any, not Never.

[JelleZijlstra]

I think the right wording is that NP includes those union elements that are subtypes of R, and NN includes those that are not subtypes of R. I will change the text to say that.

[JelleZijlstra]

Thinking about it more, this is still wrong in the presence of generics. Consider the case where A is list[Any] | set[str] and R is Iterable[str]. Then I think NP would ideally be list[str] | set[str] and NN would be list[Any], but this specification would dictate that NP is just set[str].

I think this specification only holds for literal types. I'll reword it to say it's an example and limited to literal types. It would be a mistake to attempt a general specification for intersection types here.

[carljm]

I'm actually not sure what you mean by "literal types" here? My initial reading of that term is that it includes only types using the Literal special form. If that is what you mean, it seems like an oddly specific example that might cause more confusion than it clears up ("what's so special about Literal?"). If that's not what you mean, then I think we need a clearer term.

I don't think certain kinds of types are special; from the examples given so far, I think the correct specification is asymmetrical: NP are those elements of the union that are consistent subtypes of R, and NN are those elements of the union that are not subtypes of R. In other words, Any can always be ruled in and never ruled out. (If I'm not mistaken, this is the wording you originally had, so I'm sorry that I confused it with a not-thought-through comment!)

Another approach (since we are not trying to provide a full spec here) might be to eliminate this paragraph and provide just a list of concrete examples.

[JelleZijlstra]

I did mean Literal only. Those types have the advantage that they cannot be subclassed or be generic, which makes life simpler.

I don't think your spec behaves the way I'd want a type checker to behave. For example, if A is Any | str and R is str, I would want NP to be str, not Any | str.

Still, you're right that the example becomes oddly specific if it's just about literals. I'll think about another rewording.

[erictraut]

I don't think your spec behaves the way I'd want a type checker to behave.

The spec, as it's currently written, doesn't dictate the exact behavior. It provides the type-theoretically-correct formulation, and it recommends that type checkers employ similar logic that they do for isinstance type narrowing. I think that's the best we can do here.

Rich Chiodo and I did an in-depth analysis and presentation at a typing meetup on this topic. If you didn't attend that meeting or would like to refresh your memory, check out the presentation here.

We should probably choose an example in the spec that is straightforward, non-controversial, and likely to generate the same results for all type checkers (based on their current isinstance narrowing behaviors).

[carljm]

I don't think any spec framed solely in terms of inclusion/exclusion of items in a union can handle the generic examples, where we'd ideally want to refine the type parameters of an element of the original union.

I think the formal spec in terms of intersections (and the parallel to isinstance) is perhaps the only spec that needs to be provided here. A fuller specification of how type checkers approximate intersections might be useful, but seems out of scope for this PEP. Replacing this paragraph with a list of concrete "desirable examples" seems like it provides a practical illustration of the previous paragraph, without trying to be a full intersection spec. I think that will be clearer than trying to provide a more general "example" in prose.

[JelleZijlstra]

Thanks Eric, the presentation was very helpful. Perhaps it should be linked from the PEP?

I dropped the paragraph this discussion is about. The previous paragraph already gives a spec in terms of intersection semantics (mirroring the spec in PEP 724) and the next section contains examples.