Write separate more detailed spec for sealed types.

[munificent]

I forked this off from the larger type-modifiers strawman for a few reasons:

• That strawman also proposed disallowing mixing in classes which is a larger breaking change that will require a migration. We almost certainly can't get that done in time for patterns.

• There is a lot more motivation around keyword choices in that doc which is useful to have tracked, but not super relevant for a feature spec, at least not at that level of detail.

• The "closed" and "base" modifiers in that proposal are small features with no breakage, and can likely be done quickly. But they'll still probably be behind a separate experiment flag from "sealed", so I thought it made sense to propose those separately.

I also changed the keyword from "switch" to "sealed". While some liked the former, my general impression is that most don't and it didn't seem to "stick". When we talk about the feature, we all seem to call it "sealed", which is probably telling us something.

cc @lrhn @jakemac53 @natebosch @stereotype441

[lrhn]

I like the semantics. They get the job done.
I really do not like using sealed as the word.

I'd prefer switch class or enum class over that (even if I know enum class is highly confusing).
The only use of exhaustiveness is in switch operations anway.
(Right? Or do we plan to, some day, treat the sealed subtypes as union types, so A a = ...; if (a is B) { ... } else { /* a promoted to C here, which is the only type in A\B *. }? So, union class?)

[lrhn]

Not sold on sealed not meaning transitively sealed.
I think people will expect sealed to mean that nobody can create instances implementing the type, not just that nobody can create immediate subtypes.

[munificent]

Not sold on sealed not meaning transitively sealed.

This is consistent with how sealed works in Kotlin, Scala, and Java (which does require you to explicitly opt the subclass in by marking it non-sealed, but the capability is there).

I was surprised too, but my informal understanding of sealed turned out to have been wrong once I dug into the semantics.

not just that nobody can create immediate subtypes.

If you want that, you can always mark the subtypes sealed too. (Or closed/base if we get those.)

Fundamentally, the way I've approached this design is, "What is the simplest set of restrictions that we need for exhaustiveness checking to work." As far as pattern matching cares, if you have a sealed type Either and two subtypes Left and Right, it does not matter at all if Left or Right happen to have their own subtypes. It's perfectly sound either way. Given that, I don't see any reason to add an unneeded restriction (which users can opt into already if they want).

[lrhn]

What is the reasoning for this restriction?

I'm thinking that we can allow the superclass to be instantiated. Then we need to include that class itself in the set of types to check to achieve exhaustiveness. You can still write abstract to avoid it.
Disallowing it should have a reason. I'm sure there are plenty of good reason, I'm just curious which ones we've used to reach the conclusion :)

I can come up with:

• It's what you'd usually want. Avoids having to write abstract on the superclass.
• If not, people may forget to write abstract on the superclass, then their switches are not exhaustive.
• If we use abstract on superclass to decide whether it needs to be part of exhaustiveness checking, we are adding implicit meaning on top of just being abstract. That really should be explicit opt-in.
• If the superclass itself is part of exhaustiveness checking, ordering of switch cases matter. Breaks what should be nicely symmetric.
• It makes exhaustiveness checking easier to just disallow it.

[munificent]

What is the reasoning for this restriction?

It's necessary to make sealed types useful. If you can have direct instances of the supertype, then in pattern matching, you have to explicitly check the supertype in addition to its subtypes. But if you have to check the supertype anyway... then you derive absolutely no benefit from marking it sealed in the first place. The whole point of sealing is to know that if you've handled all the subtypes you are done. Direct instances of the supertype break that.

[lrhn]

This is precisely the reason using the word sealed worries me.
Of these types, only num is actually exhustive-sealed. The rest are really sealed.
They have not "behaved like sealed types" with this definition of sealed.

I don't want people to start using exhaustive-sealed instead of really-sealed, just because it's the only thing they have. For one thing, it doesn't work, because the class becomes abstract. I guess it can work, but then you need to introduce a private non-abstract subclass, just to get the sealing.

We generally pretend that int, double and String are not abstract classes, and the values are instances of those classes (even if the VM has subclasses, dart2js doesn't always).
We definitely treat Null and bool as non-abstract, with null, true and false as actual instances of those types. (I don't want to consider the effect on our type system if Null has a subtype.)
At least all their constructors are factory constructors.

---

An alternative is to actually use sealed, and iff the sealed class is abstract, then it's gives exhaustiveness checking of immediate subtypes. If not abstract, it's just not implementable outside the library, but you don't get exhaustiveness checking of immediate subtypes.

Then you can seal all your types, abstract or not, in order to prevent implementations from outside the library.
(Still worries me that doing so opts you into exhaustiveness if you ever have an abstract superclass, with no way to opt out.)

So, I worry about using sealed as the word, and this section is a good example of the confusion it can cause. Exhaustiveness is not the traditional "sealed" meaning.

[munificent]

This is precisely the reason using the word sealed worries me. Of these types, only num is actually exhustive-sealed. The rest are really sealed. They have not "behaved like sealed types" with this definition of sealed.

I believe these types do behave like types marked sealed according to this proposal. The sealed modifier means "the only direct subtypes of this type must be in this library". It doesn't say that there must actually be any subtypes. And if there are none (or they are all sealed too), then a sealed type is also effectively transitively sealed, which is what we observe with the listed core lib types.

It is true that marking a class sealed while it having no subtypes in the same library means that it doesn't really give you any exhaustiveness checking benefit. It's effectively synonymous with closed base. But, if we don't get those modifiers, then marking them sealed has the same effect.

[leafpetersen]

Not sure about Null. It's just not really a class (what is its superclass?), so talking about it as sealed is fine loosely speaking, but I think kind of meaningless. The rest seems to work out to me. I think we may also have the SIMD types in this category? Are there other things we should go ahead and try to seal?

[munificent]

I think we may also have the SIMD types in this category? Are there other things we should go ahead and try to seal?

I'm fine with whatever we want to seal, though adding to this list might mean breaking changes, which I'd like to avoid in the interests of expedience.

[leafpetersen]

Actually, it's the TypedData classes. But the point is they're already sealed. dart-lang/sdk#45115

[lrhn]

Null is definitely a class. It has no superclass. That's the same as Object, and nobody doubts that Object is a class.

dartlangspec.tex:8665:

The null object is the sole instance of the built-in class \code{Null}.

Anyway,

I believe these types do behave like types marked sealed according to this proposal. The sealed modifier means "the only direct subtypes of this type must be in this library".

This sealed also implies abstract, and those classes are not abstract. They all have instances.
We can claim that the instances are actually instances of a private subclass that we never tell anyone about, and that's even true for numbers and strings on Native. It's not true on the web.
It's not true for bool or Null on native.

These classes are a different kind of sealed, the transitive one, not just the exhaustiveness one.
Nobody ever cared about exhaustivness for them. If we could make them closed base class, we wouldn't even consider using this sealed as defined here.

For typed-data, there really are subclasses in the library, because all the constructors are factory ones. We'd still use closed base class for those if we could, not sealed.

Misusing sealed to mean "cannot be subclassed outside of the library at all" is what I'd consider a failure of the design. It's one of those things that kind-of works if you squint at it correctly, but if you forget that it's a hack and introduces a publicly visible subtype (even using implements), you break the protection. It simply is not the protection we want here, we want the full, transitive protection against anyone ever creating anything implementing int.

[natebosch]

adding to this list might mean breaking changes

As long as those breaking changes are gated by the language version it shouldn't be a deal breaker. We should definitely consider whether there are any other classes worth sealing if we think there is an easy enough migration path.

[munificent]

This sealed also implies abstract, and those classes are not abstract. They all have instances.

For the purposes of making exhaustiveness checking work, this distinction doesn't matter for types like int and double which have no subtypes. You're correct that they aren't abstract. But they don't need to be. Since there is no set of subtypes you could match on, you have to match on the sealed type itself in order to cover it exhaustively. And once you do that, it's harmless for it to be non-abstract.

(We could even potentially spec sealed to say when applied to user-defined classes, they can be non-abstract if there are no subtypes. But I suspect that would just make things more confusing for users. It's probably better to just have something like closed/base/whatever to let them express that directly without getting exhaustiveness involved.)

[leafpetersen]

Null is definitely a class. It has no superclass. That's the same as Object, and nobody doubts that Object is a class.

language/specification/dartLangSpec.tex

Line 2500 in 04e34f8

Every class has a single superclass

Every class has a single superclass except class \code{Object} which has no superclass.

The spec says a lot of things, some of them even true. :)

[eernstg]

some of them are even true

Some truths have been updated, and may even be landed at some point. ;-)

In particular, https://github.com/dart-lang/language/pull/2605/files#diff-0e2f05538272f3fb682a361d7738d860125088af3ac0044e5472cac965cfdb61R24431 has:

The \code{Null} class declares exactly the same members
with the same signatures as the class \code{Object}.

and the text weasels around the question about the superclass, because I'd prefer that we introduce a class Any which is the top type (with no attached strings, unlike dynamic and void), and then we would say that Object has superclass Any, and Null also has superclass Any, and then we don't have to deal with a situation any more where Object? somehow isn't a class and the relationship between Null and Object is an anomaly.

[munificent]

I really do not like using sealed as the word.

I filed #2594 for us to discuss it more, since I think it will need input from others on the language team too.

Or do we plan to, some day, treat the sealed subtypes as union types, so A a = ...; if (a is B) { ... } else { /* a promoted to C here, which is the only type in A\B *. }? So, union class?)

See: #2179.

[leafpetersen]

Not completely sold on the syntax yet, but the basic structure LGTM.

[munificent]

I'm going to go ahead and land this, but I obviously still consider all of it up for discussion. It's just easier to iterate on a landed doc than keeping a long-running PR going.