T & Any and variance

[CarliJoy]

@mark-todd One has to be really careful and diligent with phrasing of these examples. In particular, we should try to avoid using the word "property" if we mean a regular attribute and not a @property, because it makes a huge difference whether we talk about a mutable attribute (⇝ invariant), or a read-only property (⇝ covariant).

Let's take a look at a modified version of Eric's example from earlier:

class Movie:
    info: MovieInfo

    @property
    def metadata(self) -> Metadata:
          return _get_metadata_from_server(...)

T = TypeVar("T")

Now, what is the interface of T & Movie?

• info is a mutable attribute. Therefore, Movie is invariant in info, which logically translates to the statement: S <: Movie ⟹ type(S.info) is MovieInfo, i.e. if S is a subtype of Movie, then the type of S.info must be MovieInfo.
  • Under ④, (T & Movie).info is of type T.info & Movie.info = Any & MovieInfo.
  • However, a clever type-checker should be able to deduce, even under paradigm ④, that this can be simplified to MovieInfo due to the invariance. (The only alternative is that T and Movie are incompatible)
• metadata is a read-only property, so covariant, meaning S <: Movie ⟹ S.metadata <: Movie.metadata.
  • Under ④, (T & Movie).metadata is of type T.metadata & Movie.metadata = Any & Metadata (*), which is still guaranteed to be a subtype of Metadata, but could have a much wider interface.
  • Due to covariance, Any & Metadata cannot be simplified away in this case.

So even with ④, exact inference can be made when types are invariant, and in fact this gives an alternative solution for people worried about intersection with Any by simply using invariant types. (Presumably one would want a way to manually mark read-only properties as invariant)

(*) In principal it should be something like Any & property[Metadata], but for technical reasons property isn't even generic yet in typeshed, so let's pretend for the moment it's simple a read-only, covariant attribute...

_Originally posted by @randolf-scholz in https://github.com/CarliJoy/intersection_examples/issues/31#issuecomment-1881694200_

[CarliJoy]

@randolf-scholz I am not an expert with variance. Could you extend your example for a static function as well as a method and explain what happens with arguments/return values as well?

[randolf-scholz]

I have the feeling that there might be still something wrong here, no more time atm

Here is a summary in tabular form: let `A` and `B` be two types that both share an interface `.foo` (could be attribute/method/...) with types `S≔type(A.foo)` and `T≔type(B.foo)`. Co-/Conta-/Invariance just means that if `A2 <: A`, then we must have `A2.foo <: A.foo` / `A2.foo :> A.foo` / `A2.foo == A.foo` respectively. Then from basic rules of subtyping it follows then that the type `X ≔ (A&B).foo` has to satisfy the following conditions in order to satisfy LSP: | X ≔ (A&B).foo | B.foo covariant (<:T) | B.foo invariant (==T) | B.foo contravariant (:>T) | |---------------------------|-----------------------|-----------------------|---------------------------| | A.foo covariant (<:S) | X <: S and X <: T | X <: S and X == T | X <: S and X :> T | | A.foo invariant (==S) | X == S and X <: T | X == S and X == T | X == S and X :> T | | A.foo contravariant (:>S) | X :> S and X <: T | X :> S and X == T | X :> S and X :> T |

Note: Interfaces are usually considered to have the following variance.

- Read-only ↔ covariant (read-only attributes / methods / function return types) - Write-Only ↔contravariant (function argument types / write-only attributes) - Mutable↔invariant (mutable attributes / TypeVars that appear both as inputs and outputs.)

Assuming `B` is untyped, we want to replace `T` with `Any` in the table above. A fundamental assumption of gradual typing is that when we see `Any`, we assume it is a stand in for whose place an actual type can be substituted which is compatible. This should result in the updated table | X ≔ (A&B).foo | B.foo covariant (<:T) | B.foo invariant (==T) | B.foo contravariant (:>T) | |---------------------------|-----------------------|-----------------------|---------------------------| | A.foo covariant (<:S) | X <: (S&Any) | X <: S | X <: S | | A.foo invariant (==S) | X == S | X == S | X == S | | A.foo contravariant (:>S) | X :> S | X :> S | X :> (S&Any) |

Detailed Explanation

1. First row: - `X <: S and X <: T`: simply becomes `X<:(S&Any)`, as there are no compatibility constraints - `X <: S and X == T`: compatibility demands that `T<:S`, and for any `X<:S`, it is feasibly possible that `T` happens to be `X`, so this becomes `X<:S` - `X <: S and X :> T`: compatibility demands `T<:S`, and for any `X<:S` it is feasibly possible that `T` happens to be `X`, so this also becomes `X<:S` 2. Second row: Here, compatibility demands that `T==S` in all 3 cases, so we get `X==S` 3. Third row: - `X :> S and X <: T`: compatibility demands that `S<:T`, and for any `X :> S`, it is feasibly possible that `T` happens to be `X`, so this becomes `X:>S` - `X :> S and X == T`: compatibility demands that `S<:T`, and for any `X :> S`, it is feasibly possible that `T` happens to be `X`, so this also becomes `X:>S` - `X :> S and X :> T`: this simply becomes `X :> (S& Any)`, as there are no compatibility constraints

Of course, if `B` is untyped we have no clue about the variance of `B.foo`, so we need an extra criterion to decide which constraint to pick per row. We can again argue by compatibility: It is feasible, that `B` is covariant/invariant/contravariant in `foo`, so our condition should cover all 3 cases: - Row 1: `X <: (S&Any) ∧ X <: S ∧ X <: S` ⟺ `X <: (S&Any)` - Row 2: `X == S ∧ X == S∧ X == S` ⟺ `X==S` - Row 3: `X :> S ∧ X :> S ∧ X :> (S&Any)` ⟺ `X :> (S&Any)` Therefore, we end up with the following final result: | X ≔ (A&B).foo | B untyped | B.foo co (<:T) | B.foo inv (==T) | B.foo contra (:>T) | |--------------------|---------------|------------------------|---------------------|------------------------| | A untyped | X==Any | X<:(Any&T) | X==T | X:>(Any&T) | | A.foo co (<:S) | X<:(S&Any) | X<:(S&T) | X==T if T<:S else ↯ | T<:X<:S if S:>T else ↯ | | A.foo inv (==S) | X==S | X==S if S<:T else ↯ | X==S if S==T else ↯ | X==S if S:>T else ↯ | | A.foo contra (:>S) | X:>(S&Any) | S<:X<:T if S<:T else ↯ | X==T if S<:T else ↯ | X:>(S&T) | **Please let me know if you find any errors in this analysis.** **EDIT:** We must also be careful to distinguish the cases when `B` is untyped and when merely `B.foo` is untyped / partially untyped, since in the latter case we may have variance information.

[mikeshardmind]

I believe the consistency based rule we are going for does not require we do extra work for Variance with Any that isn't already being covered more simply than this. I'll be including notes on the effective variance we expect in a few examples. IF this needs further discussion, please reopen expanding on that.