Speaking from the heart: I worry that this argument will never end, and spur ever longer, more esoteric posts.

I haven't seen a good use case for allowing dict literals with extra fields. The use case brought up in the meeting was something like

class Point:
    x: int
    y: int

def validator(p: Point):
    if isinstance(p.get("x"), int) and isinstance(p.get("y"), int):
        return
    raise TypeError("not a point")

def test():
    validator({"x": 0, "y": 42, "z": -1})  # Rejected by type checkers

but IMO this is a poorly designed API, it should be more like

def validator(p: dict) -> Point:
    if isinstance(p.get("x"), int) and isinstance(p.get("y"), int):
        return cast(Point, p)
    raise TypeError("not a point")

--Guido

On Fri, Apr 8, 2022 at 9:13 AM Steven Troxler <steven.troxler@gmail.com> wrote:
> It is common to think of types as descriptions of sets of values

This is definitely a common philosophy, and probably the most helpful when looking at the runtime use of types.

There's another common view of types as representing "evidence" that all values have some property, and static type checking works more like this - we walk the code using typing rules and build little proofs that the types are valid.

But we'd still expect transitivity in the evidence-oriented philosophy. The current behavior is a bit like having a logic where implications aren't transitive. For example, if:
   A := the value d is the evaluation of `{"x": 0, "y": 0}`
   B := the value d is compatible with type `Child`
   C := the value d is compatible with type `Parent`
Then the current typing rules specify that having evidence of `(A => B)` and `(B => C)` does not constitute evidence of `(A => C)`.



There's another school of thought that says typing rules are just arbitrary functions telling us whether a specific expression is compatible with a specific type.

In this view, soundness and completeness are the only lenses we're allowed to use to evaluate typing rules, and we're always willing to give up completeness. Since transitivity is related to completeness (I think it's essentially the simplest possible completeness property), we are free to break it if we think there's some usefulness in doing so and therefore the best approach comes down to use cases.

My view is that breaking transitivity is not good for the external data use case because it can confuse even expert users (as in this thread, where several users incorrectly concluded that TypedDict cannot be used for data where extra fields might be present).

But there's also the TypedDict-as-cheap-classes use case, where more rigid validation of literals could be pretty helpful. I'm not sure how to weigh this use case, especially since newer code probably leans toward dataclasses instead.



One thing we discussed was changing the error message to make the literal behavior clearer.

One possible phrasing of this: "Extra fields are not permitted in literal assigments to TypedDicts, although at runtime they may be present in TypedDict values."
_______________________________________________
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: guido@python.org


--
--Guido van Rossum (python.org/~guido)