Refinements for sealed types

[forax at univ-mlv.fr]

> De: "Brian Goetz" <brian.goetz at oracle.com>
> À: "Remi Forax" <forax at univ-mlv.fr>
> Cc: "amber-spec-experts" <amber-spec-experts at openjdk.java.net>
> Envoyé: Dimanche 18 Août 2019 21:25:28
> Objet: Re: Refinements for sealed types

>> So if everything is explicit, we want
>> - all sealed types to defines their permit clauses
>> (so we need a kind of "permit none" if no subtypes is allowed ?)
>> - all subtypes of a seal types to explicitly says if there are sealed or non
>> sealed (to avoid accidental unsealing).

>> am i right, or am i missing something ?

> Yes, this is basically it. I don’t think we need “permits none” because a sealed
> type with no permitted subtypes is effectively a final type, and only makes
> sense for concrete classes, so that’s a final class.

And the followup question is "is it ok to have an interface declared final ?" 

>> There are several ways to reduce the ceremony
>> - implicit declaration of sealed subtypes if the super type is sealed
>> - implicit declaration of permit clauses
>> and we may want to choose one, the other or both.
> Right. Now, some observations:

> - We have two cases (sum types, and restricted hierarchies), and two goals
> (ceremony management, and safety/clarity);
> - Implicit sealing of subtypes by default serves both goals and both use cases,
> but asymmetrically; it provides ceremony reduction for the sum types case, and
> safety for the restricted hierarchy case.
> - Ceremony reduction is far more important for the “sum types” use case than for
> the “restricted hierarchy” use case, for several reasons.
> - Implicit declaration of permits clauses provides ceremony reduction for the
> sum types case.
> - Both forms of ceremony reduction start to cross over into being liabilities
> for the restricted-hierarchy case, because readers should have full information
> about the hierarchy shape.
> - Most sum types will be co-declared; many restricted hierarchies will not be.

> So, given all this, we should focus all our ceremony-reduction on the case of
> co-declared sum types. Which is mostly what I think I was suggesting:

> - Infer the permits clause when all the subtypes are co-declared;
> - Infer “final” for leaf classes in a sum type;
> - Require explicitness in both sealed/non-sealed, and permits clause, in other
> cases.

ok, i prefer this explanation, it's clearer at least for me, 

> We could tighten this further, which probably makes sense:
> - Infer the permits clause when the subtypes are co-declared;
> - Infer final _when the current class is a subtype of a sealed type in the same
> compilation unit, and has no subtypes_ (again, co-declared with its parent);
> - Require explicit sealed or non-sealed in all other cases;
> - Require explicit permits clause in all other cases.

> So this focuses the magic on co-declared hierarchies.

I prefer this version. 

Rémi 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.java.net/pipermail/amber-spec-experts/attachments/20190820/e673cb39/attachment.html>