> On May 29, 2016, at 6:38 AM, Thorsten Seitz <[email protected]> wrote: > An, now I see what you mean. You are right, P ::= ∃ t : P . t is a > constrained existential type defining a subtype relationship. > Thanks for enlightening me! > > I haven’t perceived a protocol as an existential up to now, probably because > my understanding has come from Haskell where subtyping does not exists and > where therefore a hidden unbound type parameter plays a central role (see > definitions below) which has made me believe that an associated type is > necessary. But for simple protocols this role is indeed taken by the > conforming type. The difference is that this is equivalent to subtyping > whereas associated types (as another form of hidden unbound type parameters) > are not, resulting in two kinds of protocols. > Is there another terminology to distinguish between those two kinds?
It's not a standard restriction or really even a necessary one. It's an artifact of earlier implementations of both the type-checker and the runtime representation of protocol conformances. RE: the type-checker, it used to be the case that calls on existentials were awkward special cases: the type-checker didn't actually "open" the existential as a rigid type variable, it just magically ignored self and patched things together later. That's a type-checking strategy that's extremely prone to soundness bugs, so a harsh restriction is required. Fortunately, it's also a type-checking strategy we've abandoned, although there's still work to be done to build associated types correctly for opened existentials. RE: the runtime representation, it used to be the case that you couldn't recover associated type information at runtime from a protocol conformance and so it had to be passed separately; that could have been supported in the existential representation as well, but we knew we wanted to change that about protocol conformances, and we didn't want to introduce a great deal of complexity for an unnecessary intermediate position. So I wouldn't sweat trying to formally describe the current situation, because it's a "temporary" implementation limitation. John. > > -Thorsten > > > "Existential types, or 'existentials' for short, are a way of 'squashing' a > group of types into one, single type. […] > data T = forall a. MkT a“ > (https://en.wikibooks.org/wiki/Haskell/Existentially_quantified_types > <https://en.wikibooks.org/wiki/Haskell/Existentially_quantified_types>) > > "Existential quantification hides a type variable within a data constructor.“ > (https://prime.haskell.org/wiki/ExistentialQuantification > <https://prime.haskell.org/wiki/ExistentialQuantification>) > > "For example, the type "T = ∃X { a: X; f: (X → int); }" describes a module > interface that has a data member named a of type X and a function named f > that takes a parameter of the same type X and returns an integer. […] Given a > value "t" of type "T", we know that "t.f(t.a)" is well-typed, regardless of > what the abstract type X is. This gives flexibility for choosing types suited > to a particular implementation while clients that use only values of the > interface type—the existential type—are isolated from these choices.“ > (https://en.wikipedia.org/wiki/Type_system#Existential_types > <https://en.wikipedia.org/wiki/Type_system#Existential_types>) > > > >> Am 27.05.2016 um 19:36 schrieb John McCall <[email protected] >> <mailto:[email protected]>>: >> >>> On May 25, 2016, at 7:07 AM, Thorsten Seitz via swift-evolution >>> <[email protected] <mailto:[email protected]>> wrote: >>> This is unfortunate, because then the meaning of "existential" and >>> "non-existential" in Swift are just the opposite of their respective >>> meaning in standard terminology :-( >> >> I don't know what you mean by this. The standard terminology is that an >> existential type is one that's directly existentially-quantified, e.g. ∃ t . >> t, which is essentially what a Swift protocol type is: >> P ::= ∃ t : P . t >> P.Type ::= ∃ t : P . t.Type >> etc. Language operations then implicitly form (erasure) and break down >> (opening) those qualifiers in basically the same way that they implicitly >> break down the universal quantifiers on generic functions. >> >> If you're thinking about Haskell, Haskell's existential features are >> carefully tied to constructors and pattern-matching in part because erasure >> is a kind of implicit conversion, which would not fit cleanly into Haskell's >> type system. (Universal application also requires an implicit >> representation change, but that doesn't need to be reflected in H-M systems >> for technical reasons unless you're trying to support higher-rank >> polymorphism; I'm not up on the type-checking literature there.) >> >> John. >> >> >>> >>> -Thorsten >>> >>> >>> Am 25. Mai 2016 um 14:27 schrieb Brent Royal-Gordon <[email protected] >>> <mailto:[email protected]>>: >>> >>>>> AFAIK an existential type is a type T with type parameters that are still >>>>> abstract (see for example >>>>> https://en.wikipedia.org/wiki/Type_system#Existential_types >>>>> <https://en.wikipedia.org/wiki/Type_system#Existential_types>), i.e. have >>>>> not been assigned concrete values. >>>> >>>> My understanding is that, in Swift, the instance used to store something >>>> whose concrete type is unknown (i.e. is still abstract), but which is >>>> known to conform to some protocol, is called an "existential". Protocols >>>> with associated values cannot be packed into normal existentials because, >>>> even though we know that the concrete type conforms to some protocol, the >>>> associated types represent additional unknowns, and Swift cannot be sure >>>> how to translate uses of those unknown types into callable members. Hence, >>>> protocols with associated types are sometimes called "non-existential". >>>> >>>> If I am misusing the terminology in this area, please understand that >>>> that's what I mean when I use that word. >>>> >>>> -- >>>> Brent Royal-Gordon >>>> Architechies >>>> >>> _______________________________________________ >>> swift-evolution mailing list >>> [email protected] <mailto:[email protected]> >>> https://lists.swift.org/mailman/listinfo/swift-evolution >>> <https://lists.swift.org/mailman/listinfo/swift-evolution>
_______________________________________________ swift-evolution mailing list [email protected] https://lists.swift.org/mailman/listinfo/swift-evolution
