The negation of Any, a typechecker’s internal Unknown or Todo type isn’t Never, but some gradual type that may materialize as the negation of the materialization of that type.
This is the only sound interpretation with the current materialization I’ve seen, but it presents a problem for TypeIs functions should any typechecker actually implement this this way.
For instance, the seemingly trivial function below cannot be correctly expressed
The negated branch runs into a problem here, as TypeIs[list] is implicitly TypeIs[list[Any]
Under the current materialization rules ~list[Any] does not preclude all possible lists.
Proposal
typing.Unspecialized as a singleton value that when used as a generic parameter indicates that something refers to all possible specializations, rather than implicitly the default.
Naming, Consistency, and the rabbit hole
It may be better to name this typing.All and allow it to exist as a standalone type. I’m not personally invested in being able to directly specify a universal quantification type[1] in cases beyond generics, but that is essentially what this would be, as was noted below.
at least, not without being able to specify a predicate ↩︎
Point of clarity: typing.Unspecialized would not be valid as a standalone type, type-expression, type-variable bound or default, and should not be implicit. It is only valid in places where the difference between “All possible A” and “Some possible A with unknown or unspecified specialization” matters.
A[typing.Any] represents some specific materialization that isn’t specified and is gradual, A[typing.Unspecialized] would represent all possible materializations, and is a fully static type.
A list[T1] is assignable to list[Any] for all possible types T1. So doesn’t that imply that there exists no T2 for which list[T2] is assignable to ~list[Any]? Or is there something more to the negation type that I’m missing here?
list[Any] represents an unknown set of lists. It may materialize to any particular static type. Therefore, ~list[Any] represents all objects except some unknown set of lists. list[str] & ~list[Any] may materialize for example to list[str] & ~list[int], which is just list[str], or to list[str] & ~list[str], which is Never.
Ah I see. So if you consider list[Any] as a superposition of all its possible materializations, then you consider the ~list[Any] as the superposition of all the negation of each of them. So the assumption is that ~ is distributive w.r.t. materialization. Did I get that right?
@jorenham
I wouldn’t quite envision it that way, but I can see at least some of why that seems convenient as a comparison. The only thing I think is “not quite right though” about it is that it’s not so much that ~ is somehow distributive, but that because the bounds on a particular Any’s possible materializations are unknown, so would the bounds of “all the things not consistent with it”
I think a possibly more useful physical visualization would be more like if generics are each their own plane, and then specialization of the generics are venn-diagram-like regions on that plane (and some of these generics might be entirely disjoint, especially in the case of Invariant Generics), then we still want a way to represent “this is consistent with all things on the plane”
Would you consider ~AnyOf[A, B] to be the same as AnyOf[~A, ~B], @mikeshardmind:? (In terms of the set of possible materializations, I mean, not in the “consistent with” sense)
I’m not sure what AnyOf is meant to be here, but I would say no?
for instance something that is known to be ~list[Any] includes everything that isn’t a list, and some things that are a list depending on what the possible materialization of Any is in this context, whereas something known to be list[~Any] only includes lists, and the kinds of lists that are excluded are based on the materialization.
I don’t like the name. typing.All would be more apt, but I guess you probably were trying to avoid the direct comparison with typing.Any from the user perspective because you don’t want this used without a generic. I presume this is because you don’t want to specify Any and this thing as predicate free existential and universal quantification types.
Is this something that is useful as a manual type annotation? Or would it primarily occur as an intermediate step for type checkers?
If the former, I assume it’s a pretty advanced feature that 99% of users would never need to use?
Maybe it could be hidden somehow to not cause confusion and not require understanding the complex interactions being explained here until you encounter the need naturally.
It is the “gradual union type”, see e.g. AnyOf - Union for return types · Issue #566 · python/typing · GitHub. Basically, AnyOf[A, B] is the same as Any if the universe of possible types would be limited to just A or B, where A | B would be the “top type” (analogous to object).
I would consider ~AnyOf[A, B] to be the same as Neither[A, B], i.e. Any - (A | B), where - means something like “but not”, or “take away”. It’s similar to how not (a or b) is equivalent to not a and not b, and how ~(A | B) is equivalent to ~A & ~B.
In the same way, I’d define ~Any as Any - Any, so Never.
And I’m not saying this because “it feels right” or something. I’m saying this because it’s a consequence of de Morgan’s laws (wiki), which apply to both set theory and type theory. In the gradual typing literature I’ve seen, the negation type is also defined like this e.g. https://dl.acm.org/doi/10.1145/3290329.
If we were to add a negation type in python, then users will almost certainly expect that if you can assign something to T, you can not assign it to ~T. But that would be incompatible with how you’ve been describing ~list[Any]. I would expect ~list[Any] to be Any - list[Any], so it could materialize to anything that isn’t a list.
I believe that this definition would also void the need for the Unspecialized type that you’re proposing here.
@MegaIng Yes, it’s useful as a manual type annotation, but it would be an advanced use. While I wouldn’t want it hidden away, I would want it to not be prominently presented until we were comfortable enough explaining advanced concepts in user documentation as to correctly simplify it. (I do think there is a simple, intuitive explanation)
Yeah, and for anyone else who gets that, that’s close to the difference between this and Any. “There exists some type…” vs “For all types…”, The main thing here is that I really don’t want to frame this in the context of universal and existential quantification
It does not, and the original issue linked comes from a case where there is negation happening.
This definition doesnt work either, and there’s a reason most literature actually refuses to define negation for ?
I’m probably missing some fundamental type theory here, but wouldn’t object serve this purpose? That is, doesn’t list[object] describe all possible lists without any inference? If that’s true, then ~list[object] should describe all types that are not lists.
This almost works for “fully static types” but does not work for Any and other gradual types, because each instance of Any can have a different materialization. You wrote this as if the first Any in your subtraction means “all types”, but this is not the definition of Any
if Any is “Some unknown type”
then ~Any is “Some unknown type”
The “unknown” part of that can’t be erased. in terms of consistency, ~object can be replaced with Never for covariant use of ~object, but the same does not apply to ~Any
You also should not imply Any - T for ~T as this changes it to a gradual type.
I can see that you are trying to avoid it but personally I would find this discussion easier to follow if the language used quantifiers explicitly. It may be that there is just not some other good way of explaining these things.
There’s a way to express a version of this today that works with mypy and pyright:
def f[T](x: list[T]) -> None:
x.append(42) # error
reveal_type(x[1]) # T, assignable only to object
This matches the definition of existential types. However, the scope of the TypeVar is too broad, so this trick won’t always allow expressing the type you propose.
I ran into a similar issue recently on typeshed, where we wanted to express that a function could take any instance of a generic type, regardless of the generic parameter. My idea was to add a qualifier Covariant[T] that can be used with a generic and indicate that its type parameters behave covariantly. Then Covariant[list[A]] would be equivalent to forall T assignable to A. list[T], a static type inhabited by list[int] and by list[T] for all subclasses T of int, and Covariant[list[object]] would be equivalent to list[Unspecified] as proposed here.
Example behaviors:
def f(x: Covariant[list[int]]) -> None:
x.append(1) # error, not valid for all inhabitants of the type
reveal_type(x[0]) # int
f([1]) # OK
f([True]) # OK
f(["x"]) # error
This would allow expressing the input type of functions like json.dumps, which takes a list containing only elements of particular types, without constraining callers to an exact invariant type. (Roughly: type JSON = Covariant[list[JSON]] | Covariant[dict[str, JSON]] | int | float | bool | str | None.
This is a really bad naming that will make people misunderstand what is happening here. list[T], forall T assignable to A does not make T behave covariantly, it describes being consistent with all of the infinite set of all possible types of list[T] where T is assignable to A. It would also be incredibly hard to assign a value that is consistent with all of those at once, which is probably why it has only come up from narrowing semantics.
For the json.dumps specific case, it would be better to allow user specification of the lower bound of a gradual type. This can be done with intersections: list[T & Any] As T & Any describes some unknown type that must be assignable to T, it covers the need.
typing.Unspecified specifically was intended to mean what we know for all specializations of a Generic, or put in the phrasing that the name is from: what we know without having a specialization.
The json dumps case can be better typed with either call-site variance or the gradual intersection, but your proposed typeform is not directly equivalent to the use of a universal quantifier in the manner described.
method declaration-site variance[1] for all types[2] would likely be an improvement, but it would be a massive change to the existing type system. For currently invariant collection types, this would mean you can put in anything assignable to T, anything taken from it is only usable as T. The collection remains invariant for assignability. This can significantly improve the ergonomics when T is specified by the user, but also damages possible inference of T, as object is always a valid inference. This would also partially remedy the Sequence vs MutableSequence problem if we went this route for this problem, but I hope that sufficiently explains why this proposal is distinct from anything solving json related problems.
I had to think about this particular phrasing a bit more. I think we need to be more explicit with what’s being referred to here, and I think you’ve placed meanings in a different location from what Jelle was describing.
Spot the difference:
assignable to the set of all possible types of list[T] where T is assignable to A
assignable to all of the possible types list[T] where T is assignable to A
(move where forall is placed in a formal statement and you can convert between these)
This would be one of the myriad reasons why I don’t want to start this as supporting any user-provided predicate, and limit the valid places for it to where there actually is a distinction from Any, even without a predicate for an initial proposal, knowing it could be expanded upon later.
.