Why there is no subtyping relation between existential meta types?

Evolution Discussion
, ,
1

I'm confused about subtyping (lack of one) in meta types of protocol existentials.

Consider, the following example:

class C {}
class D: C {}

let c: C = D()
let cType: C.Type = D.self // OK

protocol P {}
protocol Q: P {}
struct S: Q {}

let q: Q = S() // OK. S seems to be a subtype of existential for Q.
let qType: Q.Protocol = S.self // error: cannot convert value of type 'S.Type' to specified type 'Q.Protocol'

let p: P = q // OK. Existential for Q seems to be a subtype of existential for P.
let pType: P.Protocol = Q.self // error: cannot convert value of type 'Q.Protocol' to specified type 'P.Protocol'

My intuitive understanding of subtyping is relation is that if you can write

let x: A = ...
let y: B = x

then A is a subtype of B.

And subtyping of types is related to subtyping of meta-types: if A is a subtype of B, then A.Type is also a subtype of B.Type.

Is my understanding correct? Is there a more formal definition?

And I'm confused, because from that logic if follows that S.Type should be a subtype of Q.Protocol, which in turn should be a subtype of P.Protocol. But currently that's not the case.

1 Like
2

There's a difference between Q.Type, which is "the type of all values conforming to Q", and Q.Protocol, which is "the type of the protocol Q". That is, Q.Protocol is not an existential metatype. That explains the S.self example.

Now, should Q.Protocol be a subtype of P.Protocol? That's a little less clear. Abstractly that might be useful: then you could say "I want to check the conformance of some protocol that refines P". But the language doesn't actually support that today, or really any other operations on protocol types, so for now there's not much point.

1 Like
3

Current syntax is pretty confusing. I'm trying to think of P.Protocol, as (any P).Type, this makes things a little more logical. Consider this example with current syntax:

struct Z<T> { init(_ type: T.Type) {} }
let p: P.Protocol = P.self
let z = Z(p)
print(type(of: z)) // prints 'Z<P>'

So, despite of being of type P.Protocol, p is also recognized as being a value of T.Type for T being the type of the existential container for P.

In that sense, when discussing about A and B, in the previous post, I assume that A or B can be existential types as well.

4

No, this is incorrect. It means that there is an implicit conversion from A to B. It may be upcasting (say if A is a subclass of B). It may involve creating an existential box (if say B is a protocol and A conforms to it). It may be a bridging conversion (A can be bridged to B). It may be an allowed implicit conversion between tuples.

    let upair: (Int, Int) = (a: 10, b: 10)
    let lpair: (a: Int, b: Int) = upair

I'm probably missing some other cases as well.

1 Like
5

@typesanitizer, could you explain the difference between subtyping and implicit conversion? Do both exist in Swift?

6

Subtyping forms a partial order.

  1. T is a subtype of T. (reflexivity)
  2. if T is a subtype of U and U is a subtype of T, then T = U (anti-symmetry)
  3. if T is a subtype of U and U is a subtype of V, then T is a subtype of V (transitivity)

Swift has subtyping for classes.

On the other hand, the implicit conversions for tuples don't have this behavior. A labelled tuple is implicitly convertible to an unlabelled tuple and vice-versa, but two labelled tuples are not implicitly convertible to each other (breaking transitivity) and the labelled and unlabelled types are not equal (breaking anti-symmetry).

// Multiple conversions are not permitted, breaking transitivity
let (x, y): (Int, Int) = (x: 10, y: 10) // OK
let (a: a, b: b) = (x, y)               // OK
let (a: _, b: _) = (x: 10, y: 10)       // error: cannot convert value of type '(x: Int, y: Int)' to specified type '(a: Int, b: Int)'

// Prints different types, breaking anti-symmetry
print(type(of: (a: 0, b: 0)), type(of: (0, 0)))

So yes, Swift does have both. What Swift doesn't have (and sometimes people ask for this, but I sure hope we don't implement it) is user-defined implicit conversions.

I misspoke about bridging conversions earlier (they don't happen with :), but (arguably) they do have counter-intuitive behavior -- naively you would expect that let y: T = x would be the same as let y = x as T when both compile but that's not the case.

let y = String() as NSString // OK
let z: NSString = String()   // error

If you relax the idea a bit (to include as and not just :), then it would seem like String and NSString are subtypes of each other and hence equal (by anti-symmetry) but they're not equal (and hence interchangeable), they are "equal upto bridging".

2 Likes
7

What about existential types? It looks like partial order stands for them. Are there any examples breaking anti-symmetry?

8

I've found a good motivational example for existential subtyping. More specifically for subtyping relation between concrete types conforming to P and existential type for P.

It is about the function type(of:). The following code snippet illustrates the problem:

protocol P {}
struct S: P {}

let x: P = S()
let t1: P.Type = type(of: x)
// error: Cannot convert value of type 'P.Type' to specified type 'P.Protocol'
// let t2: P.Protocol = type(of: x)

func getType<T>(of x: T) -> T.Type {
    return type(of: x)
}

func getType2<T>(of x: T) -> Any.Type {
    let y: Any = x
    return type(of: y)
}

let t2: P.Protocol = getType(of: x)
let t3: Any.Type = getType2(of: x)
print(t1, t2, t3) // Prints: S P S

When used in generic context, type(of:) has signature of (T) -> T.Type, and if called with T being the existential type, returns P.self of type P.Protocol.

But when type of argument is statically known, it has signature of (P) -> P.Type, and returns type of the boxed value.

Typing of the type(of:) is a hack (@_semantics("typechecker.type(of:)")), but that's ok, but I'm concerned about the difference in behaviour.

I think this can be solved by making P.Type a subtype of P.Protocol. With P.Protocol becoming a "type of a value that can be implicitly casted to existential container of P". Which includes all concrete types conforming to P, P.self, and also any existential types for protocols derived from P.

This would allow type(of:) to be typed as it is now, but always return the concrete type of the boxed value.

2 Likes
9

Oh geez. Having different behavior for type(of:) depending on whether the type of the given value is statically known or not is indeed confusing. I always assumed it digs down to what the "true underlying type" of the value is at runtime.

1 Like
10

I've been thinking about this in the background for the past week and I don't really have a good answer here. My first instinctive reaction is that "changing the meaning of existing code is probably a bad idea, even if the existing behavior is somewhat unintuitive, because that risks silently breaking someone's code relying on it". That said, I don't have a good sense for how much code this would actually break in practice. Maybe it's fine. :thinking:

11

Another problem is that this is an ABI breaking change. Currently size of P.Protocol is zero. But with existential subtyping it would need to carry a pointer to the type metadata.

Note that while P.Type needs to carry witness table for conformance to P, in case of P.Protocol it is not needed. With t: P.Type, we can call static methods declared in P, but with tEx: P.Protocol we have neither value nor concrete type conforming to P, so we cannot really call anything.

We can try to conditionally downcast P.Protocol to P.Type, but then casting code is responsible for finding the conformance witnesses:

let exT: P.Protocol = ...
if let t = exT as? T.Type {
    t.staticMethod()
}
1 Like
12

I think found an example breaking anti-symmetry. It's self conformance.

Currently you should be able to do this:

let t: Error.Type = Error.self

But [SR-13734] Segfault on let t: Error.Type = Error.self · Issue #56131 · apple/swift · GitHub