Refinements for sealed types

[Remi Forax]

----- Mail original -----
> De: "Brian Goetz" <brian.goetz at oracle.com>
> À: "amber-spec-experts" <amber-spec-experts at openjdk.java.net>
> Envoyé: Samedi 17 Août 2019 16:24:18
> Objet: Re: Refinements for sealed types

> Since I got a few questions on this, let me step back a bit further and
> shed some light on these requirements.
> 
> Sealed types are really *two* features in one:
> 
>  - Declaring a sum type, so that the sum constraint is visible to the
> compiler as a source of exhaustiveness in flow analysis (e.g., switch
> totality.)
>  - A more refined notion of "final", that allows class authors to be
> able to reason about "I know where all the implementations of this type
> are".
> 
> While the two fit (mostly) neatly into the same package, they serve very
> different audiences.  Many of the comments and questions we've gotten
> basically come down to assuming that one of these use cases is the
> "real" design goal, and the other is just a lucky accident.
> 
> Users will, hopefully, declare sums (often sums of records) in all sorts
> of places.  These folks generally don't care about "I know all the
> implementations", because these classes often have no nontrivial
> implementation, they are data carriers.
> 
> Platform developers are more likely to use sealing as a means of
> building safe APIs.  Think of how many classes are final -- for good
> reasons -- but we later wished there could be multiple implementations.
> APIs like ConstantDesc are a primary example of the second sub-feature;
> we want to expose polymorphic APIs, but control the implementations.
> (Historically we have resorted to using abstract classes with non-public
> constructors for that, but this is obviously a suboptimal move.)
> 
> In that light, wanting to infer the permitted subtypes when they are
> co-declared is reducing ceremony for users of SubFeature 1, and and
> wanting to avoid accidental unsealing is an important safety feature for
> users of SubFeature 2.

I agree about the premise of this mail, there are two ways to see a sealed type as a sum type or as a closed inheritance hierarchy.

Reducing the ceremony is a good idea by itself but i think we are not acting logically here,
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.

So i think we should first defines the rules when everything is explicit and then add the rules that reduce the ceremony.

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 ?

Rémi

> 
> On 8/15/2019 1:38 PM, Brian Goetz wrote:
>> As Gavin has worked through the spec for sealed types, it has shone a
>> spotlight on one of the messy parts -- implicitly sealed types. I've
>> got an alternate way to stack this that I think is simpler and still
>> meets the goals.
>>
>> First, the goals (which in most cases align, but in some cases
>> conflict with each other):
>>
>> Unsealed concrete leaves should not be the default.  If we follow the
>> default strategy that a class declaration gets only the flags that are
>> declared explicitly (which is generally a good default), it is quite
>> likely that many subtypes of sealed types will be extensible, when
>> that was not the intent or understanding of the author.  For example,
>> in a hierarchy like the following:
>>
>>     sealed interface X permits A, B { }
>>     class A implements X { }
>>     class B implements X { }
>>
>> it is highly likely to be a source of mistakes that A and B are
>> neither sealed nor final, even though they are co-declared with the
>> sealed interface.  The author may well assume that they are in control
>> of all the implementations of X methods, when in fact anyone can
>> subclass A and override those methods.
>>
>> Avoiding excessive ceremony.  If the user had to declare every
>> concrete subtype as final, this may well be seen as excess ceremony.
>> (This is the same reason we allow the permits clause to be inferred.)
>>
>> In the current design, we took the following path:
>>
>>  - Subtypes of sealed types are implicitly sealed, unless marked
>> non-sealed.
>>  - We infer a permits clause when it is omitted, which is possibly
>> empty (in which case the type is effectively final.)
>>
>> These are reasonable defaults, both from avoiding the safety question
>> of accidental extensibility, and reducing ceremony, but they interact
>> in some uncomfortable ways.  For example, under these rules, its
>> possible to have an explicit "permits" clause without saying "sealed",
>> which is a little strange.  And it is possible to infer both sealing
>> and the permits list, which might exceed our nontransparency comfort
>> level.
>>
>> So, let me propose a simplification:
>>
>>  - A concrete subtype A of a sealed type X, which has no permits
>> clause, no known subtypes, and is not marked non-sealed, is implicitly
>> sealed (with an empty permits clause).
>>  - Any other subtype of a sealed type must either have a "sealed"
>> modifier, or a "non-sealed" modifier.
>>  - Any type with a permits list must have a sealed modifier.
>>
>> Rationale: This still manages to avoid the "accidental extension"
>> problem, and addresses both the extension and the ceremony problem
>> where they are both most severe -- at the leaves.  Abstract types
>> (which are generally fewer in number than leaves) err on the side of
>> explicitness.
>>
>> So the above hierarchy could be written as above, and A/B would be
>> implicitly final, as desired.  If A or B wanted to permit subtypes,
>> they would need to be explicitly marked non-sealed (to reopen them),
>> or explicitly sealed (with or without an explicit permits list.)
>>
>> I think this stays within the spirit of the goals, but with a little
>> less magic / complexity.