<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div><blockquote type="cite" class=""><div class="">On May 29, 2016, at 6:38 AM, Thorsten Seitz &lt;<a href="mailto:tseitz42@icloud.com" class="">tseitz42@icloud.com</a>&gt; wrote:</div><div class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">An, now I see what you mean. You are right, P ::= ∃ t : P . t is a constrained existential type defining a subtype relationship.<div class="">Thanks for enlightening me!<br class=""><div class=""><br class=""></div><div class="">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.</div><div class="">Is there another terminology to distinguish between those two kinds?</div></div></div></div></blockquote><div><br class=""></div>It's not a standard restriction or really even a necessary one. &nbsp;It's an artifact of earlier implementations of both the type-checker and the runtime representation of protocol conformances.</div><div><br class=""></div><div>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. &nbsp;That's a type-checking strategy that's extremely prone to soundness bugs, so a harsh restriction is required. &nbsp;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.</div><div><br class=""></div><div>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.<br class=""><div><br class=""></div><div>So I wouldn't sweat trying to formally describe the current situation, because it's a "temporary" implementation limitation.</div><div><br class=""></div><div>John.</div></div><div><br class=""></div><div><br class=""><blockquote type="cite" class=""><div class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div class=""><div class=""><br class=""></div><div class="">-Thorsten</div><div class=""><br class=""></div><div class=""><br class=""></div>"Existential types, or 'existentials' for short, are a way of 'squashing' a group of types into one, single type. […]&nbsp;</div><div class="">data T = forall a. MkT a“&nbsp;</div><div class="">(<a href="https://en.wikibooks.org/wiki/Haskell/Existentially_quantified_types" class="">https://en.wikibooks.org/wiki/Haskell/Existentially_quantified_types</a>)<div class=""><br class=""></div><div class="">"Existential quantification hides a type variable within a data constructor.“</div><div class="">(<a href="https://prime.haskell.org/wiki/ExistentialQuantification" class="">https://prime.haskell.org/wiki/ExistentialQuantification</a>)<br class=""><div class=""><br class=""></div><div class="">"For example, the type "T = ∃X { a: X; f: (X → int); }" describes a module interface that has a data member named&nbsp;a&nbsp;of type&nbsp;X&nbsp;and a&nbsp;function named&nbsp;f&nbsp;that takes a parameter of the&nbsp;same&nbsp;type&nbsp;X&nbsp;and returns an integer. […]&nbsp;Given a value "t" of type "T", we know that "t.f(t.a)" is well-typed, regardless of what the abstract type&nbsp;X&nbsp;is. This gives flexibility for&nbsp;choosing types suited to a particular implementation while clients that use only values of the interface type—the existential type—are&nbsp;isolated from these choices.“</div><div class="">(<a href="https://en.wikipedia.org/wiki/Type_system#Existential_types" class="">https://en.wikipedia.org/wiki/Type_system#Existential_types</a>)</div><div class=""><br class=""></div><div class=""><div class=""><br class=""></div><div class=""><br class=""><div class=""><blockquote type="cite" class=""><div class="">Am 27.05.2016 um 19:36 schrieb John McCall &lt;<a href="mailto:rjmccall@apple.com" class="">rjmccall@apple.com</a>&gt;:</div><br class="Apple-interchange-newline"><div class=""><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><blockquote type="cite" class=""><div class="">On May 25, 2016, at 7:07 AM, Thorsten Seitz via swift-evolution &lt;<a href="mailto:swift-evolution@swift.org" class="">swift-evolution@swift.org</a>&gt; wrote:</div><div class=""><div class=""><div class="">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 :-(</div></div></div></blockquote><div class=""><br class=""></div>I don't know what you mean by this. &nbsp;The standard terminology is that an existential type is one that's directly existentially-quantified, e.g.&nbsp;∃ t . t, which is essentially what a Swift protocol type is:</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">&nbsp; P ::=&nbsp;∃ t : P . t</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">&nbsp; P.Type ::=&nbsp;∃ t : P . t.Type</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">etc. &nbsp;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.</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">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. &nbsp;(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.)</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">John.</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""><blockquote type="cite" class=""><div class=""><div class=""><div class=""><br data-mce-bogus="1" class=""></div><div class="">-Thorsten<br data-mce-bogus="1" class=""></div><div class=""><br data-mce-bogus="1" class=""></div><div class=""><br class="">Am 25. Mai 2016 um 14:27 schrieb Brent Royal-Gordon &lt;<a href="mailto:brent@architechies.com" class="">brent@architechies.com</a>&gt;:<br class=""><br class=""><div class=""><blockquote type="cite" class=""><div class="msg-quote"><div class="_stretch"><span class="body-text-content"><blockquote type="cite" class="quoted-plain-text">AFAIK an existential type is a type T with type parameters that are still abstract (see for example<span class="Apple-converted-space">&nbsp;</span><a href="https://en.wikipedia.org/wiki/Type_system#Existential_types" data-mce-href="https://en.wikipedia.org/wiki/Type_system#Existential_types" class="">https://en.wikipedia.org/wiki/Type_system#Existential_types</a>), i.e. have not been assigned concrete values.</blockquote><br class="">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".<br class=""><br class="">If I am misusing the terminology in this area, please understand that that's what I mean when I use that word.<br class=""><br class="">--<span class="Apple-converted-space">&nbsp;</span><br class="">Brent Royal-Gordon<br class="">Architechies<br class=""><br class=""></span></div></div></blockquote></div></div></div>_______________________________________________<br class="">swift-evolution mailing list<br class=""><a href="mailto:swift-evolution@swift.org" class="">swift-evolution@swift.org</a><br class=""><a href="https://lists.swift.org/mailman/listinfo/swift-evolution" class="">https://lists.swift.org/mailman/listinfo/swift-evolution</a></div></blockquote></div></div></blockquote></div><br class=""></div></div></div></div></div></div></blockquote></div><br class=""></body></html>