Should promotion take sealed types into account?

[munificent]

In order to support exhaustiveness checks in algebraic datatype-style code in pattern matching, we want some notion of sealed types.

That raises the question of whether sealed types should come into play with type promotion. For example:

sealed class Foo {} // Only subtypes are Bar and Baz
class Bar extends Foo {}
class Baz extends Foo {}

test(Foo foo) {
  if (foo is Bar) return;
  // Promote foo to Baz here?
}

I suspect that the answer is "yes", since this seems practically useful.

[jakemac53]

One concern with this is it would make it more likely for users to be broken by a package adding a new sub-type of a sealed class, because the promotion could no longer work where it did before.

This was already breaking anywhere exhaustiveness checking applies, so maybe not a large issue, but it might be easier to accidentally rely on the exhaustiveness checking in this case than say a switch statement.

[munificent]

That's true, but that is something a package author is deliberately signing themselves up for when they mark a supertype as sealed. If we treated "sealed" as a distinct concept from "final" (i.e. preventing subclassing/implementing/etc.) then the only reason to seal a class is to opt in to exhaustiveness checking. And once you do that, adding a new subtype is always a potentially breaking change, type promotion or not.

[jakemac53]

then the only reason to seal a class is to opt in to exhaustiveness checking

There are other reasons as well, you might not support arbitrary subtypes of your class for a variety of reasons. In particular you might be using some private members from the concrete type inside of some public function in the same library.

[leafpetersen]

There are other reasons as well, you might not support arbitrary subtypes of your class for a variety of reasons.

sealed as used in this context allows essentially arbitrary indirect subtypes.

[jakemac53]

sealed as used in this context allows essentially arbitrary indirect subtypes.

So is this allowed?

sealed class Animal {}
class Dog extends Animal {}

And then in some other library:

class Husky implements Dog {}

As far as exhaustiveness I see how that would be allowed, even though it's a bit weird that it implements Dog, it doesn't give much value in terms of the safety I would expect from sealing?

[jakemac53]

Of course on the flipside, this means you can implement Dog as a mock, so there are testing advantages to that approach.

[munificent]

So is this allowed?

sealed class Animal {}
class Dog extends Animal {}

And then in some other library:

class Husky implements Dog {}

As far as exhaustiveness I see how that would be allowed, even though it's a bit weird that it implements Dog, it doesn't give much value in terms of the safety I would expect from sealing?

Well, we don't technically have a real proposal for sealed types yet. But, as far as what exhaustiveness checking needs, yes, the exhaustiveness algorithm has no problem with code like the above.

In my mind, this is another point in favor of making a distinction between "sealed" and "final" classes because they are somewhat orthogonal and can be combined freely. You could have a superclass whose subclasses are all final because you don't want users to extend them but you want to retain the freedom to add more subclasses of the superclass later so you don't mark it sealed. And, conversely, you could have a sealed class like Animal here whose subclasses aren't final.

[munificent]

@stereotype441, any thoughts on this? I'm guessing there are no plans to do this. The proposal for sealed doesn't propose or specify it.

[lrhn]

I'm split.

I do want union types to be separable by tests, so FutureOr<X> f; if (f is FutureOr<X>) { ... } else { // f is X! } works (which it does today, and X? v; if (v == null) { ... } else {// v is X} works too).

But I also don't want the complication of full switch-exhaustiveness checking to apply to a chain of if (x is T) else tests. There are so many ways you can do a small tweak to such a chain so that it no longer works for exhaustiveness checking, and there is no requirement that it does, so you won't notice.

Maybe that's the answer: What if we say that sealed types are union types, and we do promote when you eliminate part of a union type, but the full sub-pattern exhaustiveness, and requirements about it, only applies to switches.

In that case I would promote foo to Baz because you started with the union type Foo ::= Bar|Baz, and you eliminated Bar.

More generally, if a value has a union type, then it can be promoted to a subset of the elements of the union. That's not always an expressible type, just like a promoted type variable isn't.

If you have:

sealed class Sup {}
class Sub1 extends Sup {}
class Sub2 extends Sup {}
class Sub3 extends Sup {}

you can promote as

test(Sup foo) {
  // foo has type Sup aka. Sup&{Sub1,Sub2,Sub3}
  if (foo is Sub1) return;
  // foo has type Sup&{Sub2,Sub3}
  if (foo is Sub2) return;
  // foo has type Sup&{Sub3} =def= Sub3
  Huzzah();
}

It should work the same for FutureOr<X> and X? which are binary (non-exclusive) union types.

The complications that I worry about are things like:

sealed class Foo {}
class Bar extends Foo {}
sealed class Baz extends Foo {}
class Baz1 extends Baz {}
class Baz2 extends Baz {}
...
test(Foo foo) {
  if (foo is Baz1) return;
  if (foo is Baz2) return;
  // Have we eliminated Baz, and promoted foo to `Bar` now?
}

I guess we can generalize to union-types of other union-types, so it's

test(Foo foo) {
  // foo : Foo{Bar,Baz{Baz1,Baz2}}
  if (foo is Baz1) return;
  // foo : Foo{Bar,Baz{Baz2}} == Foo{Bar,Baz2}
  if (foo is Baz2) return;
  // foo : Foo{Bar} == Bar
  // We *have* eliminated all of Baz, and promoted foo to `Bar` now?
}

I think it would be nice and useful.

Or we can do nothing, but then it becomes much harder to add it later. Our story is that if you want that kind of promotion or exhaustion, use a switch.
It's just not a particularly good story when it's obvious that we can figure it out in one place, and then we don't in another.

@stereotype441 Does this sound at all viable? 😅

[munificent]

I'm going to go ahead and close this. We don't have any plans to do it and my understanding is that even if we wanted to, we couldn't easily since it requires type machinery we don't currently have:

sealed class Foo {} // Only subtypes are Bar and Baz
class Bar extends Foo {}
class Baz extends Foo {}
class Bang extends Foo {}

test(Foo foo) {
  if (foo is Bar) return;
  // What is the type of foo here?
}

Without union types, there isn't an expressible answer. And I suspect that even if we had union types, it's probably still better to confine exhaustiveness checking of sealed hierarchies to switches where the algorithm is simpler and more tractable.