Uuuh why ? That’s the whole point of type intersections. Being able to label it through parameterization is just a nice plus, but philosophically, saying T & S as a type is a parameterization of T with parameter S in some way. You might be against type intersection, but it’s a feature that has been asked for for long now.
Types are not a hierarchy and should not be one as it would disable multiple inheritance.
With the current definitions of TypedDicts, the intersection of a TypedDict with any required field and any parameterization of dict is empty.
Intersections can’t solve a problem that comes from the definition of TypedDicts violating substitution when it comes to their actual runtime type. The type system is basically dependent on LSP.
The best outcome I can see here is that people stop using Typed Dicts all together, and parse into well-defined types with some library like msgspec, cattrs, or pydantic.
Barring that, because people won’t avoid broken type system features, type checkers just need to understand properly the runtime semantics of isinstance for any types with special behavior like this, and not treat isinstance as narrowing via intersection in all cases.
what if you have a kind of house rule that you treat dicts as frozendicts? If I’m understanding the problems with TypedDict correctly, nothing should possibly go wrong at runtime in a function that type-checks correctly as
def f(d: dict | frozendict | TypedDict): ...
and you don’t do any
with different code paths for dicts and frozendicts.
Whilst I do sometimes mutate dicts, I consider mutating a dict that is passed into a function an enormous code smell.
With the current definitions of TypedDicts, the intersection of a TypedDict with any required field and any parameterization of dict is empty.
Well, the doc currently states :
However, a TypedDict with extra items may be a subtype of
dict[str, VT], provided certain conditions are met, because it introduces sufficient restrictions for this subtyping relation to be safe.
so it sounds like the intersection is not always empty. Moreover, the specific case in the doc sounds correct as well.
The type system is basically dependent on LSP.
Agreed. However, this does not mean that things are broken. In particular, define
class ConstantTD[T](TypedDict, extra_items = T):
pass
I don’t see a useful place where substituting a ConstantTD[ValType] by a dict[str, ValType] is a problem, showing that indeed, dict[str, ValType] might be a more specialized version of ConstantTD[ValType] (indeed, it’s the same set of values, just with extra methods), and as ConstantTD is itself a subtype of TypedDict by nominal subtyping, this is fine.
On methods specific to TypedDicts in the case of ConstantTD:
__total__should be True as a property over the emptyset__required_keys__is the emptyset__optional_keys__is the emptyset__readonly_keys__is the emptyset__mutable_keys__is the emptyset
All this can generalize very well to regular dict, no mandatory keys so they’re always total, and all the other methods returning the emptyset is sound as well. This being said, those are dunder names and probably shouldn’t be accessed in usual code anyway.
The best outcome I can see here is that people stop using Typed Dicts all together, and parse into well-defined types with some library like msgspec, cattrs, or pydantic.
Tbh, if they are so much better, write a PEP to replace TypedDict with arguments and all. I think if they’re not part of standard lib there might be a reason. From what I understand, Python stand is to have low runtime overhead in terms of structures, and TypedDict are meant for static typing mostly. If you want absolute typesafe structures, maybe python is not the right language (remember that type hinting is completely optional and should have no impact at runtime), I’d tell you to look into Rust as it is to my knowledge one of the most type safe languages so far (I mean, there’s OCaml and Rocq with even more theoretical safety, but whatever).
Barring that, because people won’t avoid broken type system features, type checkers just need to understand properly the runtime semantics of isinstance for any types with special behavior like this, and not treat isinstance as narrowing via intersection in all cases.
Before talking about “broken type system features”, maybe a formalization of this type system should be done ? To my knowledge, so far, there’s nothing that grouped all the specs written in the PEPs and proved that it was a consistent type system. As far as I know, Python type system might even be flawed by design. Feel free to use proof assistants if you feel like it. You might be able to show that the runtime semantic is not consistent with the specified semantic.
On another note, isinstance cannot modelize completely the theoretical type system, and this can be shown. Indeed, if it was the case, isinstance would solve the halting problem (just preface a copy of your class with a turing machine of your choice), which isn’t possible. So another solution might simply to disallow TypedDict in isinstance. It’s brutal but simple, and might be way more productive than requiring runtime checked structures from msgspec, cattrs or pydantic.
You’ll note I used the words “with any required field”. Your supposed counter example doesn’t have one of those.
I suggested such when the type specification was being worked on, and was told by pretty much every typing council member that this wasn’t a path being considered, and I specifically recall explicit derision to anything that was that “academic”, so excuse me if I’m not going to take a statement like this as a real reason to put forward that level of effort, especially when the root cause here is that typed dicts violate substitution.
At runtime, typedidcts are dicts.
There is no runtime type for typed dicts, so isinstance(some_typed_dict, dict) is always true. typecheckers that treat this as an intersection, but rely on the type specification stating that in general typed_dicts aren’t subtypes of dicts is what creates the problem in the OP.
The feature is broken, and it isn’t fixable while both keeping that users can use a dict expression to write their TypedDict, but also want to enforce that certain keys must always exist. Changing TypedDicts to allow .clear, or to use return type of Never for certain methods makes the type safety worse while remaining incorrect. (these methods don’t always raise at runtime, the latter creates situations where a typechecker that optimizes out type checking “unreachable” code, is wrong about what is unreachable). It doesn’t require a full formal proof, we can show that the contradiction exists between runtime and specification.
At best, we can create rules that minimize the issue, and ideally those rules only affect users of typed dicts without negative effects for other users.
You’ll note I used the words “with any required field”. Your supposed counter example doesn’t have one of those.
Yeah okay, my bad, I read too fast. Here, the mistake’s on me. I agree with your claim, and the spec as well. Doesn’t change my point that maybe having TypedDict as a supertype of dict[str, object] might be a solution.
and I specifically recall explicit derision to anything that was that “academic”
Oh well… I wasn’t aware. What a shame. In a world where more and more programs require to be verified, refusing theoretical guarantees is probably a mistake. But whatever, sorry, didn’t know, and you see me very disappointed in the typing council. I can’t see the point of having a tool for formal proofs if not to produce formal proofs. This honestly hits very hard on my motivation for my upcoming PEP proposition about higher kinded typevars…
At runtime, typedidcts are dicts.
Might be the problem here. Rewriting them as dicts with less methods might still be a fix. Obviously, this TypedDict type would be accessible at runtime, but most of the code would come from the same C library underhand, so not too much work involved.
while both keeping that users can use a dict expression to write their TypedDict
I mean… Do you disagree with protocol subtyping ? Because protocol subtyping is exactly this, more specified protocols can be seen as less specified protocols by “forgetting” the fact they add additionnal methods. You could go the same way to cast some dicts to TypedDict (and I still believe in this case that TypedDict should still be a supertype of dict[str, object])
Changing TypedDicts to allow
.clear, or to use return type ofNeverfor certain methods makes the type safety worse while remaining incorrect.
Please, not Never again
I already have too many theoretical problems with Never.
Jokes aside, I agree with what was said earlier that if a subtype have methods that raise most of the time, it’s probably not the right way to do things, which is why I proposed to see it the other way, with TypedDict being a supertype of some dicts.
Protocol subtyping is mostly fine. There are some problems that exist currently around lossy variance and intentional type ignores in collections.abc, and those issues actually run somewhat parallel here, but the issue here isn’t structural subtyping, it’s other things like load-bearing type ignores that impact the standard library. When you start typechecking from incorrect information, you’ll find inconsistencies as a result.
TypedDicts with any required key promise that that key is always present, and provide a type for the associated value.
This promise is incompatible with the existence of methods that remove it, so treating this as just structural subtyping doesn’t work, because there’s a built-in promise that can’t be modeled under the current type system that no other added interface can violate that constraint. Then, even if it could be modeled, dict methods that always exist violate that constraint.
I may not like this and find that TypedDicts were a mistake to have the way we do, but I still think the pragmatic approach, given how many people like typed dicts[1], is to make them type check reasonably while minimizing the potential for negative impact. To me, that’s specifying isinstance, along with other runtime narrowing based on runtime type, slightly differently to better handle this and other existing ways in which isinstance isn’t an intersection, and to account for places like this where the runtime type isn’t fully consistent with the type at typechecking time.
Along with the fact that of all the reasons to break the existing typesystem users, this one ranks pretty low on my list. I would expect any large break like this to only happen if we were actually going to fix bigger issues at the same time, which seems unlikely to me. ↩︎
When you start typechecking from incorrect information, you’ll find inconsistencies as a result.
Agreed.
This promise is incompatible with the existence of methods that remove it, so treating this as just structural subtyping doesn’t work, because there’s a built-in promise that can’t be modeled under the current type system that no other added interface can violate that constraint. Then, even if it could be modeled, dict methods that always exist violate that constraint.
Not sure to understand here. I mean, I understand how it is currently a problem, but in the case where TypedDict is a supertype of dict[str, object], it means that
my_TD : SomeTD = some_dict_value
my_TD.clear() # type checker should raise an error as it shouldn't be possible
is code that runs at runtime but is not admissible for type checkers. This is parallel to
my_object : ProtocolWithout_a : some_protocol_with_a
my_object.a() # type checker raise an error because it does not necessarily have `a`
which is runtime okay but not type okay. I don’t see why it is a problem here to have it that way.
Furthermore, checking that some_dict_value can be safely interpreted as a SomeTD is the work of type checkers. If they cannot, they might flag it (it’s okay to not be able to type check everything). But to me it is very doable to like :
- record initial value of
some_dict_value - record if a deletion/reassignation happens
- record additionnal insertions
And this is probably sufficient to check the promise in 95% of usecases.
To me, that’s specifying
isinstance, along with other runtime narrowing based on runtime type, slightly differently to better handle this and other existing ways in which isinstance isn’t an intersection, and to account for places like this where the runtime type isn’t fully consistent with the type at typechecking time.
I mean, currently, isinstance shouldn’t narrow anything as TypedDicts are a subtype of dicts by the only claim that " A TypedDict type represents dict objects that contain only keys of type str." (directly from the doc). This is, by set-based type theory, a direct inclusion of TypedDict in dict. This is furthermore in agreement with the glossary in the doc :
A fully static type
Bis a subtype of a fully static typeAif and only if the set of possible runtime values represented byBis a subset of the set of possible runtime values represented byA.
dict is fully static, and TypedDict is fully static as well, as none of them contains gradual forms (once again, purely applying defs from the glossary). Hence, because TypedDict is a subtype of dict, the narrowing cannot go “upwards”, and after the isinstance, maybe calls to “forbidden methods” should be perceived as calls that returns Never but… pls send help if that’s the way it is to be done.
This being said, there’s two way of moving forward :
TypedDict <: dictis true, and then it is mandatory to implement methods like.clearetc for TypedDictsTypedDictis not a subtype ofdict, and something in the doc has to change. Anything further is up to discussion.
If you ask me, I think set-based type theory is actually a really wrong base for Python type system, and TypedDict shouldn’t be a subtype of dicts either.