Lifting the "Self or associated type" constraint on existentials

[dabrahams (Dave Abrahams)]

@algal

I suspect many people, like me, are still a bit confused about the fundamental reason for these limitations. I’d still like to understand it better! (For instance, I am embarrassed to admit, I doubt I could define “existential” to my satisfaction. I bet I’m not the only one.)

Fwiw, I am sure the essential reason for the confusion then was that prototocols with associated types behaved almost exactly unlike protocols in objective-c, which was most everyone’s reference point. I suspect this is the same thing which you are saying more precisely now, when you distinguish protocols-for-defining-constraints and protocols-for-type-erasure, but I’m not sure.

Hi @algal,

I think I'd like to answer this in reverse order:

I agree that the reference point of protocols in Objective-C was probably a source of confusion. However, I think the bigger source of confusion is that we have one thing called protocol that

• plays two distinct roles that overlap significantly in their capabilities
• can only support a fraction of its declared API in one of its roles

You can define the “existential type P” to be the most specific possible common supertype of all types conforming to the protocol P. [I don't think it's crucial that anyone understand why we use the word “existential,” FWIW. I consider that an artifact of nerdy language research whose explanation does almost nothing to illuminate the meaning of the word].

As for the fundamental reasons for this difference, it's what I said in the talk: capturing an instance of type T as an existential type erases type information, and in particular, type relationships. If you work through a couple of examples with a protocol like:

protocol P {
   init()
   associatedtype A
   func f(_: A) -> A
}

you'll see that the most specific common supertype of types conforming to P has no usable API. The compiler can't provide a working init() because it has no way to know which subtype to create. I suppose it could provide a trapping init(). But it can't even provide a trapping f because that would have to take a type that is a subtype of every conforming type's A and return a type that is a supertype of every conforming type's A. In a world where Never was a true bottom type, that could be func f(_: Never) -> Any, but of course even that doesn't satisfy the requirements for f, which say it has matching parameter and return types.

The proposal to generalize existentials says that we'll have the compiler figure out which part of a protocol's API can be used on its existential type without violating the soundness of the type system, and simply forbid the use of the other parts when handling the existential. From my point of view, without an explicit declaration from the programmer that certain parts are intended for use on the existential type, the author, users, and maintainers of a protocol have to do some fairly subtle reasoning about type soundness to understand what they are getting.