Survey of other languages that support intersections

[erictraut]

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.

[mikeshardmind]

If nobody picks this up before next weekend, I'll pick it up then, but I'd like to work on some of the other tangential things here first. Should things like Rust's traits being similar in nature and use to how an intersection of protocols would be used also be included in this?

[erictraut]

Thanks for volunteering! Please include any aspects that you think might be useful in informing the spec for Python.

[ippeiukai]

📝 TS's guide on intersection is here: https://www.typescriptlang.org/docs/handbook/2/objects.html#intersection-types

[mikeshardmind]

This paper differs from python, treating Any as an unknown element of the set of all types, but defines unions and intersections of types via the [consistent] subtyping relationship rather than by value. https://www.irif.fr/~gc//papers/icfp17.pdf This may be a useful lens for this appendix later, and may also be useful to any future redefinition of Any in Python, as with this definition of unions and intersections, The definition most equivalent here would be that Any is an unknown element in the set of all possible types. With this definition, Any can't be Anything, but it can be anything compatible with all of the other static types that are known. Essentially, there needs to be a possible type that fits in the gap for the use of Any to be sound, even if the programmer has not expressed that type.

Examples of how this paper would treat Any, which came up from a discord conversation with @mniip

Edit: Removed an example, see post below that goes into more clear detail on what this paper says for Any & T.
What I concluded for what it says about the assignability of things that are only known to be Any itself leaves a little that isn't quite proven here, but I believe it can be proven, and may work on this later.

[mikeshardmind]

In Kotlin T & Any is a non-nullable generic type. (essentially, all T and all of it's possible subtypes)

https://kotlinlang.org/spec/type-system.html#intersection-types

Kotlin also handles some cases that arise in intersections by approximating some types which may otherwise not be directly denotable by users with a specific set of rules here: https://kotlinlang.org/spec/type-system.html#type-approximation

[DiscordLiz]

Might be useful for the appendix. It's a little more general, but related to some of the sticking questions. https://github.com/rust-lang/rfcs/blob/master/text/1210-impl-specialization.md#hazard-interactions-with-type-checking

[DiscordLiz]

This paper differs from python, treating Any as an unknown element of the set of all types, but defines unions and intersections of types via the [consistent] subtyping relationship rather than by value. https://www.irif.fr/~gc//papers/icfp17.pdf This may be a useful lens for this appendix later, and may also be useful to any future redefinition of Any in Python, as with this definition of unions and intersections, The definition most equivalent here would be that Any is an unknown element in the set of all possible types. With this definition, Any can't be Anything, but it can be anything compatible with all of the other static types that are known. Essentially, there needs to be a possible type that fits in the gap for the use of Any to be sound, even if the programmer has not expressed that type.

Examples of how this paper would treat Any, which came up from a discord conversation with @mniip

# x can only be Literal[1] or Literal[2], no possible value for Any could result in otherwise
x : Literal[1, 2] & (Literal[1] | Any)
# equivalent formulation, x can still only be Literal[1] or Literal[2], so Any & T looks like T in this form.
x : Literal[1] | (Literal[2] & Any) 

y: Any = ...
z: A & B = y  # if it can be detected that A & B is impossible, the assignment itself is unsound as there isn't an instance of Any to suit it.

for the assignment based on y: Any, z: A & B, A&B impossible, Any: Never.

It appears that you think this follows out of the formal relation between A GType and set of STypes, but I would appreciate an explanation of what you think the conclusion here is that doesn't use a "python what-if" as an example as It is hard to be sure any leaps are soundly shown. If it was only this example, it would be entirely correct, but there's more to showing it to be correct than this, even if it looks obvious. If you're going the formal route, you need to show all your work, I know you know that.

As a result of that, this may not be a good example for the appendix. I don't want to say that your summation of what this means is wrong, it very well could be correct, but I think you need a little more substance to show to have it be checked as correct as well. In particular

With this definition, Any can't be Anything, but it can be anything compatible with all of the other static types that are known.

I think this is slight misstatement, but it might be equivalent, I'd need to work it out. If you're mentally mapping what was ? to python's Any, then Any is just all possible unspecified types.

It's a really subtle difference, and it may or may not matter formally, but you have to check that.

[mniip]

Any as an unknown element of the set of all types

I think it helps to be a little more specific here.
https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=b7ca4b0e6d3119aa341af73964dbe38d341061dd defines a type theory including something they called ?, that matches the semantics we want for Any in python: "this part of the type has not been specified yet so we don't do typechecking here". They also contrast how it is different from a top type (Ω in their notation, object in python): def f(x: int) -> Any: return x and def g(x: Any) -> int: return x are both valid from the gradual typing perspective.

https://repositorio.uchile.cl/bitstream/handle/2250/140079/Abstracting-Gradual-Typing.pdf expands on that notion and proposes a set-theoretic semantics for gradual types. We have the universe of static types that values actually range over, and then we have the universe of gradual types that extends the static types with Any. A gradual type is then interpreted as a set of static types it could be standing for. Note that this is a different notion from how a static type is interpreted as a set of values. The object gradual type corresponds to a set of one static type, object, which in turn corresponds to the set of all values. The Any gradual type corresponds to the set of all static types.

Finally, the paper in question, https://www.irif.fr/~gc/papers/icfp17.pdf , extends these semantics to include union and intersection types. Of extreme importance is the fact that unions and intersections are connectives for the static types. We use them to more accurately describe a set of values, rather than to describe the partial information known about a gradual type.

The counterintuitive nature of Any comes from the fact that we have two layers of "is a set of", and the subtle distinction between the two. The set of values in a static type reflects the values that we can expect to see in a hypothetical runtime. The set of static types in a gradual type reflects the possible ways the programmer may have edited the program and completed the type signature to be fully typed.

Now for the example:

x : Literal[1] | (Literal[2] & Any) 

No matter what the programmer substitutes for Any, the result can only be either of two static types: Literal[1, 2] (if the substituted static type contained the value 2), or Literal[1] (otherwise). So this gradual type corresponds to the set of these two static types. Once again this corresponds to the fact that the programmer has not yet made up their mind which of the two it should be. This in contrast to y : int | str where the programmer has made up their mind, and they have specifically decided that the variable y at runtime can contain the values from the set that is the union of all int values and all str values.

By playing the same covariance/contravariance trick with Literal[1] | (Literal[2] & Any) and Literal[1, 2] & (Literal[1] | Any) (which is an equivalent gradual type, it represents the same set of static types), we can see that not only do we have X & Any =/= X but also X | Any =/= Any.

[NeilGirdhar]

@mniip I linked your argument in the main comment of #1. Please let me know if I misinterpreted your comment.

[Feuermurmel]

In Kotlin T & Any is a non-nullable generic type. (essentially, all T and all of it's possible subtypes)

To avoid confusion, note that Kotlin's Any is not the same as Python's. Kotlin's Any is the Top Type excluding null (Any? is the actual the Top Type, comparable to Python's object). So T & Any being treated as everything in T except null follows from normal set intersection and not some special handling of Any.

Additionally confusing is the fact that Scala's Any is the the Top Type (including null).

AFAICT Kotlin's dynamic seems to be more like an equivalent of Python's Any.

[mikeshardmind]

As we've come to a point where all of the options we are giving consideration of any kind to only differ in the overlapping portion of an intersection:

• Kotlin doesn't allow such an overlap (You can't have the diamond pattern required to have a distinction between the options considered in Kotlin) Kotlin does synthesize the minimum interface.
• typescript picks a "winner" implementation for overlapping types with an undocumented sort.

[mikeshardmind]

Closing this for now, the most useful takeaways from this are in the WIP draft now. Can reopen if we think more comparisons should be drawn.