Git Product home page Git Product logo

intersection_examples's People

Contributors

carlijoy avatar junkmd avatar mark-todd avatar mikeshardmind avatar neilgirdhar avatar osintalex avatar tomasr8 avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

intersection_examples's Issues

Indirect Intersections with isinstance and Any

There is a long discussion ongoing in how to handle Any within intersections in #1 and #31.

A form of intersections are already implemented in some type checkers, i.e. MyPy

# test.py
import typing as t

class A:
    ad_mix: "A"
  
class B: ... 

class C(A,B):  ...

class D:
    ad_mix: "D"

a: A

# Intersections are done already correctly
if isinstance(a, int): # A&int
    t.reveal_type(x)  # Revealed type is "__main__.<subclass of "A" and "int">"  -> A&int
    t.reveal_type(x+10) # Revealed type is "builtins.int"

# It even find a already existing class that is the subclass of both
if isinstance(a, B): # A&B
    t.reveal_type(x) # Revealed type is "test.D"  -> "A&B"


# If things can't be combined, as there is a conflict in LSP it will return `Any`
if isinstance(a, D): # A&D
    t.reveal_type(a) # Revealed type is "Any"      # Can't be resolved as there is a conflict in classes

any: t.Any

if isinstance(any, A): # Any&A
        t.reveal_type(D)  # Revealed type is "A"

The solutions discussed in #1 and #31 could change the behaviour of if isinstance(any, T). Therefore I propose to include a sentence like.

"… Even so isinstance acts similar to an intersection, types of Any for that an instance T was determined are always treated as T and never as T&Any."

A second proposal is that we include a sentence like "An isinstance of a variable of type T1 for a type T2 that isn't a subtype of T1 should be treated as T1 & T2 by a type checker in type narrowing."

Note: Any can't be used a type for isinstance.

What do you think?

I would like to prevent surprises no matter what we decide in #1 or #31.
Also having only one "kind" of intersection would make things easier IMHO.

Handle "impossible" intersections

This issue is about handling an "impossible" intersection by static type checkers. We consider two cases:

It must be transformed to Never

Arguments in favor:

It is up to the type checker to reduce it or not

Arguments in favor:

  • @erictraut argues that the conditions are complex and expensive.
  • @erictraut argues in the context of reduction and normalization.
  • @CarliJoy argues that there are problems caused by inconsistent typing definitions in the standard library.

(Please edit this comment. I haven't gone through the whole issue to add links to everyone's arguments.)

General Organisation / How to continue / Consensus Finding

In the different issues a lot of valid points were given, that the current specification is too complex and unsound.

I recognized that I really lack the fundamentals to keep track with discussion about type theory.
Still as user I would like to see this implemented (especially for Mixins). Therefore I would like to help as much as I can i.e. in trying to keep order with issues, help organizing and maybe write things/read through them from an "normal (=not experienced with type theory)" Python user perspective.

@erictraut already did very good job in writing some general rules and applying them to the T & Any Problem

This could probably replace the current specification - hopefully I soon find time to put this into the current document.

I also was so free and included the original work of Kevin Millikin (@kmillikin) and Sergei Lebedev (@superbobry) from there PEP inside the specification document in order to create more context.
Hote that they also created PEP draft propsal for a python type system spec. This could also help clarify some thing here.

I see still the open point how to handle 'impossible' intersections that needs some discussion before reaching a consensus.

@mikeshardmind @tomasr8 @NeilGirdhar @JelleZijlstra @DiscordLiz -> Maybe you could also summarize in your understanding the current consensus and disagreement we have? This helps finding the pain points of disagreement and finding a consensus.

One note about organisational stuff: I will be on holiday 2023-07-28 t 2023-08-07 and also as I don't want to be a door keeper of any kind feel free to become a contributor and edit the draft yourself :-). I am happy for every help.

sample use case: Type object with particular constructor signature

Annotating 'Type object with particular constructor signature' requires intersection.

Suppose we have a

# returns cached instance of SomeClass or creates a new instance
def get_cached_or_create(klass):
  if _is_cached(klass):
    return _get_cached(klass)
  else:
    print(f"creating instance for {klass}")
    instance = klass()
    _set_cached(klass, instance)
    return instance

Now, how should we type get_cached_or_create?

Naive typing would be to accept type[T]:

T = TypeVar('T')

def get_cached_or_create(klass: type[T]) -> T:
  ...

However, it does not express the fact T's constructor must be callable without argument.
Above signature suggests get_cached_or_create can be called with type object with any constructor signature.

The desired typing of get_cached_or_create in fact is:

T = TypeVar('T')

def get_cached_or_create(klass: type[T] & Callable[[], T]) -> T:
  ...

The collections section seems incorrect

It reads:

The general idea that an attributes of intersected types become unions holds also for all kinds of collections.

dict[str, int] & dict[bytes, float] => dict[str|bytes, float|int]
list[str] & list[bytes] => list[str|bytes]
tuple[str, float] & tuple[bytes, int] => tuple[str|bytes, float|int]

I think it should be:

dict[str, int] & dict[bytes, float] => Never
list[str] & list[bytes] => Never
tuple[str, float] & tuple[bytes, int] => Never

I think the section should just be removed, or it should read that the rules follow from covariance/invariance/contravariance.

Add isinstance behavior

This should probably work and do the obvious thing:

if isinstance(x, A & B)

since it works for unions.

Handling of `Any` within an Intersection

There is a great deal of confusion about handling the Any type within an Intersection.

In Python, Any is both a top type (a supertype of all types), and a bottom type (a subtype of all types). Python has a gradual typing system, meaning that it will never be required that everything is typed. Everything that is not typed is considered Any.

We examine five ways to handle intersections with Any:

  • Any is removed from intersections: T & Any = T.
  • Intersections containing Any become Any: T & Any = Any.
  • Any is forbidden in intersections: T & Any is an error.
  • Any is not reduced within intersections.
  • Any is only considered in an intersection in deference to non-gradual types.

Remove Any from Intersections

Arguments in favour

Arguments against

An Intersection containing Any becomes Any

Arguments in favour

Arguments against

  • @mikeshardmind argues that this reduces the effectiveness of gradual typing by discarding constraints.

Disallow Any in Intersection

Arguments in favour

Arguments against

  • @randolf-scholz argues that they can arise from sequential instance-checks.
  • @randolf-scholz argues that code could "synthesize an intersection type dynamically".
  • @erictraut argues that "intersections with Any will arise, often in the bowels of the type checker's logic where there's no good way to report an error to the user".

Treat T & Any as irreducible in general

Arguments in favour

Arguments against

  • at least @CarliJoy has no idea how that should work in the reference, how should a type checker handle it in detail?
  • @DiscordLiz and @mikeshardmind each argued that functionally this has all the same issues as treating it as Any

Any is only considered in an intersection in deference to non-gradual types.

Arguments for

Arguments against

  • @NeilGirdhar argues that it breaks logical consistency with unions, which are the dual of intersections.

⚠️ Rules for contribution to this Issue

  • Do not post, if your argument is already handled within the description
  • Posts should include include a proper header i.e. ## Arguments in favour to Disallow Any in Intersection
  • If you want to correct or specify things in the description write a comment in the format "Old" > "New"

The general idea is that I will update the description, allowing the discussion to be included in the PEP and prevent a discussion going in circles.

I will react with 🚀 once I included something in the description.

Tracking issue for all other issues

In the spirit of #8, I thought it might be a good idea to have an issue that categorizes all of the issues we have so that we can keep track of what needs to be done. Please feel free to edit this post to add, remove, change the classification, or change the status of an issue. Ideally, all issues should be resolved (closed) before this PEP is complete.

Motivating examples

Some of these will end up in the motivation section of the PEP. We desperately need more motivating examples. If you've contributed or reviewed type annotation pull requests, it may be worth scanning over them to see if intersections would have helped. It would also be good to scan the Pyright and MyPy issue trackers.

Required behavior of intersections

These include type checker behaviors as well as runtime behavior (we may want to split them). Some of these will end up in a behavior section of the PEP.

  • #1 Once we agree on this, then we can copy into the PEP: arguments from the "support" section of the accepted idea, and arguments from the "against" section of the rejected ideas.
  • #5
  • #10
  • #16
  • #21

Adding a negation operator

#17 proposes adding Not as part of this PEP. If it is added, then it should probably get its own section.

Survey

The survey section can be populated from #14.

CPython implementation

A CPython implementation should probably be linked. @tomasr8 is working on one in #9.

Bugs

These are possible errors, oversights, or addenda for the PEP that should be resolved:

TypedDict rules are unsound

I am looking at the current rules in https://github.com/CarliJoy/intersection_examples/blob/main/specification.rst#typeddicts, which say that if two TypedDict members of an intersection share the same field with different types, then the intersection contains a field that is a union of those two types.

from typing import TypedDict
class A(TypedDict):
    a: int
class B(TypedDict):
    a: str
def takes_a(a: A) -> None:
    print(a["a"] + 1)
def takes_ab(ab: A & B) -> None:
    assert_type(ab["a"], int | str)
    takes_a(ab) # legal, A & B is compatible with A
b: B = {"a": "x"}
takes_ab(b) # legal, but throws an error at runtime

A similar hole:

def takes_ab2(ab: A & B) -> None:
    ab["a"] = 42 # legal, as ab["a"] is of type int | str
b2: B = {"a": "x"}
takes_ab2(b2)
print(b2["a"]) # now it's an int!

Possibly the type of ab["a"] should actually be int & str, not int | str.

Organising the naming poll for `OrderedIntersection`

Just adding a new thread for this, as it occurred to me that when the PEP is ready we'll need to figure out how we organise the naming poll on python discuss that was mentioned before. I think we'll need to narrow down the list of available names before it goes to a poll, as right now we have many many possibles. I think perhaps each of us should eventually submit one name each that's our favourite, and we put these in a poll (as that should reduce it to 6 options or so).

Also here's the names list as it is currently - feel free to add to it: https://docs.google.com/spreadsheets/d/1rJlt5UfSOkVey2g5p634mKa0NdsCdpuZDwDfs4CnsiY/edit?usp=sharing

I've also been thinking some more about the points I've been discussing with @mikeshardmind, and this led me to some new thoughts about names. We established in our discussions that really OrderedIntersection is a combination of structural types, that aren't necessarily classes that can be combined together via inheritance, but are sort of structures layered on top of one another to produce a final result.

This led me to another "family" of names, where the idea is that it's kind of like a stack of differently shaped papers layered on top of each other (in art I've found this is called "paper layering"). I'm thinking a name of this type would describe quite accurately how objects are combined overlapping each other in a stack, and maybe avoid the parallel to inheritance that doesn't always apply.

Some names:

  • Overlap - this one was suggested before, but I now think maybe has more merit than I initially thought, as it describes how classes overlap one another.

  • Stack - again conveys this idea of ordered layering although maybe has too many parallels to heap and stack

  • Layered - similar to stack

  • Bundle - perhaps not ordered enough as a name

Looking for synonyms for Stack also led me to Heap and Pile, but again is this perhaps too much overlap with existing programming terms.

`TypedDict` with OrderedIntersection

Following on from from a discussion with @mikeshardmind in #41 I thought it might be worth separating this into a new thread.

This concerns how TypedDict might be combined with other classes in the new intersection - I'll start with the non-controversial case:

class A(TypedDict):
    foo: int

class B(TypedDict):
    bar: int

x: OrderedIntersection[A,B] = {"foo":1, "bar": 1}

So far so good. Now let's consider what happens if we mix it with another class or Protocol

class A(TypedDict):
    foo: int

class B:
   def test(self) -> int:
      return 1

x: OrderedIntersection[A,B] = ??

Now here we reach an issue, there's no way to make this class. A TypedDict traditionally cannot be combined with another class - and with good reason! We cannot introduce other methods to a TypedDict. But this led me to another case:

from typing import Protocol, TypedDict, TypeVar, OrderedIntersection

T = TypeVar("T")

class X(Protocol):
    def __str__(self) -> str:
        return "test"

def foo(t: T) -> OrderedIntersection[T, X]:
    ...

class Test(TypedDict):
    x: int

x: Test = {'x': 1}

y: OrderedIntersection[Test, X] = foo(x)

Here the use of __str__ in the X protocol does not impinge on the definition of Test, as this matches the function signature of a method already found on TypedDict (dict). So this intersection should be allowed.

My conclusion from this is TypedDict can only be combined with other TypedDict, or Protocol's that do not expand on the existing methods of dict.

An issue with the accepted definition of Union

The text in PEP 483 that describes how unions behave actually doesn't do a very good job as a definition of a union type.

  • Union[t1, t2, …]. Types that are subtype of at least one of t1 etc. are subtypes of this.
    • Unions whose components are all subtypes of t1 etc. are subtypes of this. Example: Union[int, str] is a subtype of Union[int, float, str].
    • The order of the arguments doesn’t matter. Example: Union[int, str] == Union[str, int].
    • If ti is itself a Union the result is flattened. Example: Union[int, Union[float, str]] == Union[int, float, str].
    • If ti and tj have a subtype relationship, the less specific type survives. Example: Union[Employee, Manager] == Union[Employee].
    • Union[t1] returns just t1. Union[] is illegal, so is Union[()]
    • Corollary: Union[..., object, ...] returns object.

This lists some facts that are indeed true if we were to interpret Union[A, B] as a static type that stands for a set of values that is a set-theoretic union of the sets that A and B stand for. However this does not actually define Union[A, B] to be that set.

Many have interpreted the first line: "Types that are subtype of at least one of t1 etc. are subtypes of this." as a definition:

C <: A | B if and only if C <: A or C <: B

However this is now how set-theoretic unions work, it is not in general true that $C \subseteq A \cup B \iff (C \subseteq A) \lor (C \subseteq B)$

Counterexample:
>>> A = {1}
>>> B = {2}
>>> C = {1, 2}
>>> C.issubset(A | B) == (C.issubset(A) or C.issubset(B))
False

What people probably are thinking of is the formula $c \in A \cup B \iff (c \in A \lor c \in B)$, which is actually true. But we cannot use this as a definition because that involves checking potentially infinitely many $c$. Instead we want a definition in terms of the <: aka $\subseteq$ relation.

This is a solved problem and I'll cut to the chase: the formulas that define set-theoretic unions and intersections are as follows:
$$C \subseteq A \cap B \iff (C \subseteq A \land C \subseteq B)$$
$$C \supseteq A \cup B \iff (C \supseteq A \land C \supseteq B)$$

The duality between intersection and union lies in reversing the subset relation, not in replacing an "and" with an "or". In fact it is a well understood idea that transitive relations play extremely poorly with "or", and extremely well with "and". Hence the above definitions both using "and".

What about $A \cap B \subseteq ...$ and $... \subseteq A \cup B$? We have these formulas, as corollaries of the definitions above:
$$(A \subseteq D \lor B \subseteq D) \implies A \cap B \subseteq D$$
$$(D \subseteq A \lor D \subseteq B) \implies D \subseteq A \cup B$$

Proof
  • Substitute $C = A \cap B$ into the first equation. LHS is true by reflexivity, so RHS must be true too. If we have $A \subseteq D$ then by transitivity $A \cap B \subseteq A \subseteq D$. Likewise if we have $B \subseteq D$. So in total if we have either $A \subseteq D$ or $B \subseteq D$ then we have $A \cap B \subseteq D$.
  • Same proof but with all relations reversed. Substitute $C = A \cup B$ into the second equation, RHS must be true. If $D \subseteq A$ then by reflexivity $D \subseteq A \subseteq A \cup B$. Same for $B$.
Note that these are one-way implications. Sufficient but not necessary conditions. There's once again a symmetry with reversing the subset relation, but no symmetry between "and" and "or".

In #1, here, @erictraut lists all 4 of these on equal footing, labelled "non-controversial". I want to emphasize that two of these involving "and" are actually definitions by universal property, and the two involving "or" are special cases/corollaries.

What does the PEP-483 paragraph actually define?

Most of the bullet list is actually describing a reduction procedure for type expressions involving class literals and unions. The proposed algorithm of checking C | D <: A | B with (C <: A or C <: B) and (D <: A or D <: B) only works exactly because each of A, B, C, D can only be a class, as the only other possible form - union - gets flattened first. However in presence of intersections this algorithm already fails:

A & (B | C) <: (A & B) | (A & C) vs A & (B | C) <: A & B or A & (B | C) <: A & C

I'll also cut to the chase here: you want to reduce the left hand side to a disjunctive normal form, and the right hand side to a conjunctive normal form. The | on the left and the & on the right can then be taken apart. But the & on the left and the | on the right cannot. Problems of the kind t1 & ... <: s1 | ... where t1, ..., s1, ... are class literals -- are in general irreducible and will require knowledge of the inheritance tree and whether a multiple inheritance child class exists/can be constructed.

The PEP should use & exclusively

The PEP is inconsistent and uses Intersection sometimes. It would be better to exclusively use the & notation, and mention the Intersection as existing solely in typing_extensions for backwards compatibility.

Naming 4 vs 5

Starting this thread after discussion on #31 about what Option 4 and 5 should be renamed to.

Rules of this thread as follows - post simply the name suggestion in the style:

Option 4 -> name
Option 5 -> name

Most thumbs up in a few days wins!

I'll post up any already suggested names to get the ball rolling

sample use case: return type of `@contextmanager` decorated functions

I want to contribute a real life use case that we encountered which may justify the needs of Intersection types.

Can anyone suggest an alternative without using Intersection?

from typing import *
from contextlib import AbstractContextManager, ContextDecorator, contextmanager

    
@contextmanager
def _hoge():
    ...
    try:
        yield
    finally:
        ...


def foo() -> ContextManager[Never] & ContextDecorator:  # How should we annotate this without Intersection?
    ...
    return _hoge()


# ====
# foo is used both as ContextManager and ContextDecorator

with foo():
    ...

@foo()
def bar():
    ...

NOTE: the spec of @contextmanager is here:
https://docs.python.org/3/library/contextlib.html#contextlib.contextmanager

Essentially, what the decorated function returns is a ContextManager that uses ContextDecorator mixin.

Union and Intersections

Intersection A & B

Type: Intersection of A and B. If A and B are both concrete types and not protocols, this must be a subclass of both. If either is a protocol, the protocol must be satisfied. If A or B is already an intersection, the intersections are combined.
Interface: The interface of A and B are both available and must not conflict.

(A & B) & C is equivalent to A & B & C

Union A | B

Type: Union of A and B. If A or B are already Unions, The unions are combined

Interface: The attributes, methods, and properties shared between A and B which have compatible types. If A and B use an identifier in conflicting ways, the accessor of the object cannot know which way it is used without checking.

(A | B) | C is equivalent to A | B C

(The below may seem contrived, but I think including it can assure the definitions we end up on remain consistent)

The order of intersections and unions matters

Unions of Intersections (A & B) | (B & C)

Type: a union of the intersection A & B and the intersection B & C
Interface: The shared compatible interface of 1) the combined interfaces of A and of B which must not conflict with each other and 2) the combined interfaces of B and of C which must not conflict with each other

(A & B) | (B & C) is equivalent to (A | C) & B

Intersection of Unions (A | B) & (B | C)

Type: Intersection of the unions A | B and B | C
Interface: The interface of both the unions A | B and B | C, where each of those unions has the shared minimum nonconflicting interface, and no permutation of union elements results in a conflicting interface for the intersection*

(A | B) & (B | C) is not equivalent to B & (A | C), but to (A & C) | (B & (A | C))

* A contrived case, to be sure, but...

class A(Protocol):
    def this(self: Self) -> Self:
        ...

class B(Protocol):
    def that(self: Self, other: T) -> T:
       ...

class C(Protocol):
    def this(self: Self) -> None:
        ...

Problematic = (A | B) & (B | C)

There are two possibilities here

  1. This reduces to: (A & B) | B | (B & C) due to the incompatibility between A & C
  2. This is considered unsatisfiable as a set of types

I believe 2 to be the correct interpretation. 1 results in a different interface than may be expected.

Why this matters when considering Any

This is a set of ordering and satisfiability constraints that works with the proposed update to the definitions of Any and Never. Should these orderings and constraints be considered undesirable, we may be back to the drawing board on handling Any

Originally posted by @mikeshardmind in #1 (comment)

Second opinions on a couple specific issues

So.. while working on something formal for #38, I'm left in a situation where there are a few corner cases I really don't like, and I think we need answers for.

  1. type[OrderedIntersection[T, U]] : The primary use case seems to imply that the class that satisfies this should be instantiable as T, but type is currently not type safe for __init__ (my displeasure at LSP exceptions for "pragmatic" reasons have already been expressed, and I dont think it's in scope to change that) so do users need to do
    OrderedIntersection[Callable[*expected_init_args, OrderedIntersection[T, U]], OrderedIntersection[T, U]] to actually have type safety here? This seems exceptionally verbose for a situation that shouldn't require this level of verbosity, especially since there's no way to just "copy" T.__init__'s signature, is there something we can do to improve this without fixing the fact that LSP is being ignored for constructors?

  2. What about intersections with members of the numeric tower? OrderedIntersection[HasDotHexMethod, float] allows fixing (one of) the type holes with it. Do we need to do anything else here? I'm leaning no and that we should, after this is accepted, look into fixing some things with the numeric tower and having protocols built with intersections that express common things people want to be able to allow for duck typed math while remaining type safe, but I think that doesn't require extra work here, but future work after, have I missed something that requires we consider it more ourselves?

Survey of other languages that support intersections

Numerous other programming languages (including some that support gradual typing) provide support for intersections. It would be instructive to learn from these other languages. How did they solve certain problems (e.g. intersection with Any)? How do they teach the concept to their developers?

Would someone like to volunteer to do a survey and a summary of learnings? This could help inform some of the discussions and design tradeoffs.

The summary could also be included as an appendix to the PEP, like I did for PEP 695. Such a survey would bolster confidence in the design and increase the likelihood of the PEP's acceptance.

Combination with `Self`

While reading specification.rst, I had a question that crossed my mind.

In below case, unless from __future__ import annotations is used, a NameError is raised at runtime.

The `LoginRequiredMixin` is designed to be used with the `View` base class which defines the
`dispatch` method.
Intersection types allow expressing that directly via
::
class LoginRequiredMixin:
def dispatch(self: LoginRequiredMixin & View, request, *args, **kwargs): ...
Source: https://docs.djangoproject.com/en/3.2/topics/auth/default/#django.contrib.auth.mixins.LoginRequiredMixin

To avoid runtime errors, it's necessary to use string literals for typing as shown below.

    class LoginRequiredMixin: 
        def dispatch(self: "LoginRequiredMixin & View", request, *args, **kwargs): ... 

For expressing that self is a mixin, in order to convey the same meaning without using string literals, I think that it should be typed with using Self.

    class LoginRequiredMixin: 
        def dispatch(self: Self & View, request, *args, **kwargs): ... 

Moreover, it's necessary to consider the interaction with methods and attributes that return Self.

class Mixin:
    me: Self
 
 
a: Mixin & Tb = a.me

In the above case, I think that b should be interpreted as Mixin & T by type checkers.

Any opinions would be appreciated.

Example use case for intersection

While reading through #29, I saw this comment:

I think the most important thing that we're missing are motivating examples.

So I figured I'd chime in with one that I run into very, very frequently! Hopefully this might be of some use. As some background: I make heavy use of decorators, both for "plain" callables as well as classes. In fact, a very common pattern I use is to combine both of them: decorators on methods to indicate some special behavior, and then a decorator on the class to collect those and do some kind of transform on them. I find this to be a pretty clean library API, and I use it all the time, for a wide variety of things. Critical to note here is that the decorators always return the original object, with a few attributes added to it. This is something I've found much more ergonomic than wrapping, but that's a whole separate discussion that I won't go into. The important thing to know is that adding class attributes to classes, or attributes to functions, is extremely common for me.

So without further ado, here is a (simplified) example of the kind of thing I currently use fairly frequently, but cannot correctly type-hint due to missing intersections:

class _Stator(Protocol):
    """This protocol is used to define the actual individual states for
    the state machine.
    """
    _is_stator: ClassVar[Literal[True]]


class _StatorAction(Protocol):
    _stator_cls_required: type[_Stator]

    # Ideally this would also include modifications to the function signature to
    # note that "stator" is required as the first positional arg


def stator_action[C: Callable](stator_action: C) -> Intersection[_StatorAction, C]:
    stator_action._stator_cls_required = get_annotations(stator_action)['stator']
    return stator_action


class StateMachine[SM](Protocol):
    """This protocol describes the return of the @state_machine
    decorator, and contains the implementations for the functions that
    are added into the decorated class.
    """
    _stator_actions: ClassVar[tuple[_StatorAction, ...]]

    @contextlib.contextmanager
    def from_checkpoint(self, stator: _Stator) -> Generator[SM, None, None]:
        """Creates a StatorMachina instance and loads the passed stator
        into it, setting it as the currently active state. Then, upon
        context exit, verifies that the state machine was exited either
        through a paused or final state, or by an error.
        """
        do_some_stuff()
        yield cast(MachinaProtocol, stator_machina)
        do_other_stuff()


def stator[T: type](stator_cls: T) -> Intersection[type[_Stator], T]:
    """Use this decorator to declare a particular node on the state
    diagram, including all of the internal state that needs to be stored
    at that point.

    It may be useful to pair this with a dataclass (and by "may", I mean
    "almost certainly IS"), but this isn't an absolute requirement.
    """
    stator_cls._is_stator = True
    return stator_cls


def stator_action[C: Callable](stator_action: C) -> Intersection[_StatorAction, C]:
    stator_action._stator_cls_required = get_annotations(stator_action)['stator']
    return stator_action


class Transition[S: _Stator]:
    """Return a state node wrapped in a Transition to denote a state
    transition. Can also be used to transition the state machine into
    a paused state.
    """

    def __init__(self, to_state: S):
        self._to_state = to_state


def state_machine[SM](cls: SM) -> Intersection[SM, StateMachine]:
    """This decorator marks a class as a state machine class, gathers
    up all of the stator actions, and constructs the internal machinery
    used by from_checkpoint to enforce correct state transitions.
    """
    cls._stator_actions = gather_stator_actions(cls)
    cls.from_checkpoint = _build_from_checkpoint(cls)
    return cls

This is then coupled with a bunch of other code that operates on _Stator, _StatorAction, etc. Code using this looks something like this (note that this is the unsimplified version; in reality most of those decorators are second-order decorators).

@dataclass
@stator(checkpoint=True)
class DmktSignupFormSubmitted:
    """The first state in both the initiation and reinitiation flows:
    the dmkt signup form was submitted.
    """
    email_address: str
    topics: list[str]
    dmkt_frequency: DirectMarketingFrequency


@dataclass
@stator
class DmktSignupTokenIssued(DmktSignupFormSubmitted):
    """The second state in both the initiation and reinitiation flows:
    we issued the relevant token.
    """
    token_id: UserVisibleUUID
    consent_copy_info: ConsentCopyInfo


@state_machine
class InitiationFromDmktSignup(StateMachine):
    """When a user goes through the direct marketing signup flow (ie,
    the mailing list signup), and no existing someone is found at the
    given email address, this state machine is responsible for guiding
    the person through the initiation flow, from initial form submission
    all the way through final double-opt-in confirmation, including the
    break in the middle for the email verification link.

    Note that, due to race conditions, just because a someone doesn't
    exist at the time of the dmkt signup, doesn't mean they don't
    concurrently complete a registration. So this flow can still result
    in a noop / error condition.
    """

    def __init__(self, *args, db_conn, **kwargs):
        """SUPER IMPORTANT: the db_conn needs to be within a transaction
        already!
        """
        super().__init__(*args, **kwargs)
        self._db_conn = db_conn

    @stator_action(DmktSignupFormSubmitted)
    async def issue_initiation_token(
            self, stator: DmktSignupFormSubmitted
            ) -> Transition[DmktSignupTokenIssued]:
        """The first step in the initiation flow: issuing a signup token
        that stores the submitted info.
        """
        consent_copy_info = await get_copy_info_for_flavor(
            UserfacingCopyFlavor.DMKT_MAILING_LIST_DOUBLEOPTIN_EMAIL)
        token_payload = DmktSignupResumeEncapsulation(
            email_address=stator.email_address,
            topics=stator.topics,
            dmkt_frequency=stator.dmkt_frequency,
            userfacing_copy_version_id=
                consent_copy_info.userfacing_copy_version_id)
        token_id = await issue_anonymous_token(
            {AttestedAction.DMKT_SIGNUP_RESUME: token_payload})
        return Transition(DmktSignupFormSubmitted(
            email_address=stator.email_address,
            topics=stator.topics,
            dmkt_frequency=stator.dmkt_frequency,
            token_id=token_id,
            consnt_copy_info=consent_copy_info))

    @resume_at_stator(DmktSignupEmailClicked)
    @stator_action(DmktSignupTokenIssued)
    async def send_initiation_email(self, stator) -> Transition[Paused]:
        """Once the token has been issued, we can send the initiation
        email containing the consent copy and a link to the token.
        """


# Note: I've removed the web framework stuff here so it's more concise 
async def form_submit_route_handler():
    maybe_someone_id = await get_someone_id_from_email(
        form_payload.email_address)

    form_submitted = DmktSignupFormSubmitted(
        email_address=form_payload.email_address,
        topics=form_payload.subscription_topics,
        dmkt_frequency=form_payload.contact_frequency)

    postgres_pool = Singleton.get(TaetimePostgres)
    async with postgres_pool.acquire_wrapped_conn() as conn:
        if maybe_someone_id is None:
            initiation = InitiationFromDmktSignup(db_conn=conn)

            with initiation.from_checkpoint(form_submitted) as initiation_flow:
                async with conn.transaction():
                    await initiation_flow.issue_initiation_token()
                    await initiation_flow.send_initiation_email()

There are a couple things I want to point out here:

  1. Note that there are 4 times I would use an intersection in the library code, even for that relatively short snippet. I believe there are even more in the test code for it as well (not 100% sure; I'm much laxer on typing with test code)
  2. For library consumers, it's impossible for me to correctly type-hint this code. Either they're missing the state machine actions -- which is terrible UX for someone writing code that interacts with the state machine -- or they're missing from_checkpoint, which is added by the @state_machine decorator. Explicitly subclassing StateMachine (as I did above) is a workaround for the from_checkpoint, but for more sophisticated decorators (or ones that are meant for functions and not for classes), this isn't an option. Furthermore, in reality you might want the @stator decorator to add some methods on to the class -- just like @dataclass does. At that point, you're really SOL.
  3. For library implementers, this also presents a problem. The actual implementations of the above decorators want to make heavy use of _Stator, _StateMachine, etc protocols internally, but they can't do that without sacrificing the API presented to library consumers. So as a result, the types applied to implementation functions are both overly broad (lots of unqualified types) and still fail type checking because the type checker doesn't know about the intersections, so I either have to wrap the implementation in two calls to cast (first to apply the protocol, then to revert to the original type), or I have to add a bunch of type: ignore comments.
  4. It seems to me like a lot of untyped code in the stdlib could probably be given types with the above protocol + intersection pattern; for example, tons of stuff in functools.

Generic type alias

The efforts of everyone involved in this project are remarkable.

I am curious whether Intersection is intended to allow generic type aliases like Union. I noticed that TypeVar is used in specification.rst, which may imply that generic aliases are possible.

If generic type aliases are possible, I think the specification would look like this:

class Foo: ...
class Bar: ...
class FooBar(Foo, Bar): ...

_T = TypeVar("_T")

# cases of Union...
# pre-PEP604
Spam = Union[_T, Foo]
# post-PEP604, pre-PEP695
Spam = _T | Foo
# post-PEP695
type Spam[T] = T | Foo
# simple usecases
def bacon(spam: Spam[Bar]): ...
bacon(FooBar())  # OK
bacon(Foo())  # OK
bacon(Bar())  # OK
bacon(1)  # NG


# cases of Intersection...
# pre-PEP695
Ham = Intersection[_T, Foo]
Ham = _T & Foo
# post-PEP695
type Ham[T] = T & Foo
# simple usecases
def lettuce(ham: Ham[Bar]): ...
lettuce(FooBar())  # OK
lettuce(Foo())  # NG
lettuce(Bar())  # NG
lettuce(0)  # NG

Any opinions would be appreciated.

Multiple inheritance and intersections.

We need to discuss how intersections relates to, and integrates with multiple inheritance. Points to discuss:

  1. Should class C(A, B) always be considered a subtype of A & B?
    1. Naive multiple inheritance creates order dependent MRO, but intersections are order independent. Usually, extra work needs to be done to ensure LSP-compatibility of C with both A and B.
    2. issubclass always considers C a subclass of both A and B, since it is a nominal subtype of both. This leads to a conflict with (i) if we also want isinstance(x, A&B)isinstance(x, A) and isinstance(x, B), since C might fail to be a structural subtype of A&B.
    3. Correctly implementing C(A,B) as a subtype of A&B generally requires overloads involving intersections. Since these are currently missing, there is lots of formally incorrectly annotated code. This has lead to type-checkers allowing certain false negative LSP violations: python/mypy#15790. How big is the problem? Eric tested against the mypy-primer and found over 2.3k errors.
  2. Should it be possible to subclass intersections? class C(A & B)
    1. Checks for existence of diamond problem at class definition time and raises TypeError in this case.
    2. This guarantees order-independence of the MRO.

Regarding ①, I still think considering C(A, B) always as a subtype of A&B is the reasonable choice, type-checkers can raise errors inside the class body of C at places where it violates structural subtyping. However, what I worry is that type-checkers will shy away from implementing python/mypy#15790, since tons and tons of legacy code will be incorrectly typed. This is where C(A&B) could come into play, with 2 benefits: Type-checkers can, without raising tons of errors in existing code bases, perform stricter checking inside such classes, and secondly, it can provide a second layer of security by testing for the diamond problem at class creation time.

CPython implementation of intersections

This is my stab at a reference implementation of the Intersection type in CPython:
https://github.com/tomasr8/cpython/tree/intersection-type
Contributions/improvements welcome!

Build instructions:

https://devguide.python.org/getting-started/setup-building/
TLDR:

git remote add tomasr8 https://github.com/tomasr8/cpython
git fetch tomasr8
git checkout --track tomasr8/intersection-type
make clean && make -s -j2
./python

TODOs

  • Intersection flattening (same as unions)
  • fix some copy&paste errors - references to Union and UnionGenericAlias and some docstrings
  • isinstance support
  • Incorporate python/cpython#105511 when it gets merged

Example

from typing import Intersection

Intersection[int, str]
Intersection[int, float, int]  # == Intersection[int, float] (deduped)
Intersection[int, Intersection[float, str]]  # == Intersection[int, float, str] (flattened)
Intersection[int]  # == int

# overloaded __and__ for types
int & str
type(int & str)

class T: ...
T & int

class A: ...
class B: ...
class C(A, B): ...

a = A()
c = C()

isinstance(a, A & B)
isinstance(c, A & B)

An argument against intersections. Or, having our cake, and eating it too.

Note: This is An argument for the intentional non-implementation of pure intersections, and instead use all of what we worked out to implement an alternative option that satisfies all currently supportable use-cases, while leaving the door open to full intersections. This is not arguing to throw away everything we've worked on, but to use what we worked out to help our collective use cases, productively. I am actively inviting any constructive detraction to this, as if there is something these cannot do that are "must haves" to go this route would require determining if intersections are must-have to support those uses.

(edited) Note 2: Where you see type[*Ts] and object[*Ts]it may make more sense to haveOrderedIntersection` There's more details at the end on this now

With Thanks to @DiscordLiz , @erictraut , @gvanrossum, @mark-todd, and @NeilGirdhar in alphabetical order (and no other order of particularity) for presenting each extremely strong, and opinionated arguments as well as some feedback that led to some self-reflection on why I felt so strongly about particular outcomes of this, I believe that there is a strong argument that without other constructs (such as negation, pick, and omit), there is not a good argument for the inclusion of the theoretical intersection, and that even with those, it might only make sense for that to work with structural subtyping.

However, that leaves an awkward question, how can we best handle the use cases that are certainly valid without them such that I can say we don’t need intersections? Have we really just wasted months of work? No.

The pitch: The order matters to us and to the behavior we want, so lets go with an ordered construct that's simpler and still does what we need.

type[*Ts] and object[*Ts]

First of all, my apologies to @mark-todd as when this was originally floated as an idea in a slightly different form by him in Discord, I stated the non-equivalence to intersections and that that should be separate, and we went back to working on intersections, but there’s a real question here I think we need to answer: Do these not solve every case we care about sufficiently? As originally stated, I would say that they didn't, but I believe I made a mistake in viewing these as something we should consider separately instead of as something which might do enough while being simpler. Exploring the idea further led to a slight tweak in which they appeared to me to solve all presented use cases that intersections could in the context of the current type system.

If it does, we can use the existing explorations to justify this construct instead and leave notes on rationale for anyone who wants to explore the difference between this and “true intersections” at a later date.

Background

The primary difference between all interpretations of Intersection which anyone involved has stated support for (For this I'm mostly looking at 4, 5, and the not fully fleshed out, hypothetical 6 from #31, #37) comes into play in things that are defined on multiple operands. Put another way, the unordered nature of Intersection as a parallel construct to Unions has some very unpleasant consequences. This became especially contentious when looking at what happens in non-disjoint cases and (implicitly non-disjoin) cases involving Any.

I iterated on this several times trying to find a solution that satisfied all the complaints from multiple parties, but every time there was still some corner case that had to favor one use over another, and given that we wanted intersections to also take up an operator in the type system & the consequences for needing two different constructs to express one version or the other wasn’t sitting right with me. With some time spent reflecting on it, I realized my primary issue with favoring any solution over another was that by promoting one to use & and another being relegated to requiring an import, we were necessarily putting some needs above others when there was no consensus on which behavior would be more common, or how this would reconcile with Any.

Enter, an alternative: type[*Ts]

This is ordered. People want option 4 for type[Any & T]? Write type[Any, T]. Want option 5? Write type[T, Any]. This reflects existing behavior, including the ordered nature with subclassing of Any.

Semantics

type[*Ts] does not create a new type at runtime. It creates a virtual type that has the bases *Ts. The order is not semantically considered for nominal subtyping, but should be considered when handling diamond patterns. As a return type or annotation, the type returned must have the bases *Ts. The bases do not need to be in the same order, but the types must resolve as if they were. object[*Ts] is the equivalent formulation for an instance of something of that type, reflecting the duality between type and object at both runtime and in the type system.

This allows the following class definitions (and many non-trivial others)

class Foo(A, B):
    pass

#and 

class Bar(B, A):
    pass 

# but also

class Baz(A, B, C):
    pass

to each work for type[A, B] or instances of these classes for object[A, B].

This also allows all of the current assumptions of nominal subtyping to apply to this construct.

In the case of protocols, each must be satisfied.

Because of this, it is enough at assignment to check that each type in Ts for type[*Ts] is satisfied, as any real object being passed would be checked when defined for LSP. LSP does not need to be checked for at time of assignment. At time of use, lookup should be done in order. By deferring to the fact that LSP violations would be detected elsewhere, the ordered search should be fine.

Examples:

class X:
    def foo(self) -> int:
        ...

class Y:
    def bar(self) -> int:
        ...

class Z:
    def foo(self, arg: bool = True) -> int:
       ...

def goodcase1(x: object[X, Y]) -> tuple[int, int]:
    return x.foo(), x.bar() 


def goodcase2(x: object[Any, X]) -> Any:
    return x.foo("bar")  # Any has precedence

def goodcase3(x: object[X, Any]) -> int:
    ret = x.foo()
    reveal_type(ret)  # int, not Any, X has precedence
    x.bar()  # not on x, but allowed, see Any
    return x.foo() 

def badcase1(x: object[X, Z]) -> int:
    return x.foo(True)  # definition from X takes precedence for differing type of method foo
    # And any attempt to create this type would cause an LSP violation,
    # you can't subclass from both and have X's definition have precedence, so the error surfaces in multiple places.

def goodcase4(x: object[Z, X]) -> int:  
     return x.foo(True)  # definition from Z takes precedence for differing type of method foo
    # It's possible to create this type as well.

Does this really cover all of our use cases?

It covers all of mine, including potential future cases with type negation as a separate construct. I've given it a lot of thought, and it seems to cover every case I've seen floated for intersections, both in this repo and elsewhere when discussing intersections for python, but the trick with type[A, B] allowing the mro order to be B, A is mandatory for that to be the case

There are potential cases that I would be blind to here, but we’ve limited the scope of this to non-disjoint overlap of types with differing types involved in resolution, and this allows handling of even that scope to a very large degree.

There are potentially other cases that can come up with higher kinded types. I have not explored in depth what this would mean with the inclusion of higher kinded types in python, because there is no strong prevailing push for these to use as a framework to explore. The temptation to view HKTs as in one of the languages that has them exists, but there’s no guarantee that any of these would reflect what is added to python’s type system. I believe that this composes properly with any reasonable future interpretation of higher kinded types, but will refrain from saying that HKTs could not re-introduce the need for a fully featured intersection.

What about type safety vs pragmatism and warnings?

  • The ordering gives the user control in the only place it matters.
  • It would be reasonable to implement a check that Any did not precede non-Any types in the order, or even to preclude it all together in a check, but this would be an optional additional constraint provided by a specific tool, not something that needs to be forbidden by the type system (And which would have negative effects on gradual typing to forbid outright)

What about ergonomics and obviousness of behavior?

In the most commonly anticpated case, of disjoint types, the ordering won’t matter. The definition above only cares about the order when mro would change a resolved type. The complex cases where the ordering will matter should be obvious, as it will be the same as the required mro order when defining the type.

What about backwards compatibility with type[T] (singular type)?

Behavior is unchanged, the definition here is compatible with and does not change the behavior of the current use of type[T]

What about not using type and object here?

It's probably better to use a new typing.OrderedIntersection instead of object for this, and allow it to compose with type with the existing semantics.

That would make one of the examples using decorators look like this:

# I believe this is in here, but a protocol indicating supporting rich comparison if not
from useful_types import RichComparable  

def total_ordering(typ: type[T]) -> type[OrderedIntersection[RichComparable, T]]:  # see functools.total_ordering
    ...

# Any type wrapped in this is now known to be both a nominal subtype of the original type
# while also being a structural subtype of the protocol RichComparison.

@total_ordering
class Point:
    def __eq__(self, other) -> bool: ...
    def __lt__(self, other) -> bool:  ...

Having our cake and eating it too

It may be less satisfying for some here to have done all this work and to walk away not implementing intersections, but if we use this work to implement something that handles as many cases as this would, and which leaves the edge cases in the user's hands to pick the behavior they want, I think we walk away accomplishing everything we set out to do by adding intersections, by not adding intersections. If this works for everyone here, the work wasn't a waste, but informative of what the issues would be with an unordered intersection, and an exploration of what the scope of difference would be with different solutions. This remains available as a reference to those revisiting and (if we go with this) we should absolutely document for history "why not a true intersection".

Sample use case: Returning from a dataclass-transform

This is a typical use of the PEP 681 dataclass_transform:

class DataclassInstance(Protocol):  # See usefule_types.experimental.DataclassLike
    __dataclass_fields__: ClassVar[dict[str, dataclasses.Field[Any]]]


@overload
@dataclass_transform(frozen_default=True, field_specifiers=(field,))
def dataclass(*, init: bool = True, repr_: bool = True, eq: bool = True,
              order: bool = False) -> Callable[[type[Any]], type[DataclassInstance]]:
    ...


@overload
@dataclass_transform(frozen_default=True, field_specifiers=(field,))
def dataclass(cls: type[Any], /, *, init: bool = True, repr_: bool = True, eq: bool = True,
              order: bool = False) -> type[DataclassInstance]:
    ...

What we would like to have, in fact, would be the following return types:

@overload
@dataclass_transform(frozen_default=True, field_specifiers=(field,))
def dataclass[T](*, init: bool = True, repr_: bool = True, eq: bool = True,
              order: bool = False) -> Callable[[type[T]], type[T] & type[DataclassInstance]]:
    ...


@overload
@dataclass_transform(frozen_default=True, field_specifiers=(field,))
def dataclass[T](cls: type[T], /, *, init: bool = True, repr_: bool = True, eq: bool = True,
              order: bool = False) -> type[T] & type[DataclassInstance]:
    ...

This would allow the type check to know that the returned dataclass is both a DataclassInstance (supports dataclasses.fields, dataclasses.replace, etc.) as well as remaining T.

Removing behaviour with OrderedIntersection and Protocols

Is there a way to remove behaviour from a type with OrderedIntersection and a Protocol, while having the resulting type still compatible with a type that supports that behaviour?

More concretely, suppose I was trying to replicate PEP 705 for list and create a type like list[ReadOnly[T]], let's call it ReadOnlyList[T]. This should have the following properties:

def foo(param: ReadOnlyList[Sequence[int]]) -> None:
  foo.append([4])  # Type check error: append is not accessible via ReadOnlyList
  foo.clear()  # Don't worry about making this illegal for now

bar: list[tuple[int]] = [(), (3,), (4,5)]
foo(bar)  # OK: tuple[int] is a subtype of Sequence[int]

Could I do that? Maybe with something like this?

class NoListMutatorMethods:
  def append(x: typing.Never) -> None: ...
  def extend(iterable: typing.Never) -> None: ...
  # etc
  
type ReadOnlyList[T] = OrderedIntersection[list[T], NoListMutatorMethods]

I feel like the answer is probably "no, there's no way to spell this using OrderedIntersection and Protocol", since you can't remove methods in a subclass/subtype. However, some of the conversation in #42 led me to wonder if I misunderstood the construct.

So I guess a prerequisite question is: Should both (or either) of these always be valid for any A and B where OrderedIntersection[A, B] is valid:

def as_first_type(x: OrderedIntersection[A, B]) -> A:
  return x

def as_second_type(x: OrderedIntersection[A, B]) -> B:
  return x

(I have not thoroughly read all the conversations up to this point, my apologies if this is already in there or is obvious to someone who understands MRO more than me :( )

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

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.

Intersections with `Callable`, in particular `Any` & `Callable`

In this issue, we shall discuss intersections with Callable. There is an unresolved issue with respect to Any & Callable, that stems from the following 2 axioms:

  1. Intersections with Callable are resolved by intersecting with an equivalent Callback-Protocol (see current draft)
  2. (x & y).foo = x.foo & y.foo (see Eric's outline: #1 (comment))

Both of these together can lead to infinite regress.

Therefore, we cannot use ① when intersecting function-types with function-types. One can distinguish 3 cases:

  1. Intersections of function-types with non-function-types: then we can apply rule ①
  2. Intersections of two function-types: regular subtyping and the more complicated function signature subtyping rules apply.
  3. Intersections of function-types with Any

EDIT: The suggestions below are outdated. The intersection with Any is irreducible. What needs to be discussed is what happens when the type is attempted to be evaluated with arguments args.


As I see it, there are 2 options of how to resolve ③:

For a strict interpretation of Any as an unknown type, Any could feasibly be Callable[..., R], which is a "consistent" subtype of Callable[[T1, T2, ..., Tn], R]. It follows that:

Any & Callable[[T1, T2, ..., Tn], R] = Callable[..., R]

The consequence is that (Any & T).foo(*args, **kwargs), is valid for any method foo of T, which as expressed in the Any intersection thread causes some pains, as it makes Any & T behave very similar to Any itself (only attribute types and function return types are preserved)

An alternative approach would hinge on a slight re-interpretation of Any in the context of intersections. One could demand that Any shall be interpreted as a disjoint type from whatever it is intersected with (= maximum compatibility). That is, in Any & T, we interpret Any as an unknown type that presumably shares no overlapping methods with T. This leads to

Any & Callable[[T1, T2, ..., Tn], R] = Callable[[T1, T2, ..., Tn], R]

I.e. we come back full circle to question if Any can be simplified away from intersections. Under this premise, we would have 3 simple rules, as I mentioned in #1 (comment)

  1. Any & T is an irreducible form
  2. (Any & T).fooT.foo if T implements foo
  3. (Any & T).barAny if T does not implement bar

So, does it make sense to have a general exemption to the rules #1 (comment) when intersecting Any with function-types?

T & Any and variance

@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 #31 (comment)

Motivation section

The motivation is really uncompelling. It describes what intersections do, but not why we need them. I think it would be better to dig through the mypy issues to find various problems that require intersection to solve them and present them under motivation.

For example, this one: python/mypy#9424:

from typing import Optional, TypeVar

U = TypeVar('U', bound=Optional[int])


def f(u: U) -> U:
    if u is None:
        return None
    assert isinstance(u, int)  # removing this line causes it to pass.
    return u

works with working intersections since u will have static type int & U.

Support variable intersections

I just want to mention one more example here, which requires Union and Intersection, which is when the number of things intersected is variable. This can happen when TypeVarTuple are involved, and it kind of implies that a speccing of empty unions and empty intersections is necessary. (See python/typing#1362)

from typing import TypeVarTuple, Union

items = TypeVarTuple("items")
protocols = TypeVarTuple("protocols")   # something like tuple[type[Protocol], ...]

def pick_random_element(tup: tuple[*items]) -> Union[*items]: ...
    """Return random element form a tuple."""
    # if tuple is empty, raises an exception ⟺ return `Never`.

def create_intersection_protocol(tuple: tuple[*protocols]) -> type[Intersection[*Protocols]]: ...
    """Creates the intersection of pairwise disjoint protocol classes."""
    # if intersection is empty, returns a protocol that matches with any class.

EMPTY_TUPLE = ()
pick_random_element(EMPTY_TUPLE)  # should reveal as `Never`.
create_intersection_protocol(EMPTY_TUPLE)  # should reveal as `object`!?

Note that bounds are (not yet) supperted by TypeVarTuple, so the latter cannot be hinted properly right now.

Originally posted by @randolf-scholz in #12 (comment)

Rekindling Intersection

I'm adding this here as well as on the Discord, in case this has more visibility. I've been trying to make sense of all the discussions that happened in August, and where that might leave the PEP. The number of outstanding issues (as far as I can tell) seems now limited to essentially just the Any discussion, as well as some edge cases with dataclass transforms. In some way this is good news, as it limits the number of things that need to be still discussed.

As a general path to completion:

  1. Agree a set of example tests that are coherent and reflect the same implementation.

  2. (optional) Ideally we would have a working mypy implementation of Intersection that passes the tests using the new system.

  3. Ensure the examples are consistent with the pep.

I would suggest a kind of fresh start for development - anyone who's still interested in development of this, please thumbs up this message and we can organise a call with everyone.

Interest in discussing topics from here at the PyCon US Typing Summit?

Jelle and I are starting to look at organizing a Typing Summit at PyCon US 2024.

We are still working with the conference coordinators to find the date, but the summit will be on one of the main conference days (Friday May 17 - Sunday May 19).

I was wondering whether you all think that the topics you've been discussing would be worth a presentation and discussion (or maybe two - I can see there are a lot of specific issues as well as some more conceptual questions about the semantics of types in general).

You'll have to pardon me jumping in here without having caught up on all the discussion; I'll try to catch up more but it will likely take me a week or two, and one of the reasons I think this is worth bringing up at the Typing Summit is to help get folks like me who haven't been following up to speed.

I also joined the discord so we could discuss there that's preferable.

How to proceed from here

Maybe this is a "me issue" and not that this can't be done right now, but I'm unsure how to meaningfully make progress in specifying OrderedIntersection. As far as I'm concerned, it should be as simple as.

For something to be consistent with assignment to a variable with a type specification of OrderedIntersection, it must be consistent with all operands of the OrderedIntersection. For the use of something that is an OrderedIntersection to be consisdered consistent, it must be consistent with the first relevant type found in the OrderedIntersection.

All of the rationale for that is already covered over in #38 , the rationale and explaining the rationale is not the issue I'm having.

Based on a lot of other discussions about the typing spec, I don't think it should be specified much more than what is above.

Examples of practical effects and comparisons, and why that's the decision? sure, but this should be extremely clear that these are examples based on the current state for the PEP process, and the examples should not be taken as limitation on intersections, and instead should be updated if the examples ever become wrong due to other changes to other types.

Based on the direction of other parts of typing, it doesn't seem like such a sparse definition will be accepted. I think overspecifying this is a road to compositional incompatabilities.

For instance, the discussion we had about this with TypedDicts. If we decided to say any more and actually say it can't compose TypedDicts with non-typed dicts only because there is no legal way to do this currently, then the spec for intersection has precluded a change to TypedDict that could allow it. The consistency based definition will allow a user to specify such an intersection, but they won't be able to create something to assign to that intersection (without a cast). Such uses then allow disovering what the use cases for expanding on TypedDict may be, and only the specification for typed dict would need to change for the use to be fully legal later on.

The consistency-based rule is rather simple and leaves what is and isn't compatible to the types within the intersection, but the entire direction of the typing spec seems to be trying to come up with increasingly precise, narrow, and even intentionally-limited definitions instead of definitions that state the minimum behavior and generalize, and It's been hard to find a way to describe intersections that doesn't feel wrong as a result, either for being out of place in the specification and unlikely to be accepted by those who want precise and narrow definitions, or for being precise and narrow when that's more limiting to all future constructs without needing to be.

I could use some other guidance here because if I'm off base, and I should just write the simpler definition and explicitly reject a more narrow one in the PEP itself to avoid the issues of composition and that is a direction we want, then I can finish the draft much sooner as there I need far less language to go this route, and I think I've been expending too much time trying to reconcile narrow definitions.

Interpretation of type `Any & T`

Following on from the lengthy discussion here #1, it was concluded that Any & T is the best resultant type for intersecting Any. This is symmetric with the way union works Any | T -> Any | T. Conversation on this new thread will investigate the types of the attributes and methods of this intersection type. Just a note, inspired by @CarliJoy we can number and summarise different interpretations. We should also seek to again create a real world example that explores the new types, and compares different interpretations.

Also if a summary of each new interpretation could be succinctly provided alongside a usage example that would be grand :)

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.