We need `Not` to properly express some parts of Intersections

[mikeshardmind]

TBD, see #16

Edit: This issue is currently incomplete and is being used to transparently post components of it for review. Please hold comments on the following topics for now:

• Too complex
• Unneeded
• Type-checking implementation detail vs specification

Please do comment if you can directly find fault in any labeled resource that is a fault arising from an internal self-consistency problem.

Please hold comments that think something isn't relevant. Many of these are either to help illustrate later details or to provide helpful resources, but may not become part of the pep itself. The goal is to start by being correct, then to refine our definitions to be as simple and succinct as possible from there, while having the proof of that correctness available as a resource. We can cut sections for irrelevance when we have the full picture, not before.

If there is an issue with this after all is presented, please point it out then. I am not spending my time translating abstract logic to Python's type system and to a form that people are more familiar with as simply an exercise in doing so. I'm doing so because Python doesn't have a formalized type system, so we need to put it into the language people here are all familiar with and use so that we can look for any fault in it from that shared point of understanding.

Intersections get extremely into the weeds of type theory when considering a language with no formalized type system, only a set of not fully internally consistent rules. Please do not expect that proofs be simple when the situation itself is not. We can come up with simple procedures after we have correctness shown.

[DiscordLiz]

• Not is needed to decouple ordering from overload sets, allowing Intersections to be unordered
• Not and XOR are invalid on Gradual types with current knowledge and theory

I assume @mikeshardmind can fill in the rest based on other discussion, please do not wait on me feeling like explaining this.

[mikeshardmind]

@mniip and @DiscordLiz both had things that arose from abstract logic in discord. I understand them, but I'm still wrangling some of how to best succinctly express them. There has been a lot of discussion today, so I may not get to explain all of this today/tonight. If people would like to read through the details on Discord, they can, but it is a lot to reparse through, and I do not mind taking the time to come up with an accurate formulation of the ideas requiring this, but need some time to do so.

[mikeshardmind]

I'm not putting the whole thing tonight, I'm exhausted.

1. The order of overloads currently matters
2. We do not want the order of Intersection operands to matter (ie. A & B should equal B & A)
3. Because A and B can each have overloads, 1 conflicts with 2
4. To resolve this, we can determine which overloads have disjoint parameter lists and which are specializations of each other, and synthesize new overloads which do not rely on the ordering to be correct. This requires type negation to do.
5. In the case that 4 cannot be resolved, it is either unsafe or ambiguous as any arbitrary order would make A & B != B & A
6. By 5, we need to resolve 4 to ensure a use is safe given the information available to static analysis.

---

I will not elaborate with python examples or with a formal proof of this tonight.

---

There has already been prior art on this done in Rust in an accepted RFC https://github.com/rust-lang/rfcs/blob/master/text/1210-impl-specialization.md#permitting-overlap

For those who do not want to read the whole thing, this is the opening to the section I have linked:

The goal of specialization is to allow overlapping impls, but it's not as simple as permitting all overlap. There has to be a way to decide which of two overlapping impls to actually use for a given set of input types. The simpler and more intuitive the rule for deciding, the easier it is to write and reason about code -- and since dispatch is already quite complicated, simplicity here is a high priority.

If you believe that you can show a simpler method than this, you may want to reach out to the rust team as well 😃

While overloads and intersections do not fully map to rust's impls, and dispatch on type to an implementation is different to overloads, the static typing concerns are highly related, and it can still help us ensure we pick the most accurate return type from available implementations.

[mikeshardmind]

one additional quote from the Rust RFC:

One nice thing about this approach is that, if there is an overlap without there being an intersecting impl, the compiler can tell the programmer precisely which impl needs to be written to disambiguate the overlapping portion.

Which means we have a path towards helpful error messages with this as well. This may be more a concern of type checkers than this PEP, but the fact that the approach provides such a nice path is a big plus.

[DiscordLiz]

I don't know if this was clear to everyone else from the partial summary.

• Negation is needed to synthetically remove the ordering of overloads, but not for any of the steps above which are listed after it.
• Removing the ordering of overloads is necessary for many of the things we've all "agreed" on such distribution rules working properly.

I have not composed all of my thoughts on this into one post yet. I can show that type negation is necessary to remove the ordering via both type theory and topology, but I would prefer to stick to type theory given the problem domain. I would not mind being proven to have missed an alternative option for doing this, but it isn't as simple as "intersect the first on one side with the first on the other", and I believe it will become more clear why later. A hint to why this is the case is that it is possible to have a "smaller" compatible minimum bound than this in some cases, and that this also needs to interact with comparing which implementations can be seen as specializations of others after.

I would highly appreciate that people coming into this discussion be aware that a lot of this has been discussed elsewhere already, and, at least for why type negation is necessary to remove the ordering of overloads, it is only a matter of forming a "to the point" post explaining all of what has already been explored and the ramifications of it. Independently of what I have done, there's at least two other people who have each started some kind of machine verifiable formal proof of some of these conclusions. I do not want to discourage other contributors from voicing issues with what is later shown, to the contrary if I and others have been wrong on some of this show us. I am happy to engage in constructive contradictions. But I want them to actually be constructive and not a chore to respond to because enough detail was not included to refute something which claims to. When this happens, it can feel like people aren't even reading what each other are saying.

I also would want to encourage other people to come talk with us less formally about those things. @mikeshardmind has already committed to ensuring all of what is relevant gets summarized for at minimum an appendix to the PEP, so you will not be missing out after the fact if you do not, but people should be empowered to be a part of the precursor discussions as well. The discord link has been shared multiple times already, but here it is again

[diabolo-dan]

3. Because A and B can each have overloads, 1 conflicts with 2

Can I request this be expanded on? It seems untrue to me, or more specifically that it presupposes the need to synthesise the interface in a concrete way, and if that is the case I'd request for that to be expanded on.

[randolf-scholz]

I agree with @diabolo-dan here, in python A&B will only exist as an abstract static type, hence there is no need for a synthesized interface. If a user wants to implement a subtype AB of A&B, they are responsible themselves for creating a list of overloads for AB.foo that is compatible with both A.foo's overloads and B.foo's overloads. The type-checker can verify that this is compatible with (A&B).foo without ever needing a concrete realization of (A&B).foo.

[mikeshardmind]

Again, checking that a type is consistent with A&B (assignment) is different from checking that if all you know is A&B and not the type that will be assigned to A&B, what you concretely know about the use

The difference is here:

def f(x: A & B):
    return x.foo(...)  # Method foo
    # or
    return x(...)  # Callables A & B
    # We only know foo by the minimum bound provided by A & B here.
    # We need a procedure to correctly determine the minimum bound.

This isn't about if some type is A & B, but if some use is A & B.

It needs to be part of the spec as well, not just "well leave the details to type checkers", because you can return the result. This makes it part of a library's typed API, if type checkers diverge here, this would be pure chaos.

When it comes to methods of classes or callables in general, the way parameter lists and return types interact with substitution is slightly more complicated. While parameters may be more specific, return types must not be for the same original parameter types (Yes, I spelled out variance of callables without naming each one, intentional to avoid another point of confusion for people)

Because of this, if we only know Intersection.foo we need to be able to determine a few things.

1. does exactly one intersection operand provide foo? (use that one)
2. Are all of the provided foos identical? (use any)
3. Can they all be shown to be direct specializations (use the most specific one)
4. (In the case of Callables) Are they compatible? (determine a minimum bound)

A few things about 4

• In the case of there not being any overloads, there might be required overloads to create compatibility. If this is the outcome, we need to determine what the least additional specification of overloads would be, without the order of overloads being important, as this defines the minimum bound.

• In the case of there being overloads, we need to show that the overloads are compatible (3) and find the minimum bound of them unordered(4) and (funnily enough) we still may have to add more overloads as above to determine a minimum bound.

• Never is always compatible, which is a hilarious way to break expectations some people may have. If we don't go through the steps of determining synthetic additional overloads which would create a minimum bound of compatibility, our only route is to just go "can't happen", when it clearly can. It's a hammer in search of screws if we don't first tighten down what we can.

If I need to figure out some more contrived examples to show it is necessary to do more than check consistency with each individually, I will later. The need for it was not shown by a direct example originally, and I'm more focused on summarizing correctly what was shown first as I have time.

[diabolo-dan]

This isn't about if some type is A & B, but if some use is A & B.

Some use is A & B iff the use is A or the use is B.

A type checker can check those independently to validate the use is valid at all.
If neither are valid, then the use is invalid.
If exactly one is valid, the return type will be the return type of the valid use.
If both are valid, the return your will be the intersections of the return types.

[mikeshardmind]

@diabolo-dan

If both are valid, the return your will be the intersections of the return types.

Yes, and how do you propose we resolve this without a concrete type (in the body accepting an intersection), and without handling determining what the minimum bound of that intersection is when it comes to callables that are not directly compatible but can be? That is what this issue is about.

It isn't just the intersection of the return types. A simple example of this was already shown yesterday in the long thread.

[DiscordLiz]

If people don't have anything additional to add that wasn't already argued, wait until this is fully explained. You're just creating the same arguments that end up wasting time having to be addressed when they could be being spent on detailing more of the problem space.

[mikeshardmind]

Generalized specialization from known type information

This is single, position only, required parameters for the sake of being building blocks for later

There are also some cases retained that only result in Never. These are not directly Never alone, as they may still intersect with other things in the chaining of intersections.

General forms (Table A)

Intersection	Simplification (if it exists)
(A) -> A & (A) -> B	(A) -> A & B
(A) -> A & (B) -> B
(A) -> C & (B) -> D	(A &~B) -> C & (B & ~A) -> D & (A & B) -> C & D
(A & ~B) -> A & (B & ~A)
(A) -> A & (B) -> B & (C) -> C
(A & ~(B | C)) -> A & (B & ~(A | C)) -> B & (C & ~(A | B)) -> C

General form, with B as a subtype of A and D as a subtype of C (Table B)

Intersection	Simplification (if it exists)
(A) -> A & (A) -> B	(A) -> B
(A) -> A & (B) -> B	(B) -> B
(A) -> C & (B) -> D	(A &~B) -> C & (B) -> D
(A & ~B) -> A & (B & ~A)	(A) -> A
(A) -> A & (B) -> B & (C) -> C
(A & ~(B | C)) -> A & (B & ~(A | C)) -> B & (C & ~(A | B)) -> C

General form, with B as a subtype of A and D is not a subtype of C (Table C)

Intersection	Simplification (if it exists)
(A) -> C & (B) -> D	(A &~B) -> C

General forms, A, B, C, D are mutually incompatible (Table D)

Intersection	Simplification (if it exists)
(A) -> A & (A) -> B	(A) -> Never
(A) -> A & (B) -> B
(A) -> C & (B) -> D	(A) -> Never & (B) -> Never
(A & ~B) -> A & (B & ~A)
(A) -> A & (B) -> B & (C) -> C
(A & ~(B | C)) -> A & (B & ~(A | C)) -> B & (C & ~(A | B)) -> C

---

These are some of the simplest examples here to use as a baseline reference with more complex things discussed later, this set follows entirely from basic subtyping rules. The specializations here could be seen as type-checker implementation details only if not for how we need to build on them to resolve more complex cases.

---

Edit: Removed things in the form (T) ->T, T: A | B. These were intended as template shorthand,, not TypeVars, but even with a definition of this included, it was determined more likely to cause confusion

[mikeshardmind]

How to decouple Ordering from Overloads

Note: This is the how portion, not the why portion

given a set of overloads, the overloads can be decoupled from having an ordering concern by finding those that are disjoint and those which are specializations of each other, then adding type negations to prevent the less specialized ones from being used for more specialized cases. Note that we only add the negations for parameters, not for return types.

An example given using the subtyping relationship B <: A

(overload) (A, B) -> A
(overload) (B, A) -> B
(overload) (B) -> B
(overload) (A) -> A
(implementation, not checked) (T, U=None) -> T

In this case, (B) -> B is more specific than (A) -> A

We can remove the ordering between these two by negating the more specific from the less specific

(A & ~B) -> A & (B) -> B

in the 2-ary cases of (B, A) -> B and (A, B) -> A, we have

(B, A) -> B & (A & ~B, B) -> A

This makes the full set

(A & ~B) -> A
(B) -> B
(B, A) -> B 
(A & ~B, B) -> A

but we can now freely re-order these, make other simplifications on them, and intersect them without an ordering concern as they have been made fully disjoint by specificity.

Now, lets explore the same, but without a subtype relationship

(overload) (A, B) -> A
(overload) (B, A) -> B
(overload) (B) -> B
(overload) (A) -> A
(implementation, not checked) (T, U=None) -> T

In this case, we need to ensure that (A, B) -> A takes priority over (B, A) -> A and (B) ->B takes priority over (A) -> A without the ordering mattering. You may notice that earlier, the subtype relation gave us a naturally higher specificity, and this wasn't required.

This can be accomplished in a similar manner by assuming a total ordering between parameter lists of the same arity representing an equivalent relation

for the lower priority, we negate all higher priority types.

So we keep (A, B) -> A and (B) - > B untouched as the highest priority in each arity

this makes the full set

(A, B) -> A
(B & ~A, A & ~B) -> B
(B) -> B
(A & ~B) -> A

but these are now freely reorderable, and do not need to be treated with the care of an overload

For one more case of this showing how this resolves with more types to order:

(overload) (A) -> A
(overload) (B) -> B
(overload) (C) -> C

Absent a subtype relationship to order on most specific, we can allow this to become unordered while retaining the same priority with:

(A) -> A
(B & ~A) -> B
(C & ~(A | B)) -> C

[DiscordLiz]

The cases that simplify to (something) -> Never which need preservation are important because if we just removed them, we could reach incorrect results for (something) on an intersection with this. We can only completely remove anything which resolves as never when we are completely done intersecting.

An example of a slightly more interesting case for Types A,B,C and an unbound TypeVar T.

((A) -> A & (A) -> B) | (C) -> C) & (T) -> T

((A) -> Never) | (C) -> C) & (T) -> T

This is now (T) -> T, Where T is not A

Now it should be noted that (A) -> Never is compatible with (T) -> T,
so we can allow this case, but should we when it can never not error?

This one is more philosophical, and not born of necessity, necessity is the (de)ordering of overloads in parameters.
This is just one such example in which negation arises in the return type out of just logically possible things.

---

Once the ordering of overloads is removed, they can be treated as if they are just an intersection. This comes into play with correctly making other simplifications and selections, and with allowing the same logic to be applied to multiple parts of the problem. The ability for users to negate types also allows them to escape any ordering rules that exist currently. It also means type-checkers can have extremely efficient checking, but I've been convinced to save that part for an appendix.