Great! Thanks for the additional details! -Thorsten
> Am 31.05.2016 um 19:31 schrieb John McCall <[email protected]>: > >> 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) >> >> "Existential quantification hides a type variable within a data constructor.“ >> (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) >> >> >> >>>> Am 27.05.2016 um 19:36 schrieb John McCall <[email protected]>: >>>> >>>> On May 25, 2016, at 7:07 AM, Thorsten Seitz via swift-evolution >>>> <[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]>: >>>> >>>>>> 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), 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] >>>> https://lists.swift.org/mailman/listinfo/swift-evolution >> >
_______________________________________________ swift-evolution mailing list [email protected] https://lists.swift.org/mailman/listinfo/swift-evolution
