SE-0309: Unlock existential types for all protocols

[xwu (Xiaodi Wu)]

@anthonylatsis

the mapping from some types to underlying types can be seen as a one-to-one relationship (every some type corresponds to a single conforming type).

Well, a many-to-one relationship, no?

[sighoya]

@anthonylatsis

I think the practical meaning lies in understanding the differences rather than trying to break down the terms.

I disagree, to understand the differences one needs to define semantics for the terms first. To be concrete, what is an existential, a compile time existential, existential containers, existential values, existential types, existential box, opaqueness.

Then, differences between the meaning of these terms can be inferred and reoccurring discussions about them can be eliminated.

@anthonylatsis

although some types and generic parameter types may also be defined via existential quantification.

What does that mean?
Did you refer to the point of assigning an any P to some P?
And if some P types can be defined in terms of existential quantification, why aren't these existential types then?

@anthonylatsis

The mapping from existential types to underlying types can be seen as a one-to-many relationship (every existential type corresponds to every conforming type)

Agree

@anthonylatsis

while the mapping from some types to underlying types can be seen as a one-to-one many-to-one relationship (every some type corresponds to a single conforming type)

Disagree, as this would imply some P != some P at the type level, which is a contradiction.
I think you are talking about three entities here:

opaque type: some P
underlying type transparent to the type system: (global1(),Int)
underlying type opaque to the type system: Int

And yes, between the "underlying type transparent to the type system" and "the underlying type opaque to the type system" we have a many-to-one mapping, e.g. Int can be mapped to type (global1(),Int) and (global2(),Int) but Float can't be mapped to (global1(),Int) as changing function global1 to return Float would also change the transparent type to (global1(),Float).

The mapping from some P to the "underlying type transparent to the type system" as well as to the "underlying type opaque to the type system" is one-to-many.
To see this, just change return 2 to return 2.0 in a function with some Number as return type and the function is still sound.

[xwu (Xiaodi Wu)]

@sighoya

Disagree, as this would imply some P != some P at the type level, which is a contradiction.

Mmm, some P != some P is in fact the fundamentally unique raison d’être of opaque types.

[sighoya]

@xwu

Mmm, some P != some P is in fact the fundamentally unique raison d’être of opaque types.

This is like saying: x != x or 2 != 2.
I think you mean underlyingTypeOf(var1:Some P=...) != underlyingTypeOf(var2: Some P=...) which can be true depending on the ....

[xwu (Xiaodi Wu)]

@sighoya

This is like saying: x != x or 2 != 2 .

Yes, it’s somewhat like .nan != .nan.

[xAlien95 (Stefano De Carolis)]

@sighoya

This is like saying: x != x or 2 != 2 .

Yes, at the type level it's true*

let x: some Numeric = 2
let y: some Numeric = 2

x == y  // Binary operator '==' cannot be applied to operands of type 'some Numeric' (type of 'x') and 'some Numeric' (type of 'y')

*: unless your some Numeric refers to an already specified some Numeric

let x: some Numeric = 2
let y = x

x == y

y is still some Numeric, but it's some Numeric (type of 'x') and type identity works.

[sighoya]

@xwu

Yes, it’s somewhat like .nan != .nan .

:/ Hmm..., good point.
Reminds me a bit of anonymous types/values where we create hidden tags to disambiguate them, i.e. make them false comparable
So we have:

x: some P => x: some Var(x).P
y: some P => y: some Var(y).P
some Var(x).P != some Var(y).P

Confusing, that a type is defined by its context.

@xAlien95

let x: some Numeric = 2
let y: some Numeric = 2

x == y  // Binary operator '==' cannot be applied to operands of type 'some Numeric' (type of 'x') and 'some Numeric' (type of 'y')

That doesn't prove some Numeric != some Numeric as we don't compare types with each other. Equality isn't defined in general for some types but most of the time for the underlying type, so we have:

(Var(x),Int) for x and (Var(y),Int) for y which aren't comparable to each other because the Self behind some P mismatches.

[Moximillian (Mox)]

@sighoya

opaque type : some P
underlying type transparent to the type system : (global1(),Int)
underlying type opaque to the type system : Int

While it’s very useful for you and other language theory oriented people to use very finegrained terminology for these things, I don’t think it fair to keep telling people are wrong when they use terms like opaque or existential with the meaning that is commonly used within swift community.

It’s like travelling to China and telling everyone they should all speak only English because that’s a language that you use.

I don’t know if I got the translations right, but I think:
Opaque type == ”underlying type transparent to the type system”
Existential == ”existential container type”

It would allow for more people to understand and also contribute to the discussion, if we don’t spend so much time trying to redefine the words themselves.

[sighoya]

@Moximillian

While it’s very useful for you and other language theory oriented people to use very finegrained terminology for these things, I don’t think it fair to keep telling people are wrong when they use terms like opaque or existential with the meaning that is commonly used within swift community.

You must differentiate, I don't say that someone is wrong just that I disagree.

@Moximillian

It’s like travelling to China and telling everyone they should all speak only English because that’s a language that you use.

That's a good example. But to understand Chinese it would be great to know terminology.

@Moximillian

I don’t know if I got the translations right, but I think:
Opaque type == ”underlying type transparent to the type system”
Existential == ”existential container type”

Here, the same. It would be nice to be sure about that, not "I think". You know to what I'm referring, too.

@Moximillian

It would allow for more people to understand and also contribute to the discussion, if we don’t spend so much time trying to redefine the words themselves.

Yes, and exactly, therefore, it would be nice to have a definition placed somewhere, for example in the type spec.
I'm not the only one who is confused, I see this discussion bubbled up again and again.
Moreover, just someone said something in this thread doesn't mean it is carved in stone.

That's all I wanted to say, I will leave the discussion.

[DeFrenZ (Davide De Franceschi)]

@sighoya

Reminds me a bit of anonymous types/values where we create hidden tags to disambiguate them, i.e. make them false comparable

You could say it's exactly what's happening here. If you have

let x: some Numeric = 1
let y: some Numeric = 2
let z = x // some Numeric

you could effectively read it as

let x: some Numeric #1 = 1
let y: some Numeric #2 = 2
let z = x // some Numeric # 1

and probably the compiler does something like this under the hood to keep reference of when you use "the same some".
And this is because some Numeric isn't a type. So writing some Numeric != some Numeric is not wrong as much as it doesn't make sense. A bit like 1/0. But some Numeric #1 is a type, but the type isn't available to the code... "opaque" comes effectively from the fact that this type is hidden

[Moximillian (Mox)]

@sighoya

Yes, and exactly, therefore, it would be nice to have a definition placed somewhere, for example in the type spec .
I'm not the only one who is confused, I see this discussion bubbled up again and again.
Moreover, just someone said something in this thread doesn't mean it is carved in stone.

Opaque type actually has a formal definition in the link you referred. There’s also dedicated section discussing opaque types, and to me that gives a pretty good sense of what is meant with it in the swift context.

The Swift Programming Language: Redirect

Elsewhere in the swift book, existentials are mentioned briefly:

Protocols as Types
Protocols don’t actually implement any functionality themselves. Nonetheless, you can use protocols as a fully fledged types in your code. Using a protocol as a type is sometimes called an existential type , which comes from the phrase “there exists a type T such that T conforms to the protocol”
The Swift Programming Language: Redirect

@sighoya

That's all I wanted to say, I will leave the discussion.

I find your contributions valuable and interesting, I just wanted to point out that discussions can easily end up in deadlock, if we are not using shared terminology. I do not claim my interpretation is necessarily correct, I just try to use the terms as described in the swift book and commonly used by the developers of the swift language itself, which most typically manifests in the individual proposals like the one for opaque types: https://github.com/apple/swift-evolution/blob/master/proposals/0244-opaque-result-types.md

[anthonylatsis]

@sighoya

What does that mean?
Did you refer to the point of assigning an any P to some P ?

Not at all. It simply means we could use the existential quantifier ∃ (shorthand for "there exists") to symbolically define a some type. Existential quantification is just a tool for building symbolical expressions and is found all over the place in mathematics (take the definition of the limit of a sequence).

@sighoya

And if some P types can be defined in terms of existential quantification, why aren't these existential types then?

There may very well be a book on type theory where the formal equivalent of a some type is classified as an existential type. Another thing is the way these formal terms got twisted and adapted for Swift.

@sighoya

Disagree, as this would imply some P != some P at the type level, which is a contradiction.
I think you are talking about three entities here:

opaque type : some P
underlying type transparent to the type system : (global1(),Int)
underlying type opaque to the type system : Int

It only seems a contradiction. some P is the extent to which we are able to express an opaque type in Swift code. The full identity of a some type is not hidden from us because the concept demands it, we simply lack a surface-level mechanism for expressing it today. An opaque type is opaque because the underlying type (Int) is opaque to the caller, not because the identity of the opaque type is syntactically opaque in certain aspects; opaqueResultTypeOf(global1) would have also been an acceptable syntax for an opaque type.

P.S. Discussion or not, remember that you are always welcome to ask questions.

[1oo7 (J. Shad.)]

@filip-sakel

To be clear, we don't propose altering the existential syntax; let a: any Hashable will be invalid.

Sorry to resurrect this old thread but I am just curious... will any Hashable still be invalid once SE-0309 goes live?

I feel like it would be pretty awesome if we get to replace the likes of AnyView, AnyPublisher, AnyHashable etc. with any View, any Publisher, and any Hashable, so there must be some reason why this would be illegal.

So really this is just me asking why it's illegal :D

[filip-sakel]

SE 309 didn't introduce the any syntax to retain a focused scope. This is what SE 335 was for, which came after this proposal, meaning that any Hashable will, indeed, be valid.

However, replacing AnyHashable with any Hashable involves that the existential type conform to itself, which has not yet been proposed.

[John_McCall]

AnyHashable is also quite a bit more complex than any Hashable: it has a special representation and aggressively bridges to Objective-C (when ObjC support is enabled). Because of ABI stability and its special-case ties to bridging, it is hard to imagine it going anywhere.

[filip-sakel]

We could, however, self-conform the Hashable existential, when/if this feature is introduced so that those who want a syntactically lighter-weight alternative can use it. Moving to any Hashable would also alleviate the commonly used special-case conversion of Hashable->AnyHashable from most code, so that most users’ mental model is simplified. Perhaps it could also bring about performance improvements?

[davdroman (David Roman)]

The same could be proposed for any Equatable too. Not all existentials should self-conform by default because the implementation isn't always possible/intuitive, but IMO having any Equatable and any Hashable self-conform would be tremendously useful.

[Karl]

Checking the equality of values with different types can be hard to define in a way that's usable. That's why Equatable uses Self in the first place rather than Any. The issues with any Equatable emerge naturally because it's just an awkward concept to begin with.

Rather than self-conformance for any Equatable, I think it would be more valuable to look at ways we can preserve type identity, so you can replace them with some Equatable more often.

For example, Array<any Equatable> is supported today, but Array<some Equatable> is not - and IMO that would be a better solution. It actually addresses the conceptual weakness and fixes things by making the language more expressive. It works because we can communicate to the compiler more precisely.

(Note: in practice, I suspect it will more likely be some MyProtocolWhichRefinesEquatable instead of just plain "Equatable")

There can still be cases where you need to erase type identity and reestablish it later with some kind of unboxing/generic binding and conditional casting, but hopefully we can make those situations rare enough that it isn't such a big deal.

[Zollerboy1 (Josef Zoller)]

@Karl

Checking the equality of values with different types can be hard to define in a way that's usable. That's why Equatable uses Self in the first place rather than Any . The issues with any Equatable emerge naturally because it's just an awkward concept to begin with.

With the implicit opened existential proposal we could do something like this, no?

extension any Equatable: Equatable {
    public func ==(lhs: any Equatable, rhs: any Equatable) -> Bool {
        areEqual(lhs, rhs)
    }

    private func areEqual<T: Equatable>(_ a: T, _ b: any Equatable) -> Bool {
        if let b = b as? T {
            return a == b
        }
        return false
    }
}

[Karl]

You can write that, but it wouldn't hold that a == b gives the same result as b == a.

In your example, you're taking the type T from the value of the left-hand side. So if we have a value of a base class, base, and a value of a subclass, sub, we can test base == sub because the RHS (sub) can be downcast to the base class type. However, sub == base wouldn't work - the RHS is now base, which can't be downcast to the subclass type.

Weird stuff like that is why it's best to steer clear of mixed-type equality, IMO. It's more trouble than it's worth.