For what it's worth, in the abstract I agree with the idea that (any P).Type
probably ought to be the concrete metatype of the existential type and any P.Type
ought to be the existential metatype. P.Type
has always been a rather fast-and-loose syntax because it isn't a simple composition of a type and an operator upon it. If we'd always had any
, that would be easy to clear up.
This might be rather dense, but the formal understanding here is that a protocol type P
(under this proposal, any P
) is the existential type â T:P . T
, which you can read as "there exists a type T
that conforms to P
such that this is a T
". For example, if I have an Int
, I can convert it to Encodable
:
-
Encodable
as a type means â T:Encodable . T
("there exists a type T
that conforms to Encodable
such that this is a T
")
-
Int
is a type that conforms to Encodable
, so it's a valid substitution for T
- The open formula in my existential is just
T
, and if I substitute T=Int
into that, I get Int
- So I can make a value of the existential type if I can provide an
Int
In principle, this can be arbitrarily generalized. For example, â K:Hashable,V:Encodable . [K: V]
means "there exists a type K
that conforms to Hashable
and another type V
that conforms to Encodable
such that this a dictionary from K
to V
". I can make a value of this type from, say, a value of type [String: Int]
by assigning K=String, V=Int
. This existential type would be usefully different from e.g. [AnyHashable: Encodable]
because it expresses that all the keys have the same type and all the values have the same type. But Swift doesn't allow this kind of unrestricted existential, for a variety of reasons.
What Swift does allow is the specific case of an "existential metatype". Swift interprets the syntax P.Type
to mean â T:P . T.Type
, which is to say, "there exists a type T
that conforms to P
such that this is a T.Type
". Therefore, for example, you can form an Encodable.Type
with a value of Int.Type
by letting T=Int
.
This is not a compositional interpretation of that syntax. Taking the components independently, you would expect P.Type
to be (â T:P . T).Type
, i.e. the metatype of the existential type, which is a singleton type (it has exactly one value). But we wanted to allow this existential metatype to be written, and we felt the existential metatype was much more likely to be useful than the singleton metatype of the existential, and we felt that programmers would often reach for it first and be surprised if it didn't work. So we stole the syntax for this purpose.
The any
operator really cannot be totally compositional: it doesn't apply to an arbitrary type, or even to most types, and it essentially rewrites its operand. So building this extra metatype thing into its rewrite rule isn't particularly strange. But the any
operator also acts almost like an â
qualifier, in that you could naturally think of it as "containing" the rewrite and producing a normal type that you would expect to behave compositionally. Compositionally, (any P).Type
would be the metatype of the existential, and so different from any P.Type
. That's weird, but not that weird.
Unfortunately, I'm not sure we can get away with making that change, because I think it might have weird implications for typealias
es. typealias MyP = P
is something that people can write today, and MyP.Type
is the existential metatype, not the metatype of an existential. Do we disallow this somehow? Does it change behavior if someone rewrites it to typealias MyP = any P
, so that whether a protocol (or protocol composition) typealias
is "any
-ed" changes the semantics? This might be too much for people to understand.